fix: message placement and recursive function highlighting

examples/website/DemoSite/Blog/Conditionals.lean

@@ -29,6 +29,10 @@ def slowId : Nat → Nat
   | 0 => 0
   | n + 1 => slowId n + 1
 
+#eval slowId 5
+
 /-- An array literal -/
 example := #[1, 2, 3]
+
+example := 33
 ```

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

@@ -108,7 +108,6 @@ where
 
 def identKind [Monad m] [MonadInfoTree m] [MonadLiftT IO m]  [MonadFileMap m] [MonadEnv m] [MonadMCtx m] (ids : HashMap Lsp.RefIdent Lsp.RefIdent) (stx : TSyntax `ident) : m Token.Kind := do
   let trees ← getInfoTrees
-
   let mut kind : Token.Kind := .unknown
 
   for t in trees do
@@ -117,19 +116,28 @@ def identKind [Monad m] [MonadInfoTree m] [MonadLiftT IO m]  [MonadFileMap m] [M
       match info with
       | .ofTermInfo termInfo => do
         let expr ← instantiateMVars termInfo.expr
-        let ty ← instantiateMVars (← runMeta <| Meta.inferType expr)
-        let tyStr := toString (← runMeta <| Meta.ppExpr ty)
         match expr with
         | Expr.fvar id =>
           let seen ←
             if let some y := ids.find? (.fvar id) then
               match y with
-              | .fvar x => pure <| .var x
-              | .const x => do
+              | .fvar x =>
+                let ty ← instantiateMVars (← runMeta <| Meta.inferType expr)
+                let tyStr := toString (← runMeta <| Meta.ppExpr ty)
+                if let some localDecl := termInfo.lctx.find? x then
+                  if localDecl.isAuxDecl then
+                    let e ← runMeta <| Meta.ppExpr expr
+                    pure (.const (toString e) tyStr none)
+                  else pure (.var x tyStr)
+                else pure (.var x tyStr)
+              | .const x =>
                 let sig := toString (← runMeta (PrettyPrinter.ppSignature x)).1
                 let docs ← findDocString? (← getEnv) x
                 pure (.const x sig docs)
-            else pure (.var id)
+            else
+              let ty ← instantiateMVars (← runMeta <| Meta.inferType expr)
+              let tyStr := toString (← runMeta <| Meta.ppExpr ty)
+              pure (.var id tyStr)
           if seen.priority > kind.priority then kind := seen
         | Expr.const name _ => --TODO universe vars
           let docs ← findDocString? (← getEnv) name
@@ -218,12 +226,15 @@ private defmethod Lean.Position.notAfter (pos1 pos2 : Lean.Position) : Bool :=
   pos1.line < pos2.line || (pos1.line == pos2.line && pos1.column ≤ pos2.column)
 
 
-def HighlightState.ofMessages (messages : Array Message) : HighlightState := {
-  messages := sortedMessages
-  nextMessage := if h : 0 < sortedMessages.size then some ⟨0, h⟩ else none
-  output := []
-  inMessages := []
-}
+def HighlightState.ofMessages [Monad m] [MonadFileMap m]
+    (stx : Syntax) (messages : Array Message) : m HighlightState := do
+  let msgs ← (·.qsort cmp) <$> messages.filterM (isRelevant stx)
+  pure {
+    messages := msgs,
+    nextMessage := if h : 0 < msgs.size then some ⟨0, h⟩ else none,
+    output := [],
+    inMessages := [],
+  }
 where
   cmp (m1 m2 : Message) :=
     if m1.pos.before m2.pos then true
@@ -234,7 +245,16 @@ where
       | none, some _ => true
       | some e1, some e2 => e2.before e1
     else false
-  sortedMessages := messages.qsort cmp
+
+  isRelevant (stx : Syntax) (msg : Message) : m Bool := do
+    let text ← getFileMap
+    let (some s, some e) := (stx.getPos?.map text.toPosition , stx.getTailPos?.map text.toPosition)
+      | return false
+    if let some e' := msg.endPos then
+      pure <| !(e'.before s) && !(e.before msg.pos)
+    else
+      pure <| !(msg.pos.before s) && !(e.before msg.pos)
+
 
 abbrev HighlightM (α : Type) : Type := StateT HighlightState TermElabM α
 
@@ -372,5 +392,6 @@ partial def highlight' (ids : HashMap Lsp.RefIdent Lsp.RefIdent) (stx : Syntax)
 def highlight (stx : Syntax) (messages : Array Message) : TermElabM Highlighted := do
   let modrefs := Lean.Server.findModuleRefs (← getFileMap) (← getInfoTrees).toArray
   let ids := build modrefs
-  let ((), {output := output, ..}) ← StateT.run (highlight' ids stx) (.ofMessages messages)
+  let st ← HighlightState.ofMessages stx messages
+  let ((), {output := output, ..}) ← StateT.run (highlight' ids stx) st
   pure <| .fromOutput output

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

@@ -7,7 +7,7 @@ namespace Verso.Genre
 inductive Highlighted.Token.Kind where
   | keyword (name : Option Name) (docs : Option String)
   | const (name : Name) (signature : String) (docs : Option String)
-  | var (name : FVarId)
+  | var (name : FVarId) (type : String)
   | option (name : Name) (docs : Option String)
   | docComment
   | sort
@@ -21,7 +21,7 @@ instance : Quote Highlighted.Token.Kind where
     | .keyword n docs => mkCApp ``keyword #[quote n, 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) => mkCApp ``var #[mkCApp ``FVarId.mk #[quote n]]
+    | .var (.mk n) type => mkCApp ``var #[mkCApp ``FVarId.mk #[quote n], quote type]
     | .docComment => mkCApp ``docComment #[]
     | .sort => mkCApp ``sort #[]
     | .unknown => mkCApp ``unknown #[]

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

@@ -40,7 +40,7 @@ instance [Monad m] : MonadConfig (HtmlT Page m) where
 open HtmlT
 
 defmethod Highlighted.Token.Kind.«class» : Highlighted.Token.Kind → String
-  | .var _ => "var"
+  | .var _ _ => "var"
   | .sort  => "sort"
   | .const _ _ _ => "const"
   | .option _ _ => "option"
@@ -50,7 +50,7 @@ defmethod Highlighted.Token.Kind.«class» : Highlighted.Token.Kind → String
 
 defmethod Highlighted.Token.Kind.data : Highlighted.Token.Kind → String
   | .const n _ _ => "const-" ++ toString n
-  | .var ⟨v⟩ => "var-" ++ toString v
+  | .var ⟨v⟩ _ => "var-" ++ toString v
   | .option n _ => "option-" ++ toString n
   | _ => ""
 
@@ -70,6 +70,8 @@ defmethod Highlighted.Token.Kind.hover? : (tok : Highlighted.Token.Kind) → Opt
       | none => .empty
       | some txt => {{<hr/><pre class="docstring">{{txt}}</pre>}}
     some <| hover {{ {{toString n}} {{docs}} }}
+  | .var _ type =>
+    some <| hover {{ {{type}} }}
   | _ => none