chore: bump to new nightly (#286)

This fixes compatibility with upstream changes to LSP internals. In
the process, the refactoring of the syntax representation was
propagated to the semantic token highlighter, greatly improving it.

lean-toolchain

@@ -1,2 +1,2 @@
-leanprover/lean4:v4.17.0-rc1
+leanprover/lean4:nightly-2025-02-06
 

src/verso-manual/VersoManual/Docstring.lean

@@ -1229,7 +1229,7 @@ def blockFromMarkdownWithLean (names : List Name) (b : MD4Lean.Block) : DocElabM
                 (elabBlockCode := tryElabBlockCode)
             synthesizeSyntheticMVarsUsingDefault
 
-            discard <| addAutoBoundImplicits #[]
+            discard <| addAutoBoundImplicits #[] (inlayHintPos? := none)
 
             return res
           catch e =>

src/verso/Verso/Doc/Concrete.lean

@@ -51,10 +51,12 @@ def inlineStr := withAntiquot (mkAntiquot "inlineStr" `inlineStr) (inStrLit <| t
 elab "inlines!" s:inlineStr : term => open Lean Elab Term in
   match s.raw with
   | `<low| [~_ ~(.node _ _ out) ] > => do
-    let (tms, _) ← DocElabM.run {} (.init (← `(foo))) <| out.mapM elabInline
+    let (tms, _) ← DocElabM.run {} (.init (← `(foo))) <| out.mapM (elabInline ⟨·⟩)
     elabTerm (← `(term| #[ $[$tms],* ] )) none
   | _ => throwUnsupportedSyntax
 
+
+
 set_option pp.rawOnError true
 
 /--
@@ -117,8 +119,8 @@ elab "#docs" "(" genre:term ")" n:ident title:inlineStr ":=" ":::::::" text:docu
     | dbg_trace "nope {ppSyntax title}" throwUnsupportedSyntax
   let titleString := inlinesToString (← getEnv) titleParts
   let ((), st, st') ← liftTermElabM <| PartElabM.run {} (.init titleName) <| do
-    setTitle titleString (← liftDocElabM <| titleParts.mapM elabInline)
-    for b in blocks do partCommand b
+    setTitle titleString (← liftDocElabM <| titleParts.mapM (elabInline ⟨·⟩))
+    for b in blocks do partCommand ⟨b⟩
     closePartsUntil 0 endPos
     pure ()
   let finished := st'.partContext.toPartFrame.close endPos
@@ -137,10 +139,10 @@ elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:completeDocument eoi :
   let titleString := inlinesToString (← getEnv) titleParts
   let ((), st, st') ← PartElabM.run {} (.init titleName) <| do
     let mut errors := #[]
-    setTitle titleString (← liftDocElabM <| titleParts.mapM elabInline)
+    setTitle titleString (← liftDocElabM <| titleParts.mapM (elabInline ⟨·⟩))
     for b in blocks do
       try
-        partCommand b
+        partCommand ⟨b⟩
       catch e =>
         errors := errors.push e
     closePartsUntil 0 endPos
@@ -211,7 +213,7 @@ elab (name := completeDoc) "#doc" "(" genre:term ")" title:inlineStr "=>" text:c
   let initState : PartElabM.State := .init titleName
   withTraceNode `Elab.Verso (fun _ => pure m!"Document AST elab") <|
     incrementallyElabCommand blocks
-      (initAct := do setTitle titleString (← liftDocElabM <| titleParts.mapM elabInline))
+      (initAct := do setTitle titleString (← liftDocElabM <| titleParts.mapM (elabInline ⟨·⟩)))
       (endAct := fun ⟨st, st', _⟩ => withTraceNode `Elab.Verso (fun _ => pure m!"Document def") do
         let st' := st'.closeAll endPos
         let finished := st'.partContext.toPartFrame.close endPos
@@ -221,7 +223,7 @@ elab (name := completeDoc) "#doc" "(" genre:term ")" title:inlineStr "=>" text:c
         let docName := mkIdentFrom title n
         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)
+      (handleStep := (partCommand ⟨·⟩))
       (run := fun act => liftTermElabM <| Prod.fst <$> PartElabM.run {} initState act)
 
 /--

src/verso/Verso/Doc/Elab.lean

@@ -17,11 +17,11 @@ open Verso.Syntax
 def throwUnexpected [Monad m] [MonadError m] (stx : Syntax) : m α :=
   throwErrorAt stx "unexpected syntax{indentD stx}"
 
-partial def elabInline (inline : Syntax) : DocElabM (TSyntax `term) :=
+partial def elabInline (inline : TSyntax `inline) : DocElabM (TSyntax `term) :=
   withRef inline <| withFreshMacroScope <| withIncRecDepth <| do
-  match inline with
+  match inline.raw with
   | .missing =>
-    ``(sorryAx Inline (synthetic := true))
+    ``(sorryAx (Inline _) (synthetic := true))
   | stx@(.node _ kind _) =>
     let exp ← inlineExpandersFor kind
     for e in exp do
@@ -91,7 +91,7 @@ open Lean.Parser.Term in
 def appFallback
     (stx : Syntax)
     (name : Ident) (resolvedName : Name)
-    (argVals : Array Arg) (subjectArr : Option (Array Syntax))
+    (argVals : Array Arg) (subjectArr : Option (Array (TSyntax `inline)))
     : DocElabM Term := do
   let f := mkIdentFrom name resolvedName
   let valStx : ArgVal → DocElabM Term := fun
@@ -192,10 +192,10 @@ def _root_.Verso.Syntax.display_math.expand : InlineExpander
   | _ => throwUnsupportedSyntax
 
 
-def elabBlock (block : Syntax) : DocElabM (TSyntax `term) :=
+def elabBlock (block : TSyntax `block) : DocElabM (TSyntax `term) :=
   withTraceNode `Elab.Verso.block (fun _ => pure m!"Block {block}") <|
   withRef block <| withFreshMacroScope <| withIncRecDepth <| do
-  match block with
+  match block.raw with
   | .missing =>
     ``(sorryAx Block (synthetic := true))
   | stx@(.node _ kind _) =>
@@ -213,10 +213,10 @@ def elabBlock (block : Syntax) : DocElabM (TSyntax `term) :=
   | _ =>
     throwUnexpected block
 
-def partCommand (cmd : Syntax) : PartElabM Unit :=
+def partCommand (cmd : TSyntax `block) : PartElabM Unit :=
   withTraceNode `Elab.Verso.part (fun _ => pure m!"Part modification {cmd}") <|
   withRef cmd <| withFreshMacroScope <| do
-  match cmd with
+  match cmd.raw with
   | stx@(.node _ kind _) =>
     let exp ← partCommandsFor kind
     for e in exp do
@@ -241,7 +241,7 @@ where
 @[part_command Verso.Syntax.footnote_ref]
 partial def _root_.Verso.Syntax.footnote_ref.command : PartCommand
   | `(block| [^ $name:str ]: $contents* ) =>
-    addFootnoteDef name =<< contents.mapM (elabInline ·.raw)
+    addFootnoteDef name =<< contents.mapM (elabInline ·)
   | _ => throwUnsupportedSyntax
 
 @[part_command Verso.Syntax.link_ref]
@@ -363,7 +363,7 @@ partial def _root_.Verso.Syntax.para.expand : BlockExpander
 def elabLi (block : Syntax) : DocElabM (Syntax × TSyntax `term) :=
   withRef block <|
   match block with
-  | `(list_item|*%$dot $contents:inline*) => do
+  | `(list_item|*%$dot $contents:block*) => do
     let item ← ``(ListItem.mk #[$[$(← contents.mapM elabBlock)],*])
     pure (dot, item)
   | _ =>

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

@@ -488,7 +488,7 @@ unsafe def partCommandsForUnsafe (x : Name) : PartElabM (Array PartCommand) := d
 opaque partCommandsFor (x : Name) : PartElabM (Array PartCommand)
 
 
-abbrev RoleExpander := Array Arg → Array Syntax → DocElabM (Array (TSyntax `term))
+abbrev RoleExpander := Array Arg → TSyntaxArray `inline → DocElabM (Array (TSyntax `term))
 
 initialize roleExpanderAttr : KeyedDeclsAttribute RoleExpander ←
   mkDocExpanderAttribute `role_expander ``RoleExpander "Indicates that this function is used to implement a given role" `roleExpanderAttr
@@ -515,7 +515,7 @@ opaque codeBlockExpandersFor (x : Name) : DocElabM (Array CodeBlockExpander)
 
 
 
-abbrev DirectiveExpander := Array Arg → Array Syntax → DocElabM (Array (TSyntax `term))
+abbrev DirectiveExpander := Array Arg → TSyntaxArray `block → DocElabM (Array (TSyntax `term))
 
 initialize directiveExpanderAttr : KeyedDeclsAttribute DirectiveExpander ←
   mkDocExpanderAttribute `directive_expander ``DirectiveExpander "Indicates that this function is used to implement a given directive" `directiveExpanderAttr