diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean
index 06986e5..5c84f1e 100644
--- a/src/verso-manual/VersoManual/Docstring.lean
+++ b/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 =>
diff --git a/src/verso-manual/VersoManual/Glossary.lean b/src/verso-manual/VersoManual/Glossary.lean
index fad52b8..1a58532 100644
--- a/src/verso-manual/VersoManual/Glossary.lean
+++ b/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
diff --git a/src/verso/Verso/Code/Highlighted.lean b/src/verso/Verso/Code/Highlighted.lean
index f47e268..2d7be7c 100644
--- a/src/verso/Verso/Code/Highlighted.lean
+++ b/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'});
diff --git a/src/verso/Verso/Doc/ArgParse.lean b/src/verso/Verso/Doc/ArgParse.lean
index 56499ac..5e065f2 100644
--- a/src/verso/Verso/Doc/ArgParse.lean
+++ b/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"
diff --git a/src/verso/Verso/Doc/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean
index 78f6926..02efaba 100644
--- a/src/verso/Verso/Doc/Concrete.lean
+++ b/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)
 
diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean
index 71d655c..c1f379a 100644
--- a/src/verso/Verso/Doc/Elab.lean
+++ b/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 =>
diff --git a/src/verso/Verso/Doc/Elab/ExpanderAttribute.lean b/src/verso/Verso/Doc/Elab/ExpanderAttribute.lean
index 8cc8009..33a4d72 100644
--- a/src/verso/Verso/Doc/Elab/ExpanderAttribute.lean
+++ b/src/verso/Verso/Doc/Elab/ExpanderAttribute.lean
@@ -16,7 +16,6 @@ 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
 
 
@@ -24,3 +23,18 @@ unsafe def mkDocExpanderAttrUnsafe (attrName typeName : Name) (descr : String) (
 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
diff --git a/src/verso/Verso/Doc/Elab/InlineString.lean b/src/verso/Verso/Doc/Elab/InlineString.lean
index ee1faf9..990063f 100644
--- a/src/verso/Verso/Doc/Elab/InlineString.lean
+++ b/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>"
diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean
index e0c0d74..b2ba9e1 100644
--- a/src/verso/Verso/Doc/Elab/Monad.lean
+++ b/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
diff --git a/src/verso/Verso/Doc/Lsp.lean b/src/verso/Verso/Doc/Lsp.lean
index 2290006..ff9f579 100644
--- a/src/verso/Verso/Doc/Lsp.lean
+++ b/src/verso/Verso/Doc/Lsp.lean
@@ -11,6 +11,7 @@ import Verso.Doc.Elab
 import Verso.Syntax
 import Verso.Hover
 import Verso.Doc.PointOfInterest
+import Verso.Doc.Name
 
 namespace Verso.Lsp
 
@@ -242,29 +243,62 @@ def rangeContains (outer inner : Lsp.Range) :=
   outer.start < inner.start && inner.«end» ≤ outer.«end» ||
   outer.start == inner.start && inner.«end» < outer.«end»
 
-mutual
-  partial def graftSymbolOnto (inner outer : DocumentSymbol) : Option DocumentSymbol :=
-    match outer, inner with
-    | .mk s1, .mk s2 =>
-      if rangeContains s1.range s2.range then
-        -- add as child
-        some <| .mk {s1 with children? := some (graftSymbolInto inner (s1.children?.getD #[])) }
-      else
-        -- signal peer
-        none
-
-  partial def graftSymbolInto (inner : DocumentSymbol) (outer : Array DocumentSymbol) : Array DocumentSymbol := Id.run do
-    let mut i := 0
-    while h : i < outer.size do
-      let sym := outer[i]
-      if let some sym' := graftSymbolOnto inner sym then
-        return outer.set i sym'
-      i := i + 1
-    return outer.push inner
-end
-
-def graftSymbols (inner outer : Array DocumentSymbol) : Array DocumentSymbol :=
-  inner.foldr graftSymbolInto outer
+-- mutual
+--   partial def graftSymbolOnto (inner outer : DocumentSymbol) : Option DocumentSymbol :=
+--     match outer, inner with
+--     | .mk s1, .mk s2 =>
+--       if rangeContains s1.range s2.range then
+--         -- add as child
+--         some <| .mk {s1 with children? := some (graftSymbolInto inner (s1.children?.getD #[])) }
+--       else
+--         -- signal peer
+--         none
+
+--   partial def graftSymbolInto (inner : DocumentSymbol) (outer : Array DocumentSymbol) : Array DocumentSymbol := Id.run do
+--     let mut i := 0
+--     while h : i < outer.size do
+--       let sym := outer[i]
+--       if let some sym' := graftSymbolOnto inner sym then
+--         return outer.set i sym'
+--       i := i + 1
+--     return outer.push inner
+-- end
+
+-- def graftSymbols (inner outer : Array DocumentSymbol) : Array DocumentSymbol :=
+--   inner.foldr graftSymbolInto outer
+
+partial def mergeInto (sym : DocumentSymbol) (existing : Array DocumentSymbol) : Array DocumentSymbol := Id.run do
+  let ⟨sym⟩ := sym
+  for h : i in [0:existing.size] do
+    let ⟨e⟩ := existing[i]
+    have : i < existing.size := by get_elem_tactic
+    have : i ≤ existing.size := by omega
+    let children := e.children?.getD #[]
+
+    -- the symbol to be inserted belongs before the current symbol
+    if sym.range.end ≤ e.range.start then
+      return existing.insertIdx i ⟨sym⟩
+    -- the symbol to be inserted intersects the current symbol but neither contains the other
+    else if sym.range.start < e.range.start && sym.range.end ≤ e.range.end then
+      return existing.insertIdx i ⟨sym⟩
+    else if sym.range.start ≥ e.range.start && sym.range.start < e.range.end && sym.range.end > e.range.end then
+      return existing.insertIdx (i + 1) ⟨sym⟩
+    -- The symbol to be inserted is inside the existing one
+    else if sym.range.start ≥ e.range.start && sym.range.end ≤ e.range.end then
+      return existing.set i ⟨{e with children? := some (mergeInto ⟨sym⟩ children)}⟩
+    -- The symbol to be inserted encompasses the existing one
+    else if sym.range.start ≤ e.range.start && sym.range.end ≥ e.range.end then
+      let (inside, outside) := existing.partition (fun ⟨e⟩ => sym.range.start ≤ e.range.start && sym.range.end ≥ e.range.end)
+      let (pre, post) := outside.partition (fun ⟨e⟩ => sym.range.end ≤ e.range.start)
+      return pre ++ inside.foldr (init := #[⟨sym⟩]) mergeInto ++ post
+    -- The symbol to be inserted is after the existing one
+    else
+      continue
+  -- If we got through the loop, then the new symbol belongs at the end
+  return existing.push ⟨sym⟩
+
+def mergeManyInto (syms : Array DocumentSymbol) (existing : Array DocumentSymbol) : Array DocumentSymbol :=
+  syms.foldr (init := existing) mergeInto
 
 open Lean Server Lsp RequestM in
 def mergeResponses (docTask : RequestTask α) (leanTask : RequestTask β) (f : Option α → Option β → γ) : RequestM (RequestTask γ) := do
@@ -286,20 +320,21 @@ partial def handleSyms (_params : DocumentSymbolParams) (prev : RequestTask Docu
   -- bad: we have to wait on elaboration of the entire file before we can report document symbols
   let t := doc.cmdSnaps.waitAll
   let syms ← mapTask t fun (snaps, _) => do
-      return { syms := getSections text snaps : DocumentSymbolResult }
+      return { syms := (← getSections text snaps) : DocumentSymbolResult }
   let syms' ← mapTask t fun (snaps, _) => do
       return { syms := ofInterest text snaps : DocumentSymbolResult }
   mergeResponses (← mergeResponses syms syms' combineAnswers) prev combineAnswers
   --pure syms
   where
-    combineAnswers (x y : Option DocumentSymbolResult) : DocumentSymbolResult := ⟨graftSymbols (x.getD ⟨{}⟩).syms (y.getD ⟨{}⟩).syms⟩
-    tocSym (text : FileMap) : TOC → Id (Option DocumentSymbol)
+    combineAnswers (x y : Option DocumentSymbolResult) : DocumentSymbolResult :=
+      ⟨mergeManyInto (x.getD ⟨{}⟩).syms (y.getD ⟨{}⟩).syms⟩
+    tocSym (env) (text : FileMap) : TOC → IO (Option DocumentSymbol)
       | .mk title titleStx endPos children => do
         let some selRange@⟨start, _⟩ := titleStx.lspRange text
           | return none
         let mut kids := #[]
         for c in children do
-          if let some s := tocSym text c then kids := kids.push s
+          if let some s ← tocSym env text c then kids := kids.push s
         return some <| DocumentSymbol.mk {
           name := title,
           kind := SymbolKind.string,
@@ -308,16 +343,17 @@ partial def handleSyms (_params : DocumentSymbolParams) (prev : RequestTask Docu
           children? := kids
         }
       | .included name => do
-        -- TODO Evaluate the name to find the actual included title
+        let title := (← findDocString? env name.getId).getD (toString <| Verso.Doc.unDocName name.getId)
         let some rng := name.raw.lspRange text
           | return none
         return some <| DocumentSymbol.mk {
-          name := toString name,
+          name := title,
           kind := SymbolKind.property,
-          range := rng
-          selectionRange := rng
+          range := rng,
+          selectionRange := rng,
+          detail? := some s!"Included from {name.getId}"
         }
-    getSections text ss : Array DocumentSymbol := Id.run do
+    getSections text ss : IO (Array DocumentSymbol) := do
       let mut syms := #[]
       for snap in ss do
         let info := snap.infoTree.deepestNodes fun _ctxt info _arr =>
@@ -326,7 +362,7 @@ partial def handleSyms (_params : DocumentSymbolParams) (prev : RequestTask Docu
             data.get? TOC
           | _ => none
         for i in info do
-          if let some x ← tocSym text i then syms := syms.push x
+          if let some x ← tocSym snap.env text i then syms := syms.push x
       pure syms
     ofInterest (text : FileMap) (ss : List Snapshots.Snapshot) : Array DocumentSymbol := Id.run do
       let mut syms := #[]
@@ -336,11 +372,27 @@ partial def handleSyms (_params : DocumentSymbolParams) (prev : RequestTask Docu
           | .ofCustomInfo ⟨stx, data⟩ =>
             data.get? PointOfInterest |>.map (stx, ·)
           | _ => none
-        for (stx, ⟨title⟩) in info do
+        for (stx, {title, selectionRange, kind, detail?}) in info do
           if let some rng := stx.lspRange text then
-            syms := syms.push <| .mk {name := title, kind := .constant, range := rng, selectionRange := rng}
+            -- Truncate the inner to the outer if the user made a mistake with it
+            let selectionRange := truncate rng (selectionRange.map text.utf8RangeToLspRange |>.getD rng)
+            let sym := .mk {
+              name := title,
+              range := rng,
+              selectionRange,
+              detail?,
+              kind
+            }
+            -- mergeInto is needed here to keep the tree invariant
+            syms := mergeInto sym syms
       pure syms
-
+    truncate (outer inner : Range) : Range :=
+      if inner.start < outer.start && inner.end < outer.end then outer
+      else if inner.start > outer.end then outer
+      else
+        let start := if outer.start > inner.start then outer.start else inner.start
+        let «end» := if outer.start < inner.start then outer.start else inner.start
+        ⟨start, «end»⟩
 
 -- Shamelessly cribbed from https://github.com/tydeu/lean4-alloy/blob/57792f4e8a9674f8b4b8b17742607a1db142d60e/Alloy/C/Server/SemanticTokens.lean
 structure SemanticTokenEntry where
@@ -501,23 +553,39 @@ def renumberLists : CodeActionProvider := fun params snap => do
       }
     }
 
-partial def directiveResizings (startPos endPos : String.Pos) (text : FileMap) (parents : Array (Syntax × Syntax)) (subject : Syntax) : StateM (Array (Bool × Syntax × Syntax × TextEditBatch)) Unit := do
+partial def directiveResizings
+    (startPos endPos : String.Pos)
+    (startLine endLine : Nat)
+    (text : FileMap)
+    (parents : Array (Syntax × Syntax))
+    (subject : Syntax) :
+    StateM (Array (Bool × Syntax × Syntax × TextEditBatch)) Unit := do
   match subject with
   | `<low|(Verso.Syntax.directive  ~opener ~_name ~_args ~_fake ~_fake' ~(.node _ `null contents) ~closer )> =>
     let parents := parents.push (opener, closer)
-    if inRange opener || inRange closer then
+    if onLine opener || onLine closer then
       if let some edit := parents.flatMapM getIncreases then
         modify (·.push (true, opener, closer, edit))
       if let some edit := getDecreases (opener, closer) contents then
         modify (·.push (false, opener, closer, edit))
     else
-      for s in contents do directiveResizings startPos endPos text parents s
+      for s in contents do directiveResizings startPos endPos startLine endLine text parents s
   | stx@(.node _ _ contents) =>
     if inRange stx then
       for s in contents do
-        directiveResizings startPos endPos text parents s
+        directiveResizings startPos endPos startLine endLine text parents s
   | _ => pure ()
 where
+  onLine (stx : Syntax) : Bool := Id.run do
+    if startLine != endLine then return false
+    let some stxPos := stx.getPos?
+      | false
+    let some stxTailPos := stx.getTailPos?
+      | false
+    let ⟨{line := stxStartLine, ..}, {line := stxEndLine, ..}⟩ :=
+      text.utf8RangeToLspRange ⟨stxPos, stxTailPos⟩
+    if stxStartLine != stxEndLine then return false
+    startLine == stxStartLine
   inRange (stx : Syntax) : Bool :=
     if let some ⟨stxStart, stxEnd⟩ := stx.getRange? then
       -- if the syntax starts before the selection, then it should end after the selection begins
@@ -562,7 +630,10 @@ def resizeDirectives : CodeActionProvider := fun params snap => do
   let text := doc.meta.text
   let startPos := text.lspPosToUtf8Pos params.range.start
   let endPos := text.lspPosToUtf8Pos params.range.end
-  let ((), directives) := directiveResizings startPos endPos text #[] snap.stx |>.run #[]
+  let ((), directives) :=
+    (directiveResizings startPos endPos
+      params.range.start.line params.range.end.line
+      text #[] snap.stx).run #[]
   pure <| directives.map fun (which, _, _, edits) => {
     eager := {
       title := (if which then "More" else "Less") ++ " Colons",
@@ -577,6 +648,7 @@ def resizeDirectives : CodeActionProvider := fun params snap => do
   }
 
 
+
 deriving instance FromJson for FoldingRangeKind
 deriving instance FromJson for FoldingRange
 
diff --git a/src/verso/Verso/Doc/Name.lean b/src/verso/Verso/Doc/Name.lean
index 8508b69..3c201bd 100644
--- a/src/verso/Verso/Doc/Name.lean
+++ b/src/verso/Verso/Doc/Name.lean
@@ -10,8 +10,25 @@ namespace Verso.Doc
 
 open Lean
 
+@[match_pattern]
+private def versoModuleDocNameString : String := "the canonical document object name"
+
 def docName (moduleName : Name) : Name :=
-  id <| .str moduleName "the canonical document object name"
+  id <| .str moduleName versoModuleDocNameString
+
+/-- If the argument is a module's document name, extract the module name. Otherwise do nothing. -/
+def unDocName (docName : Name) : Name :=
+  match docName with
+  | .str moduleName versoModuleDocNameString => moduleName
+  | _ => docName
+
+/-- info: `X.Y -/
+#guard_msgs in
+#eval unDocName <| docName `X.Y
+
+/-- info: `X.Y -/
+#guard_msgs in
+#eval unDocName `X.Y
 
 macro "%doc" moduleName:ident : term =>
   pure <| mkIdentFrom moduleName <| docName moduleName.getId
diff --git a/src/verso/Verso/Doc/PointOfInterest.lean b/src/verso/Verso/Doc/PointOfInterest.lean
index 4c8c7b1..b2aabdb 100644
--- a/src/verso/Verso/Doc/PointOfInterest.lean
+++ b/src/verso/Verso/Doc/PointOfInterest.lean
@@ -12,8 +12,14 @@ open Lean Elab Server RequestM
 
 structure PointOfInterest where
   title : String
+  selectionRange : Option String.Range := none
+  kind : Lean.Lsp.SymbolKind := .constant
+  detail? : Option String
 
 deriving TypeName
 
-def PointOfInterest.save [Monad m] [MonadInfoTree m] (stx : Syntax) (title : String) : m Unit := do
-  pushInfoLeaf <| .ofCustomInfo {stx := stx, value := Dynamic.mk (PointOfInterest.mk title)}
+def PointOfInterest.save [Monad m] [MonadInfoTree m] (stx : Syntax) (title : String)
+    (selectionRange : Syntax := stx)
+    (kind : Lean.Lsp.SymbolKind := .constant)
+    (detail? : Option String := none) : m Unit := do
+  pushInfoLeaf <| .ofCustomInfo {stx := stx, value := Dynamic.mk (PointOfInterest.mk title selectionRange.getRange? kind detail?)}