diff --git a/README.rst b/README.rst index 971ad823..8b34114d 100644 --- a/README.rst +++ b/README.rst @@ -11,17 +11,18 @@ Prerequisites ``lean.nvim`` currently requires `neovim 0.5 HEAD / nightly `_. -For syntax highlighting and basic language support, you should either: +NOTE: ``lean.nvim`` is incompatible with `lean.vim `_, +as it implements its own kind of filetype detection. +You should NOT have ``lean.vim`` installed if using ``lean.nvim``. - * Install the normal `lean.vim `_. +Syntax highlighting and basic language support is included, for Lean 4 you can also +try the experimental support present via `tree-sitter-lean +`_ by installing +`nvim-treesitter `_ - * or try the experimental support present via `tree-sitter-lean - `_ by installing - `nvim-treesitter `_ - - Note that many simple syntactical things are not yet implemented - (help is of course welcome), and that ``tree-sitter-lean`` is lean - 4-only. +Note that many simple syntactical things are not yet implemented +(help is of course welcome), and that ``tree-sitter-lean`` is lean +4-only. Installation ------------ @@ -32,11 +33,12 @@ Install via your favorite plugin manager. E.g., with .. code-block:: vim Plug 'Julian/lean.nvim' - - Plug 'hrsh7th/nvim-compe' Plug 'leanprover/lean.vim' Plug 'neovim/nvim-lspconfig' + " Optional dependencies + Plug 'hrsh7th/nvim-compe' + For LSP support in Lean 3, you also first need to install ``lean-language-server``, which can be done via e.g.: @@ -64,9 +66,11 @@ Features * ``i``: toggle infoview - * ``s``: ``sorry`` insertion corresponding to the number of open goals + * ``pt``: set infoview per-tab mode - * ``3``: force a buffer into Lean 3 mode + * ``pw``: set infoview per-window mode + + * ``s``: ``sorry`` insertion corresponding to the number of open goals * A basic infoview which can show persistent goal, term & tactic state @@ -94,6 +98,17 @@ Configuration & Usage In e.g. your ``init.lua``: .. code-block:: lua + -- If you don't already have an existing LSP setup, you may want + -- to reference the keybindings section of the nvim-lspconfig + -- documentation, which can be found at: + -- https://github.com/neovim/nvim-lspconfig#keybindings-and-completion + on_attach = function(client, bufnr) + local function buf_set_keymap(...) vim.api.nvim_buf_set_keymap(bufnr, ...) end + local function buf_set_option(...) vim.api.nvim_buf_set_option(bufnr, ...) end + buf_set_keymap('n', 'gd', 'lua vim.lsp.buf.definition()', {noremap = true}) + buf_set_keymap('n', 'K', 'lua vim.lsp.buf.hover()', {noremap = true}) + buf_set_option('omnifunc', 'v:lua.vim.lsp.omnifunc') + end require('lean').setup{ -- Abbreviation support @@ -124,26 +139,20 @@ In e.g. your ``init.lua``: -- Clip the infoview to a maximum width max_width = 79, }, - -- Enable the Lean language server? + -- Enable the Lean3(lsp3)/Lean4(lsp) language servers? -- -- false to disable, otherwise should be a table of options to pass to -- `leanls`. See https://github.com/neovim/nvim-lspconfig/blob/master/CONFIG.md#leanls -- for details though lean-language-server actually doesn't support all -- the options mentioned there yet. - lsp = { - on_attach = function(client, bufnr) - -- If you don't already have an existing LSP setup, you - -- may want to reference the keybindings section of the - -- aforementioned nvim-lspconfig documentation, which - -- can be found at: - -- https://github.com/neovim/nvim-lspconfig#keybindings-and-completion - local function buf_set_keymap(...) vim.api.nvim_buf_set_keymap(bufnr, ...) end - local function buf_set_option(...) vim.api.nvim_buf_set_option(bufnr, ...) end - buf_set_keymap('n', 'gd', 'lua vim.lsp.buf.definition()', {noremap = true}) - buf_set_keymap('n', 'K', 'lua vim.lsp.buf.hover()', {noremap = true}) - buf_set_option('omnifunc', 'v:lua.vim.lsp.omnifunc') - end, + lsp3 = { + on_attach = on_attach, cmd = {"lean-language-server", "--stdio", '--', "-M", "4096"}, + }, + + lsp = { + on_attach = on_attach, + cmd = {"lean", "--server"}, } } diff --git a/ftdetect/lean.vim b/ftdetect/lean.vim index c28b0f25..4484be99 100644 --- a/ftdetect/lean.vim +++ b/ftdetect/lean.vim @@ -1 +1 @@ -autocmd BufRead,BufNewFile *.lean lua require'lean.lean3'.detect() +autocmd BufRead,BufNewFile *.lean lua require'lean.ft'.detect() diff --git a/ftplugin/lean/lean.vim b/ftplugin/lean/lean.vim new file mode 100644 index 00000000..cce11aa3 --- /dev/null +++ b/ftplugin/lean/lean.vim @@ -0,0 +1,30 @@ +if exists('b:did_ftplugin') + finish +endif +let b:did_ftplugin = 1 + +set wildignore+=*.olean + +setlocal iskeyword=@,48-57,_,-,!,#,$,% + +setlocal comments=s0:/-,mb:\ ,ex:-/,:-- +setlocal commentstring=/-\ %s\ -/ + +setlocal expandtab +setlocal shiftwidth=2 +setlocal softtabstop=2 + +function! lean#dotted2path(fname) + return substitute(a:fname, '\.', '/', 'g') . '.lean' +endfunction +setlocal includeexpr=lean#dotted2path(v:fname) + +setlocal matchpairs+=⟨:⟩ + +" Matchit support +if exists('loaded_matchit') && !exists('b:match_words') + let b:match_ignorecase = 0 + + let b:match_words = + \ ',\<\%(namespace\|section\)\s\+\(.\{-}\)\>:\' +endif diff --git a/ftplugin/lean/switch.vim b/ftplugin/lean/switch.vim index 91150a41..6f0d6569 100644 --- a/ftplugin/lean/switch.vim +++ b/ftplugin/lean/switch.vim @@ -8,11 +8,6 @@ endif let b:switch_definitions = [ \ g:switch_builtins.true_false, \ ["#check", "#eval", "#reduce"], - \ ['\(begin\n\s*\)\@:\:\' +endif diff --git a/ftplugin/lean3/switch.vim b/ftplugin/lean3/switch.vim new file mode 100644 index 00000000..91150a41 --- /dev/null +++ b/ftplugin/lean3/switch.vim @@ -0,0 +1,40 @@ +" This possibly belongs in lean.vim or switch.vim itself but putting it here +" for now. + +if !exists("g:loaded_switch") + finish +endif + +let b:switch_definitions = [ + \ g:switch_builtins.true_false, + \ ["#check", "#eval", "#reduce"], + \ ['\(begin\n\s*\)\@ max_width then + vim.api.nvim_win_set_width(infoview.window, max_width) + end + end +end + +-- physically close infoview, then erase it +local function close_win(src_idx) + if M._infoviews[src_idx] then + vim.api.nvim_win_close(M._infoviews[src_idx].window, true) + end + + M._infoviews_open[src_idx] = nil + M._infoviews[src_idx] = nil +end + +-- create autocmds under the specified group and local to +-- the given buffer; clears any existing autocmds +-- from the buffer beforehand +local function set_autocmds_guard(group, autocmds, bufnum) + local buffer_string = bufnum == 0 and "" + or string.format("", bufnum) + + vim.api.nvim_exec(string.format([[ + augroup %s + autocmd! %s * %s + %s + augroup END + ]], group, group, buffer_string, autocmds), false) +end + +function M.update() + local src_idx = get_idx() + + if M._infoviews_open[src_idx] == false then + return + end + + local infoview_bufnr + local infoview = M._infoviews[src_idx] + if not infoview then + M._infoviews[src_idx] = {} + + infoview_bufnr = vim.api.nvim_create_buf(false, true) + vim.api.nvim_buf_set_name(infoview_bufnr, _INFOVIEW_BUF_NAME .. infoview_bufnr) + for name, value in pairs(_DEFAULT_BUF_OPTIONS) do + vim.api.nvim_buf_set_option(infoview_bufnr, name, value) + end + + local current_window = vim.api.nvim_get_current_win() + local current_tab = vim.api.nvim_get_current_tabpage() + + if M._opts.one_per_tab then + vim.cmd "botright vsplit" + else + vim.cmd "rightbelow vsplit" + end + vim.cmd(string.format("buffer %d", infoview_bufnr)) + + local window = vim.api.nvim_get_current_win() + + for name, value in pairs(_DEFAULT_WIN_OPTIONS) do + vim.api.nvim_win_set_option(window, name, value) + end + -- This makes the infoview robust to manually being closed by the user + -- (though they technically shouldn't do this). + -- It makes sure that the infoview is erased from the table when this happens. + set_autocmds_guard("LeanInfoViewWindow", string.format([[ + autocmd WinClosed lua require'lean.infoview'.close_win_wrapper(%s, %s, true) + ]], current_window, current_tab), 0) + vim.api.nvim_set_current_win(current_window) + + M._infoviews[src_idx].buf = infoview_bufnr + M._infoviews[src_idx].window = window + + M._maybe_resize_infoviews() + + else + infoview_bufnr = infoview.buf + end + + local _update = lean3.is_lean3_project() and lean3.update_infoview or function(set_lines) local current_buffer = vim.api.nvim_get_current_buf() local cursor = vim.api.nvim_win_get_cursor(0) local params = vim.lsp.util.make_position_params() @@ -85,75 +174,125 @@ function M.update(infoview_bufnr) end function M.enable(opts) + if opts.one_per_tab == nil then opts.one_per_tab = true end M._opts = opts - vim.api.nvim_exec([[ - augroup LeanInfoViewOpen + + vim.api.nvim_exec(string.format([[ + augroup LeanInfoview autocmd! - autocmd BufWinEnter *.lean lua require'lean.infoview'.ensure_open() + autocmd WinEnter * lua require'lean.infoview'._maybe_resize_infoviews() + autocmd FileType lean3 lua require'lean.infoview'.set_update_autocmds() + autocmd FileType lean lua require'lean.infoview'.set_update_autocmds() + autocmd FileType lean3 lua require'lean.infoview'.set_closed_autocmds() + autocmd FileType lean lua require'lean.infoview'.set_closed_autocmds() augroup END - ]], false) + ]]), false) end -function M.is_open() return M._infoview ~= nil end +function M.set_update_autocmds() + -- guarding is necessary here because I noticed the FileType event being + -- triggered multiple times for a single file (not sure why) + set_autocmds_guard("LeanInfoViewUpdate", [[ + autocmd CursorHold lua require'lean.infoview'.update() + autocmd CursorHoldI lua require'lean.infoview'.update() + ]], 0) +end -function M.ensure_open() - if M.is_open() then return M._infoview.bufnr end +function M.set_closed_autocmds() + set_autocmds_guard("LeanInfoViewClose", [[ + autocmd QuitPre lua require'lean.infoview'.close_win_wrapper(-1, -1, false) + autocmd WinClosed ]] .. + [[lua require'lean.infoview'.close_win_wrapper(tonumber(vim.fn.expand('')), -1, false) + ]], 0) +end - local bufnr = vim.api.nvim_create_buf(false, true) - vim.api.nvim_buf_set_name(bufnr, _INFOVIEW_BUF_NAME) - for name, value in pairs(_DEFAULT_BUF_OPTIONS) do - vim.api.nvim_buf_set_option(bufnr, name, value) +function M.close_win_wrapper(src_winnr, src_tabnr, already_closed) + if src_winnr == -1 then + src_winnr = vim.api.nvim_get_current_win() end + if src_tabnr == -1 then + src_tabnr = vim.api.nvim_win_get_tabpage(src_winnr) + end + local src_idx = src_winnr + if M._opts.one_per_tab then + src_idx = src_tabnr - local current_window = vim.api.nvim_get_current_win() - - vim.cmd "botright vsplit" - vim.cmd(string.format("buffer %d", bufnr)) - - local window = vim.api.nvim_get_current_win() - - for name, value in pairs(_DEFAULT_WIN_OPTIONS) do - vim.api.nvim_win_set_option(window, name, value) + if not already_closed then + -- do not close infoview if there are remaining lean files + -- in the tab + for _, win in pairs(vim.api.nvim_tabpage_list_wins(src_idx)) do + if win == src_winnr then goto continue end + local buf = vim.api.nvim_win_get_buf(win) + local ft = vim.api.nvim_buf_get_option(buf, "filetype") + if ft == "lean3" or ft == "lean" then return end + ::continue:: + end + end end - vim.api.nvim_set_current_win(current_window) - local max_width = M._opts.max_width or 79 - if vim.api.nvim_win_get_width(window) > max_width then - vim.api.nvim_win_set_width(window, max_width) + if not already_closed then + -- this check is needed since apparently WinClosed can be triggered + -- multiple times for a single window close? + if M._infoviews[src_idx] ~= nil then + -- remove these autocmds so the infoview can now be closed manually without issue + set_autocmds_guard("LeanInfoViewWindow", "", M._infoviews[src_idx].buf) + end end - vim.api.nvim_exec(string.format([[ - augroup LeanInfoViewUpdate - autocmd! - autocmd CursorHold *.lean lua require'lean.infoview'.update(%d) - autocmd CursorHoldI *.lean lua require'lean.infoview'.update(%d) - augroup END - ]], bufnr, bufnr), false) + close_win(src_idx) +end - M._infoview = { bufnr = bufnr, window = window } - return M._infoview +function M.is_open() + return M._infoviews_open[get_idx()] ~= false end -M.open = M.ensure_open +function M.open() + local src_idx = get_idx() + M._infoviews_open[src_idx] = true + return M._infoviews[src_idx] +end -function M.close() - if not M.is_open() then return end +function M.set_pertab() + if M._opts.one_per_tab then return end - local infoview = M._infoview - M._infoview = nil + M.close_all() - vim.api.nvim_exec([[ - augroup LeanInfoViewOpen - autocmd! - augroup END + M._opts.one_per_tab = true +end - augroup LeanInfoViewUpdate - autocmd! - augroup END - ]], false) +function M.set_perwindow() + if not M._opts.one_per_tab then return end + M.close_all() + + M._opts.one_per_tab = false +end + +function M.close_all() + for key, _ in pairs(M._infoviews) do + close_win(key) + end + for key, _ in pairs(M._infoviews_open) do + M._infoviews_open[key] = nil + end +end + +-- Close the infoview associated with the current window. +function M.close() + if not M.is_open() then return end + local src_idx = get_idx() + local infoview = M._teardown(src_idx) vim.api.nvim_win_close(infoview.window, true) - vim.api.nvim_buf_delete(infoview.bufnr, { force = true }) + M._infoviews_open[src_idx] = false +end + +-- Teardown internal state for an infoview window. +function M._teardown(infoview_idx) + local infoview = M._infoviews[infoview_idx] + M._infoviews_open[infoview_idx] = nil + M._infoviews[infoview_idx] = nil + + return infoview end function M.toggle() diff --git a/lua/lean/init.lua b/lua/lean/init.lua index b4dc31b0..9fa6ecb1 100644 --- a/lua/lean/init.lua +++ b/lua/lean/init.lua @@ -6,6 +6,8 @@ local lean = { n = { ["i"] = "lua require('lean.infoview').toggle()"; ["s"] = "lua require('lean.sorry').fill()"; + ["pt"] = "lua require('lean.infoview').set_pertab()"; + ["pw"] = "lua require('lean.infoview').set_perwindow()"; ["t"] = "lua require('lean.trythis').swap()"; ["3"] = "lua require('lean.lean3').init()"; }; @@ -20,18 +22,42 @@ function lean.setup(opts) local abbreviations = opts.abbreviations or {} if abbreviations.enable ~= false then lean.abbreviations.enable(abbreviations) end + local treesitter = opts.treesitter or {} + if treesitter.enable ~= false then require('lean.treesitter').enable(treesitter) end + local infoview = opts.infoview or {} - if infoview.enable ~= false then require('lean.infoview').enable(infoview) end + if infoview.enable ~= false then + require('lean.infoview').enable(infoview) + opts.commands = vim.tbl_extend("keep", opts.commands or {}, { + LeanInfoPerTab = { + function () + require('lean.infoview').set_pertab() + end; + description = "Set one infoview per tab." + }; + LeanInfoPerWin = { + function () + require('lean.infoview').set_perwindow() + end; + description = "Set one infoview per window." + }; + }) + end - local lsp = opts.lsp or {} - if lsp.enable ~= false then lean.lsp.enable(lsp) end + local function set_cmds(lsp_opts) + lsp_opts.commands = vim.tbl_extend("keep", lsp_opts.commands or {}, opts.commands or {}) + end - local treesitter = opts.treesitter or {} - if treesitter.enable ~= false then require('lean.treesitter').enable(treesitter) end + local lsp3 = opts.lsp3 or {} + if lsp3.enable ~= false then set_cmds(lsp3) require'lean.lean3'.lsp.enable(lsp3) end + + local lsp = opts.lsp or {} + if lsp.enable ~= false then set_cmds(lsp) lean.lsp.enable(lsp) end if opts.mappings == true then vim.api.nvim_exec([[ autocmd FileType lean lua require'lean'.use_suggested_mappings(true) + autocmd FileType lean3 lua require'lean'.use_suggested_mappings(true) ]], false) end end diff --git a/lua/lean/lean3.lua b/lua/lean/lean3.lua index a297bf5f..fff97844 100644 --- a/lua/lean/lean3.lua +++ b/lua/lean/lean3.lua @@ -1,27 +1,18 @@ -local M = {} +local lspconfig = require('lspconfig') +local M = {lsp = {}} --- Ideally this obviously would use a TOML parser but yeah choosing to --- do nasty things and not add the dependency for now. Also there's no --- project root searching being done, maybe there should be. -local _MARKER = '.*lean_version.*\".*:3.*' +function M.lsp.enable(opts) + -- REMOVEME: We can do this unconditionally once neovim/nvim-lspconfig#958 is merged + if lspconfig.lean3ls then lspconfig.lean3ls.setup(opts) end +end function M.init() pcall(vim.cmd, 'TSBufDisable highlight') -- tree-sitter-lean is lean4-only - vim.b.lean3 = true -end - -function M.is_lean3_project(default) - default = default or false - local exists, result = pcall(vim.fn.readfile, "leanpkg.toml") - if not exists then return default end - for _, line in ipairs(result) do - if line:match(_MARKER) then return true end - end - return false + vim.bo.ft = "lean3" end -function M.detect() - if M.is_lean3_project() then M.init() end +function M.is_lean3_project() + return vim.bo.ft == "lean3" end function M.update_infoview(set_lines) diff --git a/lua/tests/helpers.lua b/lua/tests/helpers.lua index f8c5530d..ef77b45f 100644 --- a/lua/tests/helpers.lua +++ b/lua/tests/helpers.lua @@ -1,7 +1,5 @@ local assert = require('luassert') -local infoview = require('lean.infoview') - local api = vim.api local helpers = {_clean_buffer_counter = 1} @@ -23,7 +21,7 @@ end local function set_unique_name_so_we_always_have_a_separate_fake_file(bufnr) local counter = helpers._clean_buffer_counter helpers._clean_buffer_counter = helpers._clean_buffer_counter + 1 - local unique_name = string.format('unittest-%d.lean', counter) + local unique_name = string.format('unittest-%d', counter) api.nvim_buf_set_name(bufnr, unique_name) end @@ -36,34 +34,28 @@ function helpers.clean_buffer(contents, callback) return function() local bufnr = vim.api.nvim_create_buf(false, true) set_unique_name_so_we_always_have_a_separate_fake_file(bufnr) - api.nvim_buf_set_option(bufnr, 'filetype', 'lean') + + -- FIXME: For now all tests are against Lean 3 + api.nvim_buf_set_option(bufnr, 'filetype', 'lean3') api.nvim_buf_call(bufnr, function() - -- FIXME: For now all tests are against Lean 3 - require 'lean.lean3'.init() - local succeeded, _ = vim.wait(1000, vim.lsp.buf.server_ready) + local succeeded, _ = vim.wait(5000, vim.lsp.buf.server_ready) assert.message("LSP server was never ready.").True(succeeded) api.nvim_buf_set_lines(bufnr, 0, -1, false, vim.split(contents, '\n')) - local infoview_info = infoview.open() callback{ source_file = { bufnr = bufnr }, - infoview = { - bufnr = infoview_info.bufnr, - window = infoview_info.window, - }, } end) - infoview.close() vim.api.nvim_buf_delete(bufnr, { force = true }) end end --- Wait a few seconds for line diagnostics, erroring if none arrive. function helpers.wait_for_line_diagnostics() - local succeeded, _ = vim.wait(2000, function() + local succeeded, _ = vim.wait(5000, function() return not vim.tbl_isempty(vim.lsp.diagnostic.get_line_diagnostics()) end) assert.message("Waited for line diagnostics but none came.").True(succeeded) diff --git a/lua/tests/infoview_spec.lua b/lua/tests/infoview_spec.lua index ece9cfb1..06e93fe0 100644 --- a/lua/tests/infoview_spec.lua +++ b/lua/tests/infoview_spec.lua @@ -1,9 +1,17 @@ +local infoview = require('lean.infoview') + local clean_buffer = require('tests.helpers').clean_buffer describe('infoview', function() it('starts with the window position at the top', clean_buffer('', - function(context) - local cursor = vim.api.nvim_win_get_cursor(context.infoview.window) + function(_) + infoview.update() + local succeeded_info, _ = vim.wait(5000, infoview.open) + assert.message("Infoview was never ready.").True(succeeded_info) + local infoview_info = infoview.open() + + local cursor = vim.api.nvim_win_get_cursor(infoview_info.window) assert.is.same(1, cursor[1]) + infoview.close() end)) end) diff --git a/scripts/minimal_init.lua b/scripts/minimal_init.lua index 76663b88..b10d6fd5 100644 --- a/scripts/minimal_init.lua +++ b/scripts/minimal_init.lua @@ -7,8 +7,6 @@ local packpath = lean_nvim_dir .. '/packpath/*' vim.o.runtimepath = vim.o.runtimepath .. ',' .. packpath .. ',' .. lean_nvim_dir vim.api.nvim_exec([[ - autocmd BufNewFile,BufRead *.lean setlocal filetype=lean - runtime! plugin/lspconfig.vim runtime! plugin/plenary.vim ]], false) diff --git a/syntax/lean.vim b/syntax/lean.vim new file mode 100644 index 00000000..30089df1 --- /dev/null +++ b/syntax/lean.vim @@ -0,0 +1,113 @@ +" Vim syntax file +" Language: Lean +" Filename extensions: *.lean +" Maintainer: Gabriel Ebner + +syn case match + +" keywords + +syn keyword leanCommand prelude import include omit export open mutual +syn keyword leanCommandPrefix local private protected scoped partial noncomputable meta unsafe +syn keyword leanModifier renaming hiding where extends using with at rec deriving +syn keyword leanCommand syntax elab macro_rules macro + +syn keyword leanCommand namespace section + +syn match leanFrenchQuote '«[^»]*»' + +syn match leanDeclarationName ' *[^:({\[[:space:]]*' contained +syn match leanDeclarationName ' *«[^»]*»' contained +syn keyword leanDeclaration lemma theorem def definition axiom axioms constant abbrev abbreviation + \ inductive coinductive structure class instance skipwhite nextgroup=leanDeclarationName + +syn keyword leanCommand universe universes example axioms constants +syn keyword leanCommand meta parameter parameters variable variables +syn keyword leanCommand reserve precedence postfix prefix notation infix infixl infixr + +syn keyword leanKeyword by +syn keyword leanKeyword forall fun Pi from have show assume suffices let if else then in with calc match do this +syn keyword leanKeyword try catch finally for unless return mut continue break +syn keyword leanKeyword Sort Prop Type +syn keyword leanCommand set_option run_cmd +syn match leanCommand "#eval" +syn match leanCommand "#check" +syn match leanCommand "#print" + +syn keyword leanSorry sorry +syn match leanSorry "#exit" + +syn region leanAttributeArgs start='\[' end='\]' contained keepend contains=leanString,leanNumber +syn match leanCommandPrefix '@' nextgroup=leanAttributeArgs +syn keyword leanCommandPrefix attribute skipwhite nextgroup=leanAttributeArgs + +" constants +syn match leanOp "[:=><λ←→↔∀∃∧∨¬≤≥▸·+*-/;$|&%!×]" + +" delimiters +syn region leanEncl matchgroup=leanDelim start="#\[" end="\]" contains=TOP +syn region leanEncl matchgroup=leanDelim start="(" end=")" contains=TOP +syn region leanEncl matchgroup=leanDelim start="\[" end="\]" contains=TOP +syn region leanEncl matchgroup=leanDelim start="{" end="}" contains=TOP +syn region leanEncl matchgroup=leanDelim start="⦃" end="⦄" contains=TOP +syn region leanEncl matchgroup=leanDelim start="⟨" end="⟩" contains=TOP + +" FIXME(gabriel): distinguish backquotes in notations from names +" syn region leanNotation start=+`+ end=+`+ + +syn keyword leanTodo containedin=leanComment TODO FIXME BUG FIX + +syn match leanStringEscape '\\.' contained +syn region leanString start='"' end='"' contains=leanInterpolation,leanStringEscape +syn region leanInterpolation contained start='{' end='}' contains=TOP keepend + +syn match leanChar "'[^\\]'" +syn match leanChar "'\\.'" + +syn match leanNumber '\<\d\d*\>' +syn match leanNumber '\<0x[0-9a-fA-F]*\>' +syn match leanNumber '\<\d\d*\.\d*\>' + +syn match leanNameLiteral '``*[^ \[()\]}][^ ()\[\]{}]*' + +" syn include @markdown syntax/markdown.vim +syn region leanBlockComment start="/-" end="-/" contains=@markdown,@Spell,leanBlockComment +syn match leanComment "--.*" contains=@Spell +" fix up some highlighting links for markdown +hi! link markdownCodeBlock Comment +hi! link markdownError Comment + +if exists('b:current_syntax') + unlet b:current_syntax +endif + +hi def link leanReference Identifier +hi def link leanTodo Todo + +hi def link leanComment Comment +hi def link leanBlockComment leanComment + +hi def link leanKeyword Keyword +hi def link leanCommand leanKeyword +hi def link leanCommandPrefix PreProc +hi def link leanAttributeArgs leanCommandPrefix +hi def link leanModifier Label + +hi def link leanDeclaration leanCommand +hi def link leanDeclarationName Function + +hi def link leanDelim Delimiter +hi def link leanOp Operator + +hi def link leanNotation String +hi def link leanString String +hi def link leanStringEscape SpecialChar +hi def link leanChar Character +hi def link leanNumber Number +hi def link leanNameLiteral Identifier + +hi def link leanSorry Error + +let b:current_syntax = "lean" + +" vim: ts=8 sw=8 diff --git a/syntax/lean3.vim b/syntax/lean3.vim new file mode 100644 index 00000000..6160e3a6 --- /dev/null +++ b/syntax/lean3.vim @@ -0,0 +1,113 @@ +" Vim syntax file +" Language: Lean +" Filename extensions: *.lean +" Maintainer: Gabriel Ebner + +syn case match + +" keywords + +syn keyword leanCommand prelude import include omit export open mutual +syn keyword leanCommandPrefix local private protected scoped partial noncomputable meta unsafe +syn keyword leanModifier renaming hiding where extends using with at rec deriving +syn keyword leanCommand syntax elab macro_rules macro + +syn keyword leanCommand namespace section + +syn match leanFrenchQuote '«[^»]*»' + +syn match leanDeclarationName ' *[^:({\[[:space:]]*' contained +syn match leanDeclarationName ' *«[^»]*»' contained +syn keyword leanDeclaration lemma theorem def definition axiom axioms constant abbrev abbreviation + \ inductive coinductive structure class instance skipwhite nextgroup=leanDeclarationName + +syn keyword leanCommand universe universes example axioms constants +syn keyword leanCommand meta parameter parameters variable variables +syn keyword leanCommand reserve precedence postfix prefix notation infix infixl infixr + +syn keyword leanKeyword begin by end +syn keyword leanKeyword forall fun Pi from have show assume suffices let if else then in with calc match do this +syn keyword leanKeyword try catch finally for unless return mut continue break +syn keyword leanKeyword Sort Prop Type +syn keyword leanCommand set_option run_cmd +syn match leanCommand "#eval" +syn match leanCommand "#check" +syn match leanCommand "#print" + +syn keyword leanSorry sorry +syn match leanSorry "#exit" + +syn region leanAttributeArgs start='\[' end='\]' contained keepend contains=leanString,leanNumber +syn match leanCommandPrefix '@' nextgroup=leanAttributeArgs +syn keyword leanCommandPrefix attribute skipwhite nextgroup=leanAttributeArgs + +" constants +syn match leanOp "[:=><λ←→↔∀∃∧∨¬≤≥▸·+*-/;$|&%!×]" + +" delimiters +syn region leanEncl matchgroup=leanDelim start="#\[" end="\]" contains=TOP +syn region leanEncl matchgroup=leanDelim start="(" end=")" contains=TOP +syn region leanEncl matchgroup=leanDelim start="\[" end="\]" contains=TOP +syn region leanEncl matchgroup=leanDelim start="{" end="}" contains=TOP +syn region leanEncl matchgroup=leanDelim start="⦃" end="⦄" contains=TOP +syn region leanEncl matchgroup=leanDelim start="⟨" end="⟩" contains=TOP + +" FIXME(gabriel): distinguish backquotes in notations from names +" syn region leanNotation start=+`+ end=+`+ + +syn keyword leanTodo containedin=leanComment TODO FIXME BUG FIX + +syn match leanStringEscape '\\.' contained +syn region leanString start='"' end='"' contains=leanInterpolation,leanStringEscape +syn region leanInterpolation contained start='{' end='}' contains=TOP keepend + +syn match leanChar "'[^\\]'" +syn match leanChar "'\\.'" + +syn match leanNumber '\<\d\d*\>' +syn match leanNumber '\<0x[0-9a-fA-F]*\>' +syn match leanNumber '\<\d\d*\.\d*\>' + +syn match leanNameLiteral '``*[^ \[()\]}][^ ()\[\]{}]*' + +" syn include @markdown syntax/markdown.vim +syn region leanBlockComment start="/-" end="-/" contains=@markdown,@Spell,leanBlockComment +syn match leanComment "--.*" contains=@Spell +" fix up some highlighting links for markdown +hi! link markdownCodeBlock Comment +hi! link markdownError Comment + +if exists('b:current_syntax') + unlet b:current_syntax +endif + +hi def link leanReference Identifier +hi def link leanTodo Todo + +hi def link leanComment Comment +hi def link leanBlockComment leanComment + +hi def link leanKeyword Keyword +hi def link leanCommand leanKeyword +hi def link leanCommandPrefix PreProc +hi def link leanAttributeArgs leanCommandPrefix +hi def link leanModifier Label + +hi def link leanDeclaration leanCommand +hi def link leanDeclarationName Function + +hi def link leanDelim Delimiter +hi def link leanOp Operator + +hi def link leanNotation String +hi def link leanString String +hi def link leanStringEscape SpecialChar +hi def link leanChar Character +hi def link leanNumber Number +hi def link leanNameLiteral Identifier + +hi def link leanSorry Error + +let b:current_syntax = "lean" + +" vim: ts=8 sw=8