From 19ba625e0345a88da6c29ab91a3ba2d7a8462065 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sun, 12 Jul 2026 18:43:23 -0300 Subject: lsp gains hover, definition and completion from a text-level symbol scan --- docs/tooling.org | 34 +++++++++++++++++++++++++--------- 1 file changed, 25 insertions(+), 9 deletions(-) (limited to 'docs') diff --git a/docs/tooling.org b/docs/tooling.org index 7fb0e8c..e09917e 100644 --- a/docs/tooling.org +++ b/docs/tooling.org @@ -9,15 +9,31 @@ the checker the runtime runs. * The language server -=sol lsp= speaks the Language Server Protocol over stdio. It has one -capability, the load bearing one: diagnostics. On every open and -every change the document goes through the same parse and the same -admission the loader performs, so a recursive rule without a -decrease witness, a fact violating its schema, an unknown relation -or a failed membership criterion appears in the editor at typing -time, with the same message the runtime would give. Parse errors -carry line and column; admission errors anchor at the top of the -file until the loader learns source locations. +=sol lsp= speaks the Language Server Protocol over stdio. Four +capabilities: + +- diagnostics :: on every open and change the document goes through + the same parse and the same admission the loader performs, so a + recursive rule without a decrease witness, a fact violating its + schema, an unknown relation or a failed membership criterion + appears in the editor at typing time, with the runtime's own + message. Parse errors carry line and column; admission errors + anchor at the top of the file until the loader learns source + locations. +- hover :: a builtin shows its signature and operational meaning + (what solves backward, what residuates, what generates); a + declared relation shows its defining source lines, verbatim, + which is the honest notion of type in a language where types are + relations. +- definition :: jumping from a use site to the Relation directive + or the rule heads that define the name. +- completion :: declared relations, builtins and quantifier forms, + every label spelled in the document, directives, and the + combinators, triggered on =[=, =#= and =:=. + +Hover, definition and completion work from a per-line symbol scan of +the stored text, deliberately not from the parsed program, so they +keep working while the buffer is broken mid edit. The server is hand rolled JSON-RPC on yojson, in =bin/lsp.ml=. It answers =initialize=, tracks documents through full-content sync, -- cgit v1.2.3