2019-12-28 12:16:32 +01:00
|
|
|
local config = {}
|
|
|
|
|
|
|
|
config.fps = 60
|
2020-05-06 00:40:42 +02:00
|
|
|
config.max_log_items = 80
|
2021-05-27 08:28:58 +02:00
|
|
|
config.message_timeout = 5
|
2020-05-16 10:46:31 +02:00
|
|
|
config.mouse_wheel_scroll = 50 * SCALE
|
2021-09-30 22:10:38 +02:00
|
|
|
config.scroll_past_end = true
|
2019-12-28 12:16:32 +01:00
|
|
|
config.file_size_limit = 10
|
2022-01-28 22:30:19 +01:00
|
|
|
config.ignore_files = { "^%." }
|
2019-12-28 12:16:32 +01:00
|
|
|
config.symbol_pattern = "[%a_][%w_]*"
|
|
|
|
config.non_word_chars = " \t\n/\\()\"':,.;<>~!@#$%^&*|+=[]{}`?-"
|
|
|
|
config.undo_merge_timeout = 0.3
|
|
|
|
config.max_undos = 10000
|
2021-10-02 18:44:05 +02:00
|
|
|
config.max_tabs = 8
|
|
|
|
config.always_show_tabs = true
|
2021-12-20 12:20:06 +01:00
|
|
|
-- Possible values: false, true, "no_selection"
|
2019-12-28 12:16:32 +01:00
|
|
|
config.highlight_current_line = true
|
|
|
|
config.line_height = 1.2
|
|
|
|
config.indent_size = 2
|
|
|
|
config.tab_type = "soft"
|
|
|
|
config.line_limit = 80
|
2020-11-16 14:45:45 +01:00
|
|
|
config.max_project_files = 2000
|
2021-02-21 11:08:25 +01:00
|
|
|
config.transitions = true
|
2021-03-10 16:35:37 +01:00
|
|
|
config.animation_rate = 1.0
|
2021-03-06 11:03:12 +01:00
|
|
|
config.blink_period = 0.8
|
2021-10-02 16:38:10 +02:00
|
|
|
config.disable_blink = false
|
2021-03-31 17:33:35 +02:00
|
|
|
config.draw_whitespace = false
|
2021-04-21 09:05:15 +02:00
|
|
|
config.borderless = false
|
2021-06-18 03:35:36 +02:00
|
|
|
config.tab_close_button = true
|
2021-11-14 21:44:54 +01:00
|
|
|
config.max_clicks = 3
|
2019-12-28 12:16:32 +01:00
|
|
|
|
2021-07-13 16:14:00 +02:00
|
|
|
config.plugins = {}
|
2021-12-06 00:32:20 +01:00
|
|
|
-- Allow you to set plugin configs even if we haven't seen the plugin before.
|
2022-01-28 22:30:19 +01:00
|
|
|
setmetatable(config.plugins, {
|
|
|
|
__index = function(t, k)
|
|
|
|
if rawget(t, k) == nil then rawset(t, k, {}) end
|
|
|
|
return rawget(t, k)
|
|
|
|
end
|
2021-12-06 00:32:20 +01:00
|
|
|
})
|
2021-07-13 16:14:00 +02:00
|
|
|
|
2021-12-06 00:32:20 +01:00
|
|
|
-- Disable these plugins by default.
|
2021-07-13 16:14:00 +02:00
|
|
|
config.plugins.trimwhitespace = false
|
|
|
|
config.plugins.lineguide = false
|
2021-10-02 18:23:32 +02:00
|
|
|
config.plugins.drawwhitespace = false
|
2021-01-13 14:50:24 +01:00
|
|
|
|
2019-12-28 12:16:32 +01:00
|
|
|
return config
|