[#15064] feat: rewrite the Verso docstring parser to produce accurate syntax

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-09-06
+leanprover/lean4-pr-releases:pr-release-15064-5132248

mathlib4/Mathlib/Tactic/Linter/DocString.lean

@@ -92,7 +92,7 @@ def checkVersoSyntax (docComment : String) (fileName : Option String := none) :
     openDecls := (← getOpenDecls)
   }
   let s := mkParserState docComment
-  let s := Doc.Parser.document.run ictx pmctx (getTokenTable env) s
+  let s := (Doc.Parser.documentFn {}).run ictx pmctx (getTokenTable env) s
   return s.allErrors
 
 /--

mathlib4/MathlibTest/Linter/DocString.lean

@@ -164,7 +164,7 @@ example : Nat := 0
 
 -- Errors on underscores, but not when they appear in a URL:
 /--
-warning: expected '_' without preceding space
+warning: unterminated emphasis; expected '_'
 
 Note: This linter can be disabled with `set_option linter.style.docStringVerso false`
 -/
@@ -181,7 +181,19 @@ warning: expected identifier
 
 Note: This linter can be disabled with `set_option linter.style.docStringVerso false`
 ---
-warning: unexpected end of input; expected '![', '$$', '$', '*', '[', '[^', '_', '`' or '{'
+warning: expected identifier
+
+Note: This linter can be disabled with `set_option linter.style.docStringVerso false`
+---
+warning: unexpected ' '; expected '![', '$$', '$', '*', '[', '[^', '_', '`' or '{'
+
+Note: This linter can be disabled with `set_option linter.style.docStringVerso false`
+---
+warning: expected identifier
+
+Note: This linter can be disabled with `set_option linter.style.docStringVerso false`
+---
+warning: unexpected ' '; expected '![', '$$', '$', '*', '[', '[^', '_', '`' or '{'
 
 Note: This linter can be disabled with `set_option linter.style.docStringVerso false`
 -/
@@ -198,7 +210,19 @@ warning: expected identifier
 
 Note: This linter can be disabled with `set_option linter.style.docStringVerso false`
 ---
-warning: unexpected end of input; expected '![', '$$', '$', '*', '[', '[^', '_', '`' or '{'
+warning: expected identifier
+
+Note: This linter can be disabled with `set_option linter.style.docStringVerso false`
+---
+warning: unexpected ' '; expected '![', '$$', '*', '[', '[^', '_', '`', '{' or backticks to open inline code
+
+Note: This linter can be disabled with `set_option linter.style.docStringVerso false`
+---
+warning: expected identifier
+
+Note: This linter can be disabled with `set_option linter.style.docStringVerso false`
+---
+warning: unexpected ' '; expected '![', '$$', '*', '[', '[^', '_', '`', '{' or backticks to open inline code
 
 Note: This linter can be disabled with `set_option linter.style.docStringVerso false`
 -/

reference-manual/Manual/Meta.lean

@@ -48,8 +48,8 @@ open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets
 open SubVerso.Highlighting Highlighted
 open Lean Elab
 open Lean.Elab.Tactic.GuardMsgs
+open Lean.Doc (CodeView CodeBlockView)
 
-open scoped Lean.Doc.Syntax
 
 namespace Manual
 
@@ -71,18 +71,22 @@ def commentDirective : DirectiveExpander
 -- These are part commands rather than block expanders so that it can be used in contexts where
 -- block content doesn't fit, like right after an include. However, the blocks are still needed
 -- for contexts where part commands aren't run.
-@[part_command Lean.Doc.Syntax.codeblock, part_command Lean.Doc.Syntax.directive]
+@[part_command Lean.Doc.Parser.Block.codeblock, part_command Lean.Doc.Parser.Block.directive]
 def commentBlock : PartCommand
-  | `(block| ::: $commentId $_* { $_* } )
-  | `(block| ``` $commentId $_* | $_ ``` ) => do
+  | v => do
+    let some commentId :=
+      (match v with
+       | .directive d => some d.name
+       | .codeblock c => c.name?
+       | _ => none)
+      | throwUnsupportedSyntax
     try
       let n ← realizeGlobalConstNoOverloadWithInfo commentId
       if n == ``comment then
         return ()
       else
         throwUnsupportedSyntax
     catch | _ => throwUnsupportedSyntax
-  | _ => throwUnsupportedSyntax
 
 
 
@@ -351,9 +355,9 @@ def ctype : RoleExpander
     ArgParse.done.run args
     let #[x] := contents
       | throwError "Expected exactly one parameter"
-    let `(inline|code($t)) := x
+    let some { content := t, .. } := CodeView.of x
       | throwError "Expected exactly one code item"
-    pure #[← ``(Inline.code $(quote t.getString))]
+    pure #[← ``(Inline.code $(quote t.getVersoCode))]
 
 def Inline.ckw : Inline where
   name := `Manual.ckw
@@ -367,9 +371,9 @@ def ckw : RoleExpander
     ArgParse.done.run args
     let #[x] := contents
       | throwError "Expected exactly one parameter"
-    let `(inline|code($t)) := x
+    let some { content := t, .. } := CodeView.of x
       | throwError "Expected exactly one code item"
-    pure #[← ``(Inline.code $(quote t.getString))]
+    pure #[← ``(Inline.code $(quote t.getVersoCode))]
 
 @[inline_extension ckw]
 def ckw.descr : InlineDescr where
@@ -392,10 +396,10 @@ def ffi : DirectiveExpander
     else
       let firstBlock := blocks[0]
       let moreBlocks := blocks.extract 1 blocks.size
-      let `(block|``` | $contents ```) := firstBlock
+      let some { name? := none, content := contents, .. } := CodeBlockView.of firstBlock
         | throwErrorAt firstBlock "Expected code block"
       let body ← moreBlocks.mapM elabBlock
-      pure #[← `(Block.other {Block.ffi with data := ToJson.toJson ($(quote config.name), $(quote config.kind), $(quote contents.getString))} #[$body,*])]
+      pure #[← `(Block.other {Block.ffi with data := ToJson.toJson ($(quote config.name), $(quote config.kind), $(quote contents.getVersoCodeBlock))} #[$body,*])]
 
 @[block_extension ffi]
 def ffi.descr : BlockDescr where

reference-manual/Manual/Meta/Attribute.lean

@@ -18,13 +18,13 @@ open Verso.ArgParse
 open Verso.Code (highlightingJs)
 open Verso.Code.Highlighted.WebAssets
 
-open scoped Lean.Doc.Syntax
 
 
 open Lean Elab Parser
 open Lean.Widget (TaggedText)
 open SubVerso.Highlighting
 open Verso.Code
+open Lean.Doc (CodeView)
 
 namespace Manual
 
@@ -64,22 +64,22 @@ def attr : RoleExpander
     let () ← ArgParse.done.run args
     let #[arg] := inlines
       | throwError "Expected exactly one argument"
-    let `(inline|code( $a:str )) := arg
+    let some { content := a, .. } := CodeView.of arg
       | throwErrorAt arg "Expected code literal with the attribute"
     let altStr ← parserInputString a
 
     match Parser.runParserCategory (← getEnv) `attr altStr (← getFileName) with
     | .error e =>
       -- Attributes whose syntax requires arguments (e.g. `export`) don't parse from their bare name.
       -- When the name is a leading token, refer to that syntax and link to its docs.
-      match attrSyntaxKind? (← getEnv) a.getString with
+      match attrSyntaxKind? (← getEnv) a.getVersoCode with
       | some kind =>
         let kindDoc ← findDocString? (← getEnv) kind
         pure #[← `(Verso.Doc.Inline.other { Inline.keywordOf with
           data :=
             ToJson.toJson (α := String × Option Name × Name × Option String)
-              ($(quote a.getString), $(quote (some `attr)), $(quote kind), $(quote kindDoc))
-        } #[Verso.Doc.Inline.code $(quote a.getString)])]
+              ($(quote a.getVersoCode), $(quote (some `attr)), $(quote kind), $(quote kindDoc))
+        } #[Verso.Doc.Inline.code $(quote a.getVersoCode)])]
       | none => throwErrorAt a e
     | .ok stx =>
       let attrName ←
@@ -93,7 +93,7 @@ def attr : RoleExpander
       match getAttributeImpl (← getEnv) attrName with
       | .error e => throwErrorAt a e
       | .ok {descr, name, ref, ..} => do
-        let attrTok := a.getString
+        let attrTok := a.getVersoCode
         let hl : Highlighted := attrToken ref descr attrTok
         try
           -- Attempt to add info to the document source for go-to-def and the like, but this doesn't
@@ -139,7 +139,7 @@ def attrs : RoleExpander
     let () ← ArgParse.done.run args
     let #[arg] := inlines
       | throwError "Expected exactly one argument"
-    let `(inline|code( $a:str )) := arg
+    let some { content := a, .. } := CodeView.of arg
       | throwErrorAt arg "Expected code literal with the attribute application syntax"
     let altStr ← parserInputString a
 
@@ -183,7 +183,7 @@ def attrs : RoleExpander
         catch _ =>
           pure ()
     hl := .token ⟨.keyword ``Term.attributes none none, "@["⟩ ++ hl ++ .token ⟨.keyword ``Term.attributes none none, "]"⟩
-    pure #[← `(Verso.Doc.Inline.other {Inline.attrs with data := ToJson.toJson $(quote hl)} #[Verso.Doc.Inline.code $(quote a.getString)])]
+    pure #[← `(Verso.Doc.Inline.other {Inline.attrs with data := ToJson.toJson $(quote hl)} #[Verso.Doc.Inline.code $(quote a.getVersoCode)])]
 
 where
   -- TODO: This will eventually generate the right cross-reference, but VersoManual needs to have a

reference-manual/Manual/Meta/Basic.lean

@@ -9,8 +9,10 @@ public import Lean.Syntax
 public import Lean.Environment
 public import Lean.Parser.Types
 public import Lean.Elab.Command
+public import Lean.DocString.View
 import Lean.Parser
 
+public import Verso.Literal
 import Verso.Parser
 import Verso.Doc.ArgParse
 import SubVerso.Highlighting
@@ -19,8 +21,9 @@ open Lean
 
 namespace Manual
 
-public def parserInputString [Monad m] [MonadFileMap m]
-    (str : TSyntax `str) :
+open Verso in
+public def parserInputString [Monad m] [MonadFileMap m] [Literal k]
+    (str : TSyntax k) :
     m String := do
   let text ← getFileMap
   let preString := String.Pos.Raw.extract text.source 0 (str.raw.getPos?.getD 0)
@@ -34,7 +37,7 @@ public def parserInputString [Monad m] [MonadFileMap m]
   let strOriginal? : Option String := do
     let ⟨start, stop⟩ ← str.raw.getRange?
     start.extract text.source stop
-  code := code ++ strOriginal?.getD str.getString
+  code := code ++ strOriginal?.getD (Literal.decode str)
   return code
 
 public structure SyntaxError where
@@ -156,20 +159,30 @@ public def commandWithoutAsync : (act : CommandElabM α) → CommandElabM α :=
 public def withoutAsync [Monad m] [MonadWithOptions m] : (act : m α) → m α :=
   withOptions (Elab.async.set · false)
 
-open scoped Lean.Doc.Syntax in
+open Lean.Doc (CodeBlockView VersoCodeBlock) in
+/--
+The contents of `blk`, if it is a code block that names `name`.
+-/
+public def namedCodeBlock (name : Name) (blk : TSyntax ``Lean.Doc.Parser.block) :
+    Option VersoCodeBlock :=
+  match CodeBlockView.of blk with
+  | some { name? := some n, content, .. } => if n.getId == name then some content else none
+  | _ => none
+
+open Lean.Doc (CodeView VersoCode) in
 /--
 If the array of inlines contains a single code element, it is returned. Otherwise, an error is
 logged and `none` is returned.
 -/
 public def oneCodeStr? [Monad m] [MonadError m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
-    (inlines : Array (TSyntax `inline)) : m (Option StrLit) := do
+    (inlines : TSyntaxArray ``Lean.Doc.Parser.inline) : m (Option VersoCode) := do
   let #[code] := inlines
     | if inlines.size == 0 then
         Lean.logError "Expected a code element"
       else
         logErrorAt (mkNullNode inlines) "Expected one code element"
       return none
-  let `(inline|code($code)) := code
+  let some { content := code, .. } := CodeView.of code
     | logErrorAt code "Expected a code element"
       return none
   return some code

reference-manual/Manual/Meta/ConfigFile.lean

@@ -65,17 +65,17 @@ inline_extension Inline.configFile (filename : String) where
   toTeX := none
 
 open Verso.Doc.Elab
-open Lean.Doc.Syntax
 open Lean
+open Lean.Doc (CodeView)
 
 @[role]
 def configFile : RoleExpanderOf Unit
   | (), inlines => do
     let #[arg] := inlines
       | throwError "Expected exactly one argument"
-    let `(inline|code( $cmdName:str )) := arg
+    let some { content := cmdName, .. } := CodeView.of arg
       | throwErrorAt arg "Expected code literal with the config file's name"
-    let filename := cmdName.getString
+    let filename := cmdName.getVersoCode
 
     `(show Verso.Doc.Inline Verso.Genre.Manual from
       .other (Manual.Inline.configFile $(quote filename)) #[.code $(quote filename)])

reference-manual/Manual/Meta/CustomStyle.lean

@@ -33,4 +33,4 @@ block_extension Block.customCSS (css : String) where
 @[code_block]
 def customCSS : CodeBlockExpanderOf Unit
   | (), str =>
-    `(Block.other (Block.customCSS $(quote str.getString)) #[])
+    `(Block.other (Block.customCSS $(quote str.getVersoCodeBlock)) #[])

reference-manual/Manual/Meta/ElanCmd.lean

@@ -9,7 +9,7 @@ import Manual.Meta.LakeCmd -- TODO: generalize the common parts into a library t
 open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets
 open Lean Elab
 open SubVerso.Highlighting Highlighted
-open scoped Lean.Doc.Syntax
+open Lean.Doc (CodeView)
 
 namespace Manual
 
@@ -204,9 +204,9 @@ def elanMeta : RoleExpander
     let () ← ArgParse.done.run args
     let #[arg] := inlines
       | throwError "Expected exactly one argument"
-    let `(inline|code( $mName:str )) := arg
+    let some { content := mName, .. } := CodeView.of arg
       | throwErrorAt arg "Expected code literal with the metavariable"
-    let mName := mName.getString
+    let mName := mName.getVersoCode
 
     pure #[← `(show Verso.Doc.Inline Verso.Genre.Manual from .other {Manual.Inline.elanMeta with data := Json.arr #[$(quote mName), .null]} #[Inline.code $(quote mName)])]
 
@@ -240,9 +240,9 @@ def elanInline : RoleExpander
     let () ← ArgParse.done.run args
     let #[arg] := inlines
       | throwError "Expected exactly one argument"
-    let `(inline|code( $cmdName:str )) := arg
+    let some { content := cmdName, .. } := CodeView.of arg
       | throwErrorAt arg "Expected code literal with the Elan command name"
-    let name := cmdName.getString
+    let name := cmdName.getVersoCode
 
     pure #[← `(show Verso.Doc.Inline Verso.Genre.Manual from .other {Manual.Inline.elan with data := $(quote name)} #[Inline.code $(quote name)])]
 
@@ -289,10 +289,10 @@ def elanArgs : RoleExpander
     let () ← ArgParse.done.run args
     let #[arg] := inlines
       | throwError "Expected exactly one argument"
-    let `(inline|code( $spec:str )) := arg
+    let some { content := spec, .. } := CodeView.of arg
       | throwErrorAt arg "Expected code literal with the Elan command name"
 
-    match Parser.runParserCategory (← getEnv) `lake_cmd_spec spec.getString (← getFileName) with
+    match Parser.runParserCategory (← getEnv) `lake_cmd_spec spec.getVersoCode (← getFileName) with
     | .error e => throwErrorAt spec e
     | .ok stx =>
       match CommandSpec.ofSyntax stx with

reference-manual/Manual/Meta/ElanOpt.lean

@@ -20,8 +20,9 @@ import Manual.Meta.Basic
 
 
 open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets
-open Lean.Doc.Syntax
 open Lean Elab
+open Lean.Doc (CodeView)
+
 namespace Manual
 
 inductive ElanOptKind where
@@ -84,9 +85,9 @@ def elanOptDef : RoleExpander
     let {kind} ← ElanOptDefOpts.parse.run args
     let #[arg] := inlines
       | throwError "Expected exactly one argument"
-    let `(inline|code( $name:str )) := arg
+    let some { content := name, .. } := CodeView.of arg
       | throwErrorAt arg "Expected code literal with the option or flag"
-    let origName := name.getString
+    let origName := name.getVersoCode
     let name := origName.takeWhile fun c => c == '-' || c.isAlphanum
     let name := name.copy
     let valMeta := origName.drop name.length |>.dropWhile fun (c : Char) => !c.isAlphanum
@@ -143,12 +144,12 @@ def elanOpt : RoleExpander
     let () ← ArgParse.done.run args
     let #[arg] := inlines
       | throwError "Expected exactly one argument"
-    let `(inline|code( $name:str )) := arg
+    let some { content := name, .. } := CodeView.of arg
       | throwErrorAt arg "Expected code literal with the option or flag"
-    let optName := name.getString.takeWhile fun c => c == '-' || c.isAlphanum
+    let optName := name.getVersoCode.takeWhile fun c => c == '-' || c.isAlphanum
     let optName := optName.copy
 
-    pure #[← `(show Verso.Doc.Inline Verso.Genre.Manual from .other (Manual.Inline.elanOpt $(quote optName) $(quote name.getString)) #[Inline.code $(quote name.getString)])]
+    pure #[← `(show Verso.Doc.Inline Verso.Genre.Manual from .other (Manual.Inline.elanOpt $(quote optName) $(quote name.getVersoCode)) #[Inline.code $(quote name.getVersoCode)])]
 
 @[inline_extension elanOpt]
 def elanOpt.descr : InlineDescr where