lsp gains hover, definition and completion from a text-level symbol scan

1 files changed, 25 insertions, 9 deletions

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,