Skip to content

Commit

Permalink
Fix crashing when loading lean config
Browse files Browse the repository at this point in the history
This fixes a crash that occurs when lean is configured outside of a
`config` function from packer. Technically---instead of communicating
changes to the filetype configuration through a shared configuration
global, the relevant configuration (default filetype) is shared through
one single global.
Furthermore, if this global is written by the user before the plugin is
loaded, then this global will not be managed by the plugin. This allows
a user to configure default filetype even if the plugin is not loaded!

Fixes Julian#275
  • Loading branch information
4e554c4c committed Sep 5, 2022
1 parent 2858b36 commit 87ccbd1
Show file tree
Hide file tree
Showing 3 changed files with 30 additions and 16 deletions.
2 changes: 1 addition & 1 deletion .luacheckrc
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
globals = {
"_clean_buffer_count",
"vim",
"lean_nvim_ft_options",
"lean_nvim_default_filetype",
assert = {fields = {"message"}},
}
17 changes: 5 additions & 12 deletions ftdetect/lean.lua
Original file line number Diff line number Diff line change
Expand Up @@ -8,24 +8,17 @@ local find_project_root = require('lspconfig.util').root_pattern(
'lean-toolchain'
)

lean_nvim_ft_options = {
default = "lean",
nomodifiable = {
'.*/src/lean/.*', -- Lean 4 standard library
'.*/lib/lean/src/.*', -- Lean 4 legacy standard library
'.*/lean_packages/.*', -- Lean 4 dependencies
_LEAN3_STANDARD_LIBRARY .. '.*',
'/_target/.*/.*.lean' -- Lean 3 dependencies
}
}

local function detect(filename)
if filename:match('^fugitive://.*') then
filename = pcall(vim.fn.FugitiveReal, filename)
end

local abspath = vim.fn.fnamemodify(filename, ":p")
local filetype = lean_nvim_ft_options.default
local filetype = lean_nvim_default_filetype
if not filetype then
filetype = 'lean'
end

if abspath:match(_LEAN3_STANDARD_LIBRARY) then
filetype = 'lean3'
else
Expand Down
27 changes: 24 additions & 3 deletions lua/lean/ft.lua
Original file line number Diff line number Diff line change
@@ -1,15 +1,36 @@
local ft = {}
local _LEAN3_STANDARD_LIBRARY = '.*/[^/]*lean[%-]+3.+/lib/'

lean_nvim_ft_options._DEFAULTS = vim.deepcopy(lean_nvim_ft_options)
local options = {
default = "lean",
nomodifiable = {
'.*/src/lean/.*', -- Lean 4 standard library
'.*/lib/lean/src/.*', -- Lean 4 legacy standard library
'.*/lean_packages/.*', -- Lean 4 dependencies
_LEAN3_STANDARD_LIBRARY .. '.*',
'/_target/.*/.*.lean' -- Lean 3 dependencies
}
}

options._DEFAULTS = vim.deepcopy(options)

local global_default_managed = false
function ft.enable(opts)
lean_nvim_ft_options= vim.tbl_extend("force", lean_nvim_ft_options._DEFAULTS, opts)
if not global_default_managed and not lean_nvim_default_filetype then
-- we are not managing the ft global, but it has no value.
-- this means we have to manage it
global_default_managed = true
end
options= vim.tbl_extend("force", options._DEFAULTS, opts)
if global_default_managed then
lean_nvim_default_filetype = options.default
end
end

---Make the given buffer `nomodifiable` if its file name matches a configured list.
function ft.__maybe_make_nomodifiable(bufnr)
local name = vim.api.nvim_buf_get_name(bufnr)
for _, pattern in ipairs(lean_nvim_ft_options.nomodifiable) do
for _, pattern in ipairs(options.nomodifiable) do
if name:match(pattern) then
vim.api.nvim_buf_set_option(bufnr, 'modifiable', false)
return
Expand Down

0 comments on commit 87ccbd1

Please sign in to comment.