Code actions for typed holes and incomplete matches

The language server can fill a hole with what fits it and add the
clauses a match lacks; the sections on typed holes and exhaustiveness
say so.

🤖 Generated with [ECA](https://eca.dev)

Co-Authored-By: eca-agent <git@eca.dev>

_01.Language-basics.sz

@@ -185,6 +185,8 @@ The bindings closest to the hole are listed first: locals, then your own module'
 
 While a hole's type is still open, the other errors in the same definition are held back, since they are often caused by the hole. Once you fill it in, they show up.
 
+In an editor that uses the Bjolang language server, a hole has code actions: fill it with one of the bindings that fit, with a constructor of its type such as @code{(Circle _)}, or, where a function is wanted, with @code{(fun (x y) _)}. What you fill in can have holes of its own, so you can build an expression a step at a time and let the compiler tell you what each part has to be.
+
 @subsubsection{Unused definitions}
 
 The compiler warns about definitions nothing uses: a top-level @code{def} or @code{defun} that the module doesn't export and nothing in it reads, and a local binding (a @code{let}, a @code{def} in a body, a loop variable) that nothing in its scope reads. Dead code piles up quietly in a large program, and this keeps it from doing so.
@@ -977,6 +979,8 @@ The counterexample is a real value, and for nested patterns it tells you exactly
 Pattern Error at cards.bjo:8: this match does not cover every value. (Card (rank Ace) (suit Clubs)) reaches no clause.
 }|
 
+In an editor that uses the Bjolang language server, an incomplete match has a code action that adds the clauses it lacks, nested cases spelled out, each with a typed hole as its body: @code{((Square _) _)}.
+
 A clause that can never run, because the clauses above it already match everything it would, is also an error:
 
 @codeblock[#:lang "text"]|{