fix: document symbols display plus highlighting bug

src/verso-manual/VersoManual/Docstring.lean

@@ -701,7 +701,7 @@ def docstring : BlockRoleExpander
     match args with
     | #[.anon (.name x)] =>
       let name ← Elab.realizeGlobalConstNoOverloadWithInfo x
-      Doc.PointOfInterest.save x name.toString
+      Doc.PointOfInterest.save (← getRef) name.toString (detail? := some "Documentation")
       let blockStx ← match ← Lean.findDocString? (← getEnv) name with
       | none => logWarningAt x m!"No docs found for '{x}'"; pure #[]
       | some docs =>

src/verso-manual/VersoManual/Glossary.lean

@@ -8,14 +8,23 @@ import Lean.Data.Json
 import Lean.Data.Json.FromToJson
 
 import VersoManual.Basic
+import Verso.Doc.ArgParse
 
-open Verso Genre Manual
+open Verso Genre Manual ArgParse
 open Verso.Doc.Elab
 open Lean (Json ToJson FromJson HashSet)
 
 namespace Verso.Genre.Manual
 
 
+structure TechArgs where
+  key : Option String
+  normalize : Bool
+
+def TechArgs.parse [Monad m] [Lean.MonadError m] [MonadLiftT Lean.CoreM m] : ArgParse m TechArgs :=
+  TechArgs.mk <$> .named `key .string true <*> .namedD `normalize .bool true
+
+
 private def glossaryState := `Verso.Genre.Manual.glossary
 
 def Inline.deftech : Inline where
@@ -38,6 +47,8 @@ private partial def normString (term : String) : String := Id.run do
   if str.endsWith "s" then str := str.dropRight 1
   String.intercalate " " (str.split (fun c => c.isWhitespace || c == '-') |>.filter (!·.isEmpty))
 
+
+open Lean in
 /--
 Defines a technical term.
 
@@ -53,11 +64,27 @@ of the automatically-derived key.
 
 Uses of `tech` use the same process to derive a key, and the key is matched against the `deftech` table.
 -/
-def deftech (args : Array (Doc.Inline Manual))
-    (key : Option String := none) (normalize : Bool := true)
-    : Doc.Inline Manual :=
-  let k := key.getD (techString (.concat args))
-  Doc.Inline.other {Inline.deftech with data := if normalize then normString k else k} args
+@[role_expander deftech]
+def deftech : RoleExpander
+  | args, content => do
+    let {key, normalize} ← TechArgs.parse.run args
+
+
+    -- Heuristically guess at the string and key (usually works)
+    let str := inlineToString (← getEnv) <| mkNullNode content
+    let k := key.getD str
+    let k := if normalize then normString k else k
+    Doc.PointOfInterest.save (← getRef) str
+      (detail? := some s!"Def (key {k})")
+      (kind := .key)
+
+    let content ← content.mapM elabInline
+
+    let stx ←
+      `(let content : Array (Doc.Inline Verso.Genre.Manual) := #[$content,*]
+        let k := ($(quote key) : Option String).getD (techString (Doc.Inline.concat content))
+        Doc.Inline.other {Inline.deftech with data := if $(quote normalize) then normString k else k} content)
+    return #[stx]
 
 /-- Adds an internal identifier as a target for a given glossary entry -/
 def Glossary.addEntry [Monad m] [MonadState TraverseState m] [MonadLiftT IO m] [MonadReaderOf TraverseContext m]
@@ -96,6 +123,7 @@ def deftech.descr : InlineDescr where
 def Inline.tech : Inline where
   name := `Verso.Genre.Manual.tech
 
+open Lean in
 /--
 Emits a reference to a technical term defined with `deftech.`
 
@@ -109,11 +137,26 @@ information from the arguments in `args`, and then normalizing the resulting str
 Call with `(normalize := false)` to disable normalization, and `(key := some k)` to use `k` instead
 of the automatically-derived key.
 -/
-def tech (args : Array (Doc.Inline Manual))
-    (key : Option String := none) (normalize : Bool := true)
-    : Doc.Inline Manual :=
-  let k := key.getD (techString (.concat args))
-  Doc.Inline.other {Inline.tech with data := if normalize then normString k else k} args
+@[role_expander tech]
+def tech : RoleExpander
+  | args, content => do
+    let {key, normalize} ← TechArgs.parse.run args
+
+    -- Heuristically guess at the string and key (usually works)
+    let str := inlineToString (← getEnv) <| mkNullNode content
+    let k := key.getD str
+    let k := if normalize then normString k else k
+    Doc.PointOfInterest.save (← getRef) str
+      (detail? := some s!"Use (key {k})")
+      (kind := .key)
+
+    let content ← content.mapM elabInline
+
+    let stx ←
+      `(let content : Array (Doc.Inline Verso.Genre.Manual) := #[$content,*]
+        let k := ($(quote key) : Option String).getD (techString (Doc.Inline.concat content))
+        Doc.Inline.other {Inline.tech with data := if $(quote normalize) then normString k else k} content)
+    return #[stx]
 
 @[inline_extension tech]
 def tech.descr : InlineDescr where

src/verso/Verso/Code/Highlighted.lean

@@ -1043,7 +1043,7 @@ window.onload = () => {
       const addTippy = (selector, props) => {
         tippy(selector, Object.assign({}, defaultTippyProps, props));
       };
-      addTippy('.hl.lean .const.token, .hl.lean .keyword.token, .hl.lean .literal.token, .hl.lean .option.token', {theme: 'lean'});
+      addTippy('.hl.lean .const.token, .hl.lean .keyword.token, .hl.lean .literal.token, .hl.lean .option.token, .hl.lean .var.token', {theme: 'lean'});
       addTippy('.hl.lean .has-info.warning', {theme: 'warning message'});
       addTippy('.hl.lean .has-info.info', {theme: 'info message'});
       addTippy('.hl.lean .has-info.error', {theme: 'error message'});

src/verso/Verso/Doc/ArgParse.lean

@@ -43,6 +43,9 @@ instance : Alternative (ArgParse m) where
   failure := ArgParse.fail none none
   orElse := ArgParse.orElse
 
+def ArgParse.namedD {m} (name : Name) (val : ValDesc m α) (default : α) : ArgParse m α :=
+  named name val true <&> (·.getD default)
+
 def ArgParse.describe : ArgParse m α → MessageData
   | .fail _ msg? => msg?.getD "Cannot succeed"
   | .pure x => "No arguments expected"

src/verso/Verso/Doc/Concrete.lean

@@ -196,6 +196,10 @@ where
       (show MetaM Unit from set termState.meta.meta)
       (show CoreM Unit from set termState.meta.core.toState)
 
+open Lean.Parser.Command in
+instance : Quote String (k := ``docComment) where
+  quote str := ⟨.node .none ``docComment #[ .atom .none "/--", .atom .none (str ++ "-/")]⟩
+
 elab (name := completeDoc) "#doc" "(" genre:term ")" title:inlineStr "=>" text:completeDocument eoi : command => open Lean Elab Term Command PartElabM DocElabM in do
   findGenreCmd genre
   let endPos := (← getFileMap).source.endPos
@@ -215,7 +219,8 @@ elab (name := completeDoc) "#doc" "(" genre:term ")" title:inlineStr "=>" text:c
         saveRefs st st'
         let n ← currentDocName
         let docName := mkIdentFrom title n
-        elabCommand (← `(def $docName : Part $genre := $(← finished.toSyntax' genre st'.linkDefs st'.footnoteDefs))))
+        let titleStr : TSyntax ``Lean.Parser.Command.docComment := quote titleString
+        elabCommand (← `($titleStr:docComment def $docName : Part $genre := $(← finished.toSyntax' genre st'.linkDefs st'.footnoteDefs))))
       (handleStep := partCommand)
       (run := fun act => liftTermElabM <| Prod.fst <$> PartElabM.run {} initState act)
 

src/verso/Verso/Doc/Elab.lean

@@ -329,7 +329,7 @@ def includeSection : PartCommand
     | _ => throwErrorAt stx "Expected exactly one positional argument that is a name"
   | _ => Lean.Elab.throwUnsupportedSyntax
 where
- resolved id := mkIdentFrom id <$> resolveGlobalConstNoOverload (mkIdentFrom id (docName id.getId))
+ resolved id := mkIdentFrom id <$> realizeGlobalConstNoOverloadWithInfo (mkIdentFrom id (docName id.getId))
 
 @[block_expander Verso.Syntax.block_role]
 def _root_.Verso.Syntax.block_role.expand : BlockExpander := fun block =>

src/verso/Verso/Doc/Elab/ExpanderAttribute.lean

@@ -16,11 +16,25 @@ unsafe def mkDocExpanderAttrUnsafe (attrName typeName : Name) (descr : String) (
     valueTypeName := typeName,
     evalKey := fun _ stx => do
       Elab.realizeGlobalConstNoOverloadWithInfo (← Attribute.Builtin.getIdent stx)
-      -- return (← Attribute.Builtin.getIdent stx).getId
   } attrDeclName
 
 
 @[implemented_by mkDocExpanderAttrUnsafe]
 opaque mkDocExpanderAttributeSafe (attrName typeName : Name) (desc : String) (attrDeclName : Name) : IO (KeyedDeclsAttribute α)
 
 def mkDocExpanderAttribute (attrName typeName : Name) (desc : String) (attrDeclName : Name := by exact decl_name%) : IO (KeyedDeclsAttribute α) := mkDocExpanderAttributeSafe attrName typeName desc attrDeclName
+
+unsafe def mkUncheckedDocExpanderAttrUnsafe (attrName typeName : Name) (descr : String) (attrDeclName : Name) : IO (KeyedDeclsAttribute α) :=
+  KeyedDeclsAttribute.init {
+    name := attrName,
+    descr := descr,
+    valueTypeName := typeName,
+    evalKey := fun _ stx => do
+      return (← Attribute.Builtin.getIdent stx).getId
+  } attrDeclName
+
+
+@[implemented_by mkUncheckedDocExpanderAttrUnsafe]
+opaque mkUncheckedDocExpanderAttributeSafe (attrName typeName : Name) (desc : String) (attrDeclName : Name) : IO (KeyedDeclsAttribute α)
+
+def mkUncheckedDocExpanderAttribute (attrName typeName : Name) (desc : String) (attrDeclName : Name := by exact decl_name%) : IO (KeyedDeclsAttribute α) := mkUncheckedDocExpanderAttributeSafe attrName typeName desc attrDeclName

src/verso/Verso/Doc/Elab/InlineString.lean

@@ -12,7 +12,7 @@ open Lean
 abbrev InlineToString := Environment → Syntax → Option String
 
 initialize inlineToStringAttr : KeyedDeclsAttribute InlineToString ←
-  mkDocExpanderAttribute `inline_to_string ``InlineToString "Indicates that this function converts an inline element to a plain string for use in previews and navigation" `inlineToStringAttr
+  mkUncheckedDocExpanderAttribute `inline_to_string ``InlineToString "Indicates that this function converts an inline element to a plain string for use in previews and navigation" `inlineToStringAttr
 
 unsafe def inlineToStringForUnsafe (env : Environment) (x : Name) : Array InlineToString :=
   let expanders := inlineToStringAttr.getEntries env x
@@ -23,13 +23,13 @@ opaque inlineToStringFor (env : Environment) (x : Name) : Array InlineToString
 
 /-- Heuristically construct a plan string preview of the syntax of an inline element -/
 def inlineToString (env : Environment) (inline : Syntax) : String := Id.run do
-  match inline with
-  | stx@(.node _ kind _) =>
-    let toStr ← inlineToStringFor env kind
-    for f in toStr do
-      if let some str := f env stx then return str
-    fallback
-  | _ =>
-    fallback
+  let kind := inline.getKind
+  let toStr ← inlineToStringFor env kind
+  for f in toStr do
+    if let some str := f env inline then return str
+
+  dbg_trace "Failed to convert {inline} with {kind}"
+
+  fallback
 where
   fallback := pure "<missing>"

src/verso/Verso/Doc/Elab/Monad.lean

@@ -53,6 +53,18 @@ def _root_.Verso.Syntax.code.inline_to_string : InlineToString
     some str.getString
   | _, _ => none
 
+@[inline_to_string Verso.Syntax.role]
+def _root_.Verso.Syntax.role.inline_to_string : InlineToString
+  | env, `(inline| role{ $_ $_* }[ $body ]) =>
+    inlineToString env body
+  | _, _ => none
+
+@[inline_to_string null]
+def nullInline_to_string : InlineToString
+  | env, .node _ _ contents =>
+    return String.join <| contents.toList.map (inlineToString env)
+  | _, _ => none
+
 
 def inlinesToString (env : Environment) (inlines : Array Syntax)  : String :=
   String.intercalate " " (inlines.map (inlineToString env)).toList