feat: redo keyword highlighting

Now keywords don't show their parser names, and they participate in
occurrence highlighting

Fixes #14

Author: david-christiansen

examples/website/DemoSite/Blog/Conditionals.lean

@@ -90,6 +90,19 @@ def squish'' (n : Option Nat) : Nat :=
 
 ```
 
+Here is a mutual block:
+```lean demo
+mutual
+  def f : Nat → Nat
+    | 0 => 1
+    | n + 1 => g n
+
+  def g : Nat → Nat
+    | 0 => 0
+    | n + 1 => f n
+end
+```
+
 Here is a proof with some lambdas and big terms in it, to check highlighting:
 ```lean demo
 def grow : Nat → α → α

src/verso-blog/Verso/Genre/Blog/HighlightCode.lean

@@ -17,7 +17,7 @@ partial defmethod Highlighted.Token.Kind.priority : Highlighted.Token.Kind → N
   | .const .. => 5
   | .option .. => 4
   | .sort => 4
-  | .keyword _ _ => 3
+  | .keyword _ _ _ => 3
   | .docComment => 1
   | .unknown => 0
 
@@ -417,12 +417,12 @@ partial def renderTagged [Monad m] [MonadLiftT IO m] [MonadMCtx m] [MonadEnv m]
     let mut toks : Array Highlighted := #[]
     let mut current := ""
     while !todo.isEmpty do
-      for kw in ["let", "fun", ":=", "=>", "do", "match", "with", "if", "then", "else", "break", "continue", "for", "in", "mut"] do
+      for kw in ["let", "fun", "do", "match", "with", "if", "then", "else", "break", "continue", "for", "in", "mut"] do
         if kw.isPrefixOf todo && tokenEnder (todo.drop kw.length) then
           if !current.isEmpty then
             toks := toks.push <| .text current
             current := ""
-          toks := toks.push <| .token ⟨.keyword none none, kw⟩
+          toks := toks.push <| .token ⟨.keyword none none none, kw⟩
           todo := todo.drop kw.length
           break
       let c := todo.get 0
@@ -521,7 +521,7 @@ def findTactics (ids : HashMap Lsp.RefIdent Lsp.RefIdent) (stx : Syntax) : Highl
           }
         return
 
-partial def highlight' (ids : HashMap Lsp.RefIdent Lsp.RefIdent) (stx : Syntax) (lookingAt : Option Name := none) : HighlightM Unit := do
+partial def highlight' (ids : HashMap Lsp.RefIdent Lsp.RefIdent) (stx : Syntax) (lookingAt : Option (Name × String.Pos) := none) : HighlightM Unit := do
   findTactics ids stx
   match stx with
   | `($e.%$tk$field:ident) =>
@@ -550,7 +550,9 @@ partial def highlight' (ids : HashMap Lsp.RefIdent Lsp.RefIdent) (stx : Syntax)
     | stx@(.atom i x) =>
       let docs ← match lookingAt with
         | none => pure none
-        | some n => findDocString? (← getEnv) n
+        | some (n, _) => findDocString? (← getEnv) n
+      let name := lookingAt.map (·.1)
+      let occ := lookingAt.map fun (n, pos) => s!"{n}-{pos}"
       if let .sort ← identKind ids ⟨stx⟩ then
         emitToken i ⟨.sort, x⟩
         return
@@ -560,11 +562,11 @@ partial def highlight' (ids : HashMap Lsp.RefIdent Lsp.RefIdent) (stx : Syntax)
         | some '#' =>
           match x.get? ((0 : String.Pos) + '#') with
           | some c =>
-            if c.isAlpha then .keyword lookingAt docs
+            if c.isAlpha then .keyword name occ docs
             else .unknown
           | _ => .unknown
         | some c =>
-          if c.isAlpha then .keyword lookingAt docs
+          if c.isAlpha then .keyword name occ docs
           else .unknown
         | _ => .unknown
     | .node _ `str #[.atom i string] =>
@@ -586,9 +588,10 @@ partial def highlight' (ids : HashMap Lsp.RefIdent Lsp.RefIdent) (stx : Syntax)
       | _, _ =>
         highlight' ids dot
         highlight' ids name
-    | .node _ k children =>
+    | stx@(.node _ k children) =>
+      let pos := stx.getPos?
       for child in children do
-        highlight' ids child (lookingAt := some k)
+        highlight' ids child (lookingAt := pos.map (k, ·))
 
 def highlight (stx : Syntax) (messages : Array Message) : TermElabM Highlighted := do
   let modrefs := Lean.Server.findModuleRefs (← getFileMap) (← getInfoTrees).toArray

src/verso-blog/Verso/Genre/Blog/Highlighted.lean

@@ -8,7 +8,8 @@ deriving instance Repr for Std.Format.FlattenBehavior
 deriving instance Repr for Std.Format
 
 inductive Highlighted.Token.Kind where
-  | keyword (name : Option Name) (docs : Option String)
+  | /-- `occurrence` is a unique identifier that unites the various keyword tokens from a given production -/
+    keyword (name : Option Name) (occurrence : Option String) (docs : Option String)
   | const (name : Name) (signature : String) (docs : Option String)
   | var (name : FVarId) (type : String)
   | str (string : String)
@@ -22,7 +23,7 @@ open Highlighted.Token.Kind in
 open Syntax (mkCApp) in
 instance : Quote Highlighted.Token.Kind where
   quote
-    | .keyword n docs => mkCApp ``keyword #[quote n, quote docs]
+    | .keyword n occ docs => mkCApp ``keyword #[quote n, quote occ, quote docs]
     | .const n sig docs => mkCApp ``const #[quote n, quote sig, quote docs]
     | .option n docs => mkCApp ``option #[quote n, quote docs]
     | .var (.mk n) type => mkCApp ``var #[mkCApp ``FVarId.mk #[quote n], quote type]

src/verso-blog/Verso/Genre/Blog/Template.lean

@@ -46,13 +46,14 @@ defmethod Highlighted.Token.Kind.«class» : Highlighted.Token.Kind → String
   | .const _ _ _ => "const"
   | .option _ _ => "option"
   | .docComment => "doc-comment"
-  | .keyword _ _ => "keyword"
+  | .keyword _ _ _ => "keyword"
   | .unknown => "unknown"
 
 defmethod Highlighted.Token.Kind.data : Highlighted.Token.Kind → String
   | .const n _ _ => "const-" ++ toString n
   | .var ⟨v⟩ _ => "var-" ++ toString v
   | .option n _ => "option-" ++ toString n
+  | .keyword _ (some occ) _ => "kw-occ-" ++ toString occ
   | _ => ""
 
 
@@ -66,11 +67,13 @@ defmethod Highlighted.Token.Kind.hover? : (tok : Highlighted.Token.Kind) → Opt
       | none => .empty
       | some txt => {{<hr/><pre class="docstring">{{txt}}</pre>}}
     some <| hover {{ <code>{{sig}}</code> {{docs}} }}
-  | .option n doc | .keyword (some n) doc =>
+  | .option n doc =>
     let docs := match doc with
       | none => .empty
       | some txt => {{<hr/><pre class="docstring">{{txt}}</pre>}}
     some <| hover {{ <code>{{toString n}}</code> {{docs}} }}
+  | .keyword _ _ none => none
+  | .keyword _ _ (some doc) => some <| hover {{<pre class="docstring">{{doc}}</pre>}}
   | .var _ type =>
     some <| hover {{ <code>{{type}}</code> }}
   | .str s =>