stelf.nvim

Neovim support for STELF — the System for Totality in the Edinburgh Logical Framework.

• Tree-sitter syntax highlighting via tree-sitter-stelf
• Filetype detection for .stelf, .elf, .lf, .slf
• Prose injections for STELF's literate mode (markdown, LaTeX, Typst, HTML, and more)
• Locals (binder scopes) and comment settings

Requirements

• Neovim 0.11+ (0.12 recommended)
• nvim-treesitter on the main branch. The master branch has neither the parsers.<lang> = {...} registration API nor the User TSUpdate event this plugin hooks, so it will not work there.

No tree-sitter CLI is needed: the grammar repo commits a pre-generated src/parser.c at ABI 15.

Install

With lazy.nvim:

{ 'standardocaml/stelf.nvim', lazy = false }

Then run :TSInstall stelf once.

lazy = false is deliberate. The plugin has to register the parser before nvim-treesitter reads its parser table, which can happen from any buffer (e.g. when you run :TSInstall stelf from somewhere else), so ft = { 'stelf' } would be too late.

There is intentionally no dependencies entry for nvim-treesitter — adding one would force it to load eagerly and defeat its own lazy spec. This plugin never requires nvim-treesitter at startup; it only touches it from inside the User TSUpdate autocmd, which nvim-treesitter itself fires.

Optional: prose injections

STELF's literate mode lets the text between commands be prose in a language chosen by the %prose header. Injections are wired up for markdown, latex, typst, html, rst, rtf, javadoc, jsdoc, doxygen, org and asciidoc. Install only the ones you use:

:TSInstall markdown markdown_inline latex

Missing parsers are silently skipped — nothing breaks if you install none.

If .elf conflicts

.elf is also the conventional extension for ELF binaries. Neovim has no builtin mapping for it, so this plugin claims it — but if something else in your config maps .elf, drop it:

vim.filetype.add({ extension = { elf = nil } })

Optional: claiming .thm

tree-sitter.json in the grammar lists .thm as a STELF extension, but Neovim already maps it to tex, and LaTeX theorem files are the more common meaning. This plugin leaves that mapping alone. To override it:

vim.filetype.add({ extension = { thm = 'stelf' } })

Notes for maintainers

:checkhealth nvim-treesitter shows stelf with no columns

Expected, and not a fault in this plugin. The healthcheck reads nvim-treesitter's parser table via config.get_installed(), which — unlike get_available() — does not fire User TSUpdate first, so the externally-registered stelf entry isn't there yet and the query columns are skipped. Fire it yourself to see the real result:

:lua vim.api.nvim_exec_autocmds('User', { pattern = 'TSUpdate' })
:checkhealth nvim-treesitter

which reports stelf ✓ ✓ . . ✓ — highlights, locals and injections present; folds and indents deliberately absent (see below).

The queries live here, not in the grammar repo

install_info deliberately omits the queries field, so nvim-treesitter installs no queries for stelf and queries/stelf/ in this plugin is the only copy on the runtimepath. Adding a queries entry would put a second copy in nvim-treesitter's install directory, and vim.treesitter.query.get would silently pick whichever came first on rtp.

To check there is exactly one:

:lua vim.print(vim.treesitter.query.get_files('stelf', 'highlights'))

These queries are not copies of the grammar repo's

The grammar's queries/ target Zed / tree-sitter-highlight. Two differences matter and are load-bearing; both are documented at the top of the files here.

highlights.scm — capture precedence is reversed. tree-sitter-highlight keeps the first matching capture per node; Neovim keeps the last. The grammar's file therefore runs most-specific → generic, and copying it verbatim makes every identifier resolve to @constructor. This plugin's copy runs generic → most-specific. Two orderings inside the identifier block are load-bearing: metavariables must come before the binder rules (so a bound X stays @variable.parameter), and term_cmd must come after the bare (decl args:) rule.

injections.scm — no injection.combined. Combining the prose regions into one document makes markdown nodes span the gaps between them, so a ## heading paints the following %sort line as a heading. Each region is parsed on its own instead.

gc uses %;, not %

STELF's canonical line comment is % (percent + whitespace), but commentstring = '% %s' is unsafe in Neovim: the builtin commenting matches the left part with its trailing whitespace made optional, so it reads every %command line as already commented and gcc on %sort nat %. strips the %. The ftplugin uses %; — an equally valid opener in the grammar's comment rule — which cannot prefix a command keyword and round-trips correctly.

Updating the grammar

revision in plugin/stelf.lua is pinned to a commit. Bump it (and the tree-sitter-stelf submodule) together; nvim-treesitter compares the stored revision against it to decide whether to rebuild, so 'HEAD' would mean the parser never updates.

If the parser ABI ever drifts ahead of what the committed parser.c provides, add generate = true to install_info — that regenerates from grammar.json at install time, at the cost of requiring the tree-sitter CLI.

What is not shipped

The grammar's indents.scm and brackets.scm use Zed/Helix captures (@indent / @end); Neovim wants @indent.begin / @indent.end, so porting them is a rewrite rather than a copy. outline.scm has no Neovim equivalent. None of them are included.

The grammar's test/highlight-snapshots/*.hl do not validate these queries — they record every capture rather than resolving precedence, and are generated with first-wins semantics.