fix: stop rendering doc comments as keywords

examples/website/DemoSite/Blog/Conditionals.lean

@@ -22,3 +22,10 @@ example := if true then 1 else 2
 example := if True then 1 else 2
 example : Int := if True then 1 else 2
 ```
+
+```lean demo
+/-- A recursive function -/
+def slowId : Nat → Nat
+  | 0 => 0
+  | n + 1 => slowId n + 1
+```

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

@@ -12,6 +12,7 @@ partial defmethod Highlighted.Token.Kind.priority : Highlighted.Token.Kind → N
   | .const .. => 5
   | .sort => 4
   | .keyword _ _ => 3
+  | .docComment => 1
   | .unknown => 0
 
 -- Find all info nodes whose canonical span matches the given syntax
@@ -344,6 +345,12 @@ partial def highlight' (ids : HashMap Lsp.RefIdent Lsp.RefIdent) (stx : Syntax)
           if c.isAlpha then .keyword lookingAt docs
           else .unknown
         | _ => .unknown
+    | .node _ ``Lean.Parser.Command.docComment #[.atom i1 opener, .atom i2 body] =>
+      if let .original leading pos ws _ := i1 then
+        if let .original ws' _ trailing endPos := i2 then
+          emitToken (.original leading pos trailing endPos) ⟨.docComment, opener ++ ws.toString ++ ws'.toString ++ body⟩
+          return
+      emitString' (opener ++ " " ++ body ++ "\n")
     | .node _ k children =>
       for child in children do
         highlight' ids child (lookingAt := some k)

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

@@ -8,6 +8,7 @@ inductive Highlighted.Token.Kind where
   | keyword (name : Option Name) (docs : Option String)
   | const (name : Name) (docs : Option String)
   | var (name : FVarId)
+  | docComment
   | sort
   | unknown
 deriving Repr, Inhabited
@@ -19,6 +20,7 @@ instance : Quote Highlighted.Token.Kind where
     | .keyword n docs => mkCApp ``keyword #[quote n, quote docs]
     | .const n docs => mkCApp ``const #[quote n, quote docs]
     | .var (.mk n) => mkCApp ``var #[mkCApp ``FVarId.mk #[quote n]]
+    | .docComment => mkCApp ``docComment #[]
     | .sort => mkCApp ``sort #[]
     | .unknown => mkCApp ``unknown #[]
 

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

@@ -43,6 +43,7 @@ defmethod Highlighted.Token.Kind.«class» : Highlighted.Token.Kind → String
   | .var _ => "var"
   | .sort  => "sort"
   | .const _ _ => "const"
+  | .docComment => "doc-comment"
   | .keyword _ _ => "keyword"
   | .unknown => "unknown"