From 1ff84d285577a4cbb75d38cf00f5ce521706d03b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Feb 2026 15:59:58 +0100 Subject: [PATCH 1/4] refactor: use Verso's runParserCategory function for string parsing This is a step towards removing `parserInputString`. Upstream `runParserCategory` always starts at `pos := 0` Another option would be to update the upstream function to take this into account, but the idea is that the function will evolve to take a string literal so it should be able to compute the position by itself. I made the types different (the Verso one is monadic) as to help avoid confusion, and increase programming ergonomics. Note that we don't change the parts `in VersoManual.Docstring` as these are code strings that come from the `MD4Lean` and they don't have an attached location. --- src/verso-blog/VersoBlog.lean | 4 +- src/verso-manual/VersoManual/InlineLean.lean | 2 +- .../VersoManual/InlineLean/SyntaxError.lean | 5 +- src/verso/Verso/SyntaxUtils.lean | 71 +++++++++---------- 4 files changed, 39 insertions(+), 43 deletions(-) diff --git a/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean index 83fbfb7ce..b20441339 100644 --- a/src/verso-blog/VersoBlog.lean +++ b/src/verso-blog/VersoBlog.lean @@ -626,7 +626,7 @@ private def leanInlineImpl : RoleExpanderOf LeanInlineConfig Elab.Term.withLevelNames us else id - match Parser.runParserCategory env `term altStr (← getFileName) with + match (← SyntaxUtils.runParserCategory `term altStr) with | .error e => throwErrorAt str e | .ok stx => withOptions (fun _ => opts) <| runWithOpenDecls scopes <| runWithVariables scopes fun _ => do let (newMsgs, type, tree) ← do @@ -636,7 +636,7 @@ private def leanInlineImpl : RoleExpanderOf LeanInlineConfig let (tree', t) ← do let expectedType ← config.type.mapM fun (s : StrLit) => do - match Parser.runParserCategory env `term s.getString (← getFileName) with + match (← SyntaxUtils.runParserCategory `term s.getString) with | .error e => throwErrorAt str e | .ok stx => withEnableInfoTree false do let t ← leveller <| Elab.Term.elabType stx diff --git a/src/verso-manual/VersoManual/InlineLean.lean b/src/verso-manual/VersoManual/InlineLean.lean index ac367ccdb..2b1dd136f 100644 --- a/src/verso-manual/VersoManual/InlineLean.lean +++ b/src/verso-manual/VersoManual/InlineLean.lean @@ -28,7 +28,7 @@ open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets Expect open Lean Elab open SubVerso.Highlighting -open Verso.SyntaxUtils (runParserCategory' SyntaxError parseStrLitAsCategory strLitInputContext) +open Verso.SyntaxUtils (SyntaxError parseStrLitAsCategory strLitInputContext) open Lean.Doc.Syntax open Lean.Elab.Tactic.GuardMsgs diff --git a/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean b/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean index 73c57c6de..42da2476e 100644 --- a/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean +++ b/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean @@ -16,7 +16,7 @@ open SubVerso.Highlighting open Verso Genre Manual ArgParse Doc Elab open Verso Output Html open Verso Code Highlighted WebAssets -open Verso.SyntaxUtils +open Verso.SyntaxUtils (SyntaxError) open Lean Elab namespace Verso.Genre.Manual.InlineLean @@ -140,7 +140,8 @@ def syntaxError : CodeBlockExpanderOf SyntaxErrorConfig (detail? := some "Syntax error") let s := str.getString - match runParserCategory' (← getEnv) (← getOptions) config.category s with + let errorFn := SyntaxUtils.runParserCategory.toSyntaxErrors + match (← SyntaxUtils.runParserCategoryGen (errorFn := errorFn) config.category s) with | .ok stx => throwErrorAt str m!"Expected a syntax error for category {config.category}, but got {indentD stx}" | .error es => diff --git a/src/verso/Verso/SyntaxUtils.lean b/src/verso/Verso/SyntaxUtils.lean index 72cde7b02..dd4dfae22 100644 --- a/src/verso/Verso/SyntaxUtils.lean +++ b/src/verso/Verso/SyntaxUtils.lean @@ -186,7 +186,6 @@ deriving ToJson, FromJson, BEq, Repr, Quote -- Based on mkErrorMessage used in Lean upstream - keep them in synch for best UX -open Lean.Parser in private partial def mkSyntaxError (c : InputContext) (pos : String.Pos.Raw) (stk : SyntaxStack) (e : Parser.Error) : SyntaxError := Id.run do let mut pos := pos let mut endPos? := none @@ -270,48 +269,44 @@ actual string contents. public def parseStrLitAsCategory [Monad m] [MonadLog m] [MonadEnv m] [MonadOptions m] [MonadError m] [AddMessageContext m] (catName : Name) (input : StrLit) : m Syntax := parseStrLitWith (andthenFn whitespace (categoryParserFnImpl catName)) input -open Lean.Parser in -/-- -Runs a parser category, returning any errors encountered as a list of position-string pairs. +-- Default from upstream +public def runParserCategory.toErrorMsg (ictx : InputContext) (s : ParserState) := + s.toErrorMsg ictx + +-- Unused +public def runParserCategory.toErrorMsgList (ictx : InputContext) (s : ParserState) : List (Position × String) := Id.run do + let mut errs := [] + for (pos, _stk, err) in s.allErrors do + let pos := ictx.fileMap.toPosition pos + errs := (pos, toString err) :: errs + errs.reverse + +-- Used in Manual's syntaxError block +public def runParserCategory.toSyntaxErrors (ictx : InputContext) (s : ParserState) : Array SyntaxError := + s.allErrors.map fun (pos, stk, e) => (mkSyntaxError ictx pos stk e) + +/-- Runs a parser category, returning any errors encountered. It takes +and optional `fileName` as callers in VersoManual/Docstring like to +override it. -/ -public def runParserCategory - (env : Environment) (opts : Lean.Options) (catName : Name) - (input : String) (fileName : String := "") : - Except (List (Position × String)) Syntax := +public def runParserCategoryGen [Monad m] [MonadEnv m] [MonadLog m] [MonadOptions m] + (errorFn : InputContext → ParserState → ε) + (catName : Name) (input : String) (fileName : Option String := none) : m (Except ε Syntax) := do + let fileName ← fileName.getDM getFileName + let env ← getEnv + let options ← getOptions let p := andthenFn whitespace (categoryParserFnImpl catName) let ictx := mkInputContext input fileName - let s := p.run ictx { env, options := opts } (getTokenTable env) (mkParserState input) - if !s.allErrors.isEmpty then - Except.error (toErrorMsg ictx s) + let s := p.run ictx { env, options } (getTokenTable env) (mkParserState input) + pure $ if !s.allErrors.isEmpty then + Except.error (errorFn ictx s) else if ictx.atEnd s.pos then Except.ok s.stxStack.back else - Except.error (toErrorMsg ictx (s.mkError "end of input")) -where - toErrorMsg (ctx : InputContext) (s : ParserState) : List (Position × String) := Id.run do - let mut errs := [] - for (pos, _stk, err) in s.allErrors do - let pos := ctx.fileMap.toPosition pos - errs := (pos, toString err) :: errs - errs.reverse - -open Lean.Parser in -/-- -Runs a parser category, returning any errors encountered as `SyntaxError`s, with the source spans -computed the way Lean does. --/ -public def runParserCategory' (env : Environment) (opts : Lean.Options) (catName : Name) (input : String) (fileName : String := "") : Except (Array SyntaxError) Syntax := - let p := andthenFn whitespace (categoryParserFnImpl catName) - let ictx := mkInputContext input fileName - let s := p.run ictx { env, options := opts } (getTokenTable env) (mkParserState input) - if !s.allErrors.isEmpty then - Except.error <| toSyntaxErrors ictx s - else if ictx.atEnd s.pos then - Except.ok s.stxStack.back - else - Except.error (toSyntaxErrors ictx (s.mkError "end of input")) -where - toSyntaxErrors (ictx : InputContext) (s : ParserState) : Array SyntaxError := - s.allErrors.map fun (pos, stk, e) => (mkSyntaxError ictx pos stk e) + Except.error (errorFn ictx (s.mkError "end of input")) + +public def runParserCategory [Monad m] [MonadEnv m] [MonadLog m] [MonadOptions m] + (catName : Name) (input : String) (fileName : Option String := none) : m (Except String Syntax) := + runParserCategoryGen runParserCategory.toErrorMsg catName input fileName end Verso.SyntaxUtils From f916aa8ef3cdf1d007f6af5513fd94884a114cff Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 5 Feb 2026 21:01:40 +0100 Subject: [PATCH 2/4] refactor: use parser restarting API instead of whitespace padding This is possible after https://github.com/leanprover/lean4/pull/10043 improved upstream parsing API. This replaces the current use of `parserInputString`, which pads the input, and seems clearer overall. There are two main cases for string literals for us to process: - string literals coming from Verso: in this case, `.getPos` and `.getTailPos` do provide the correct start / end of the string, without the quotes. - string literals coming from Lean: in this case, we must account for the quotes and fixup the positions. We have handled this by convention, but `VersoUtils.parseString` takes an optional parameter as it is used in both modes. Eventually we'd like to move Verso-style strings to its own type instead of `StrLit`. Notes: - I couldn't port `VersoBlog.leanInit` as `Parser.parseHeader` always parses from `pos := 0`. This is the last blocker to completely remove `parserInputString`. - In general, it seems like most functions using `mkParserState` upstream could benefit from an update to take positions. - Tests in `UsersGuide.Markup` had to be adapted due to use of `contents.getString.trimAsciiEnd.copy`. I did this to pass CI, must implement a better fix before merging. - Code that depends on MD4Lean hasn't been ported as MD4 doesn't seem to provide the right API for us. - TODO: we should test `canonical := true` and quoting properly. Note special cases such as `` `code `` --- doc/UsersGuide/Markup.lean | 24 +++-- src/verso-blog/VersoBlog.lean | 32 +++++-- src/verso-manual/VersoManual/InlineLean.lean | 12 +-- .../VersoManual/InlineLean/SyntaxError.lean | 4 +- src/verso/Verso/Parser.lean | 8 +- src/verso/Verso/SyntaxUtils.lean | 89 +++++++++++-------- 6 files changed, 105 insertions(+), 64 deletions(-) diff --git a/doc/UsersGuide/Markup.lean b/doc/UsersGuide/Markup.lean index af6ab13f6..023068077 100644 --- a/doc/UsersGuide/Markup.lean +++ b/doc/UsersGuide/Markup.lean @@ -291,7 +291,9 @@ def markupPreview : DirectiveExpanderOf MarkupPreviewConfig let `(block|``` | $expected ```) := blk2 | throwErrorAt blk1 "Expected anonymous code block" - let stx ← blocks {} |>.parseString contents.getString.trimAsciiEnd.copy +-- XXX Fixme due to trimAsciiEnd +-- let stx ← blocks {} |>.parseString contents.getString.trimAsciiEnd.copy + let stx ← blocks {} |>.parseString contents (versoStyle := true) let p ← preview stx let p := p.pretty (width := 35) @@ -327,7 +329,7 @@ open Verso.Parser in def markupPreviewPre : CodeBlockExpanderOf MarkupPreviewConfig | {title}, contents => do - let stx ← blocks {} |>.parseString contents.getString + let stx ← blocks {} |>.parseString contents (versoStyle := true) let p ← preview stx let p := p.pretty (width := 35) @@ -430,7 +432,7 @@ Metadata blocks begin and end with `%%%`, and they contain any syntax that would a b c ``` ``` -

a b c

+

a b c

``` ::: @@ -690,7 +692,7 @@ A description item is a line that starts with zero or more spaces, followed by a
Item 2
-

Description of item 2

+

Description of item 2

``` @@ -729,7 +731,7 @@ But not this one.

So is this one.

-

But not this one.

+

But not this one.

``` ::: @@ -941,6 +943,7 @@ Hyperlinks consist of the link text in square brackets followed by the target in Lean +

``` ::: @@ -987,7 +990,9 @@ This makes it possible to represent values that begin or end with back-ticks: `` `quotedName `` ``` ``` -

"`quotedName"

+

+ "`quotedName" +

``` ::: or with spaces: @@ -996,7 +1001,9 @@ or with spaces: `` one space `` ``` ``` -

" one space "

+

+ " one space " +

``` ::: @@ -1011,6 +1018,7 @@ Images require both alternative text and an address for the image: Alt text +

``` ::: @@ -1057,6 +1065,7 @@ $`\frac{1}{2}`-powered syntax] -powered syntax +

``` ::: @@ -1071,6 +1080,7 @@ This one takes a single inline code element without needing square brackets: "2 + f 4" +

``` ::: diff --git a/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean index b20441339..6092b9397 100644 --- a/src/verso-blog/VersoBlog.lean +++ b/src/verso-blog/VersoBlog.lean @@ -29,7 +29,7 @@ namespace Verso.Genre.Blog open Lean.Doc.Syntax open Verso ArgParse Doc Elab open Lean Elab -open Verso.SyntaxUtils (parserInputString strLitInputContext) +open Verso.SyntaxUtils (inputContextFromStrLit strLitInputContext) open SubVerso.Examples (loadExamples Example) open SubVerso.Examples.Messages (messagesMatch) @@ -434,9 +434,32 @@ instance [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadErr .flag `showProofStates true "Show proof states in rendered page?" +def parserInputString [Monad m] [MonadFileMap m] + (str : TSyntax `str) : + m String := do + let text ← getFileMap + let preString := (0 : String.Pos.Raw).extract text.source (str.raw.getPos?.getD 0) + let mut code := "" + let mut iter := preString.startPos + while h : iter ≠ preString.endPos do + let c := iter.get h + iter := iter.next h + if c == '\n' then + code := code.push '\n' + else + for _ in [0:c.utf8Size] do + code := code.push ' ' + let strOriginal? : Option String := do + let ⟨start, stop⟩ ← str.raw.getRange? + start.extract text.source stop + code := code ++ strOriginal?.getD str.getString + return code + @[code_block] def leanInit : CodeBlockExpanderOf LeanInitBlockConfig | config , str => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"leanInit") <| do + -- XXX [upstream]: can't use pos here due to `Parser.parseHeader` type + let (_pos, _context) ← inputContextFromStrLit str let context := Parser.mkInputContext (← parserInputString str) (← getFileName) let (header, state, msgs) ← Parser.parseHeader context if !header.raw[0].isNone then @@ -615,9 +638,6 @@ private def leanInlineImpl : RoleExpanderOf LeanInlineConfig let {env, scopes, ngen, ..} := commandState let {openDecls, currNamespace, opts, ..} := scopes.head! - - let altStr ← parserInputString str - let leveller {α} : TermElabM α → TermElabM α := if let some us := config.universes then let us := @@ -626,7 +646,7 @@ private def leanInlineImpl : RoleExpanderOf LeanInlineConfig Elab.Term.withLevelNames us else id - match (← SyntaxUtils.runParserCategory `term altStr) with + match (← SyntaxUtils.runParserCategory `term str) with | .error e => throwErrorAt str e | .ok stx => withOptions (fun _ => opts) <| runWithOpenDecls scopes <| runWithVariables scopes fun _ => do let (newMsgs, type, tree) ← do @@ -636,7 +656,7 @@ private def leanInlineImpl : RoleExpanderOf LeanInlineConfig let (tree', t) ← do let expectedType ← config.type.mapM fun (s : StrLit) => do - match (← SyntaxUtils.runParserCategory `term s.getString) with + match (← SyntaxUtils.runParserCategory `term s) with | .error e => throwErrorAt str e | .ok stx => withEnableInfoTree false do let t ← leveller <| Elab.Term.elabType stx diff --git a/src/verso-manual/VersoManual/InlineLean.lean b/src/verso-manual/VersoManual/InlineLean.lean index 2b1dd136f..b256edf93 100644 --- a/src/verso-manual/VersoManual/InlineLean.lean +++ b/src/verso-manual/VersoManual/InlineLean.lean @@ -392,15 +392,15 @@ def leanTerm : CodeBlockExpanderOf LeanInlineConfig Core.resetMessageLog let tree' ← runWithOpenDecls <| runWithVariables fun _vars => do - let expectedType ← config.type.mapM fun (s : StrLit) => do - match Parser.runParserCategory (← getEnv) `term s.getString (← getFileName) with + let expectedType ← config.type.mapM fun (str : StrLit) => do + match (← SyntaxUtils.runParserCategory `term str) with | .error e => throwErrorAt stx e | .ok stx => withEnableInfoTree false do let t ← leveller <| Elab.Term.elabType stx Term.synthesizeSyntheticMVarsNoPostponing let t ← instantiateMVars t if t.hasExprMVar || t.hasLevelMVar then - throwErrorAt s "Type contains metavariables: {t}" + throwErrorAt str "Type contains metavariables: {t}" pure t let e ← Elab.Term.elabTerm (catchExPostpone := true) stx expectedType @@ -469,15 +469,15 @@ def leanInline : RoleExpanderOf LeanInlineConfig Core.resetMessageLog let (tree', t) ← runWithOpenDecls <| runWithVariables fun _ => do - let expectedType ← config.type.mapM fun (s : StrLit) => do - match Parser.runParserCategory (← getEnv) `term s.getString (← getFileName) with + let expectedType ← config.type.mapM fun (str : StrLit) => do + match (← SyntaxUtils.runParserCategory `term str) with | .error e => throwErrorAt term e | .ok stx => withEnableInfoTree false do let t ← leveller <| Elab.Term.elabType stx Term.synthesizeSyntheticMVarsNoPostponing let t ← instantiateMVars t if t.hasExprMVar || t.hasLevelMVar then - throwErrorAt s "Type contains metavariables: {t}" + throwErrorAt str "Type contains metavariables: {t}" pure t let e ← leveller <| Elab.Term.elabTerm (catchExPostpone := true) stx expectedType diff --git a/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean b/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean index 42da2476e..9cc4d3a8c 100644 --- a/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean +++ b/src/verso-manual/VersoManual/InlineLean/SyntaxError.lean @@ -139,9 +139,8 @@ def syntaxError : CodeBlockExpanderOf SyntaxErrorConfig (kind := Lsp.SymbolKind.file) (detail? := some "Syntax error") - let s := str.getString let errorFn := SyntaxUtils.runParserCategory.toSyntaxErrors - match (← SyntaxUtils.runParserCategoryGen (errorFn := errorFn) config.category s) with + match (← SyntaxUtils.runParserCategoryGen (errorFn := errorFn) config.category str) with | .ok stx => throwErrorAt str m!"Expected a syntax error for category {config.category}, but got {indentD stx}" | .error es => @@ -151,6 +150,7 @@ def syntaxError : CodeBlockExpanderOf SyntaxErrorConfig saveOutputs config.name msgs Hover.addCustomHover (← getRef) <| MessageData.joinSep (msgs.map fun ⟨sev, msg⟩ => m!"{sevStr sev.toSeverity}:{indentD msg.toString}") Format.line + let s := str.getString `(Block.other {Block.syntaxError with data := ToJson.toJson ($(quote s), $(quote es))} #[Block.code $(quote s)]) where sevStr : MessageSeverity → String diff --git a/src/verso/Verso/Parser.lean b/src/verso/Verso/Parser.lean index 1b6365461..919513029 100644 --- a/src/verso/Verso/Parser.lean +++ b/src/verso/Verso/Parser.lean @@ -985,13 +985,13 @@ namespace Verso.Doc.Concrete open Verso.Parser open Lean Elab Term -public def stringToInlines [Monad m] [MonadError m] [MonadEnv m] [MonadQuotation m] (s : StrLit) : m (Array Syntax) := +public def stringToInlines [Monad m] [MonadError m] [MonadLog m] [MonadOptions m] [MonadEnv m] [MonadQuotation m] (s : StrLit) : m (Array Syntax) := withRef s do - return (← textLine.parseString s.getString).getArgs + return (← textLine.parseString s).getArgs open Lean Elab Term in -public def stringToBlocks [Monad m] [MonadError m] [MonadEnv m] [MonadQuotation m] (s : StrLit) : m (Array Syntax) := +public def stringToBlocks [Monad m] [MonadError m] [MonadLog m] [MonadOptions m] [MonadEnv m] [MonadQuotation m] (s : StrLit) : m (Array Syntax) := withRef s do - return (← (blocks {}).parseString s.getString).getArgs + return (← (blocks {}).parseString s).getArgs end Verso.Doc.Concrete diff --git a/src/verso/Verso/SyntaxUtils.lean b/src/verso/Verso/SyntaxUtils.lean index dd4dfae22..200e36e77 100644 --- a/src/verso/Verso/SyntaxUtils.lean +++ b/src/verso/Verso/SyntaxUtils.lean @@ -134,6 +134,24 @@ macro_rules | `( ` ) => ``(Syntax.atom _ $e) end +open Syntax in + +/-- Get the inner start/end position of a string literal. + +If the string is coming from Verso, these are the positions stored in the syntax object. Otherwise, +the positions include the surrounding quotes and need to be adjusted. +-/ +def _root_.Lean.TSyntax.innerPos? (str : StrLit) (versoStyle : Bool) : Option (String.Pos.Raw × String.Pos.Raw) := + if versoStyle then + match str.raw.getPos?, str.raw.getTailPos? with + | (some pos), (some endPos) => some (pos, endPos) + | _, _ => none + else + -- TODO: handle raw string literals, e.g. r###"foo"###. + str.raw.getPos? |>.map fun pos => + let startPos := pos.increaseBy 1 + (startPos, startPos.increaseBy str.getString.utf8ByteSize) + /-- Returns an `InputContext` and start position for parsing the contents of a string literal that was part of the original source file. @@ -151,31 +169,23 @@ public def strLitInputContext [Monad m] [MonadFileMap m] [MonadError m] (str : S let ictx := Parser.mkInputContext text.source fileName (endPos := endPos) (endPos_valid := by grind) return (ictx, startPos) -/-- -Given a string literal, constructs a Lean string that can be parsed by the Lean parser, yielding -correct source positions for items in the string literal. --/ -public def parserInputString [Monad m] [MonadFileMap m] - (str : TSyntax `str) : - m String := do - let text ← getFileMap - let preString := (0 : String.Pos.Raw).extract text.source (str.raw.getPos?.getD 0) - let mut code := "" - let mut iter := preString.startPos - while h : iter ≠ preString.endPos do - let c := iter.get h - iter := iter.next h - if c == '\n' then - code := code.push '\n' - else - for _ in [0:c.utf8Size] do - code := code.push ' ' - let strOriginal? : Option String := do - let ⟨start, stop⟩ ← str.raw.getRange? - start.extract text.source stop - code := code ++ strOriginal?.getD str.getString - return code - +/-- Compute a parsing starting position and `InputContext` from an + embedded string literal. This is often used to call Lean's parser + re-entranly. **Precondition**: the string literal must appear in the + source, otherwise the function may panic. -/ +public def inputContextFromStrLit [Monad m] [MonadLog m] [MonadFileMap m] (str : StrLit) (versoStyle : Bool := true) (fileName : Option String := none) : m (String.Pos.Raw × InputContext) := do + -- dbg_trace "{repr str}" + let filename ← fileName.getDM getFileName + let source := (← getFileMap).source + let some (pos, endPos) := str.innerPos? versoStyle + -- XXX: replace by elaborator exception (throwErrorAt) + -- XXX: Gonna fail when users write a bad macro + | panic "invalid string literal on parser resumption (inputContextFromStrLit)" + if endPos_valid : endPos ≤ source.rawEndPos then + let iCtx := mkInputContext source filename (endPos := endPos) (endPos_valid := endPos_valid) + return (pos, iCtx) + else + panic "invalid source code slice on parser resumption, slice goes out of bounds" public structure SyntaxError where pos : Position @@ -183,8 +193,6 @@ public structure SyntaxError where text : String deriving ToJson, FromJson, BEq, Repr, Quote - - -- Based on mkErrorMessage used in Lean upstream - keep them in synch for best UX private partial def mkSyntaxError (c : InputContext) (pos : String.Pos.Raw) (stk : SyntaxStack) (e : Parser.Error) : SyntaxError := Id.run do let mut pos := pos @@ -217,18 +225,21 @@ where if let .original (trailing := trailing) .. := stx.getTailInfo then pure (some trailing) else none -public defmethod ParserFn.parseString [Monad m] [MonadError m] [MonadEnv m] (p : ParserFn) (input : String) : m Syntax := do - let ictx := mkInputContext input "" +-- This parses a regular Lean string, that is to say, positions include the outer quotes +public defmethod ParserFn.parseString [Monad m] [MonadLog m] [MonadOptions m] [MonadError m] [MonadEnv m] (p : ParserFn) (input : StrLit) (versoStyle : Bool := false): m Syntax := do + let (pos, iCtx) ← inputContextFromStrLit input versoStyle let env ← getEnv - let pmctx : ParserModuleContext := {env := env, options := {}} - let s' := p.run ictx pmctx (getTokenTable env) (mkParserState input) + let options ← getOptions + let pmctx : ParserModuleContext := {env, options} + let pst := { mkParserState iCtx.inputString with pos } + let s' := p.run iCtx pmctx (getTokenTable env) pst let stk := s'.stxStack.extract 0 s'.stxStack.size if let some err := s'.errorMsg then throwError err.toString if s'.recoveredErrors.size > 0 then throwError String.intercalate "\n" <| Std.HashSet.toList <| Std.HashSet.ofArray <| s'.recoveredErrors.map fun (p, s, e) => - let err := mkSyntaxError ictx p s e + let err := mkSyntaxError iCtx p s e err.text if h : stk.size ≠ 1 then throwError "Expected single item in parser stack, got {ppStack stk}" @@ -287,17 +298,17 @@ public def runParserCategory.toSyntaxErrors (ictx : InputContext) (s : ParserSta /-- Runs a parser category, returning any errors encountered. It takes and optional `fileName` as callers in VersoManual/Docstring like to -override it. +override it. This expects a Verso String Literal, that is to say, positions don't include the quotes. -/ public def runParserCategoryGen [Monad m] [MonadEnv m] [MonadLog m] [MonadOptions m] (errorFn : InputContext → ParserState → ε) - (catName : Name) (input : String) (fileName : Option String := none) : m (Except ε Syntax) := do - let fileName ← fileName.getDM getFileName + (catName : Name) (input : StrLit) (versoStyle : Bool := true) (fileName : Option String := none) : m (Except ε Syntax) := do let env ← getEnv let options ← getOptions let p := andthenFn whitespace (categoryParserFnImpl catName) - let ictx := mkInputContext input fileName - let s := p.run ictx { env, options } (getTokenTable env) (mkParserState input) + let (pos, ictx) ← inputContextFromStrLit input versoStyle fileName + let pst := { mkParserState ictx.inputString with pos } + let s := p.run ictx { env, options } (getTokenTable env) pst pure $ if !s.allErrors.isEmpty then Except.error (errorFn ictx s) else if ictx.atEnd s.pos then @@ -306,7 +317,7 @@ public def runParserCategoryGen [Monad m] [MonadEnv m] [MonadLog m] [MonadOption Except.error (errorFn ictx (s.mkError "end of input")) public def runParserCategory [Monad m] [MonadEnv m] [MonadLog m] [MonadOptions m] - (catName : Name) (input : String) (fileName : Option String := none) : m (Except String Syntax) := - runParserCategoryGen runParserCategory.toErrorMsg catName input fileName + (catName : Name) (input : StrLit) (versoStyle : Bool := true) (fileName : Option String := none) : m (Except String Syntax) := + runParserCategoryGen runParserCategory.toErrorMsg catName input versoStyle fileName end Verso.SyntaxUtils From 8270570a5a339dfaed08142f947fa18e1fb80a3d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Feb 2026 18:00:02 +0100 Subject: [PATCH 3/4] refactor: remove unused parser state in example's environment extension Only `Command.State` is needed to thread several example blocks. Note that before we used the parsing state resulting from the last code block, so we did resume from an offset that could be potentially much before the current code block. This worked as the string in that case was empty (produced by `parserInputString`), but would have failed once we have reuse of the input source string. --- src/verso-blog/VersoBlog.lean | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean index 6092b9397..6b69a66df 100644 --- a/src/verso-blog/VersoBlog.lean +++ b/src/verso-blog/VersoBlog.lean @@ -196,7 +196,7 @@ where section inductive LeanExampleData where - | inline (commandState : Command.State) (parserState : Parser.ModuleParserState) + | inline (commandState : Command.State) | subproject (loaded : NameSuffixMap Example) | module (positioned : Array ModuleItem) deriving Inhabited @@ -470,7 +470,7 @@ def leanInit : CodeBlockExpanderOf LeanInitBlockConfig if header.raw[1].isNone then -- if the "prelude" option was not set, use the current env let commandState := configureCommandState (← getEnv) {} let commandState := { commandState with scopes := [{ header := "", opts := pp.tagAppFns.set {} true }] } - modifyEnv <| fun env => exampleContextExt.modifyState env fun s => {s with contexts := s.contexts.insert config.exampleContext.getId (.inline commandState state)} + modifyEnv <| fun env => exampleContextExt.modifyState env fun s => {s with contexts := s.contexts.insert config.exampleContext.getId (.inline commandState)} else if header.raw[2].getArgs.isEmpty then let (env, msgs) ← processHeader header opts msgs context 0 @@ -480,7 +480,7 @@ def leanInit : CodeBlockExpanderOf LeanInitBlockConfig liftM (m := IO) (throw <| IO.userError "Errors during import; aborting") let commandState := configureCommandState env {} let commandState := { commandState with scopes := [{ header := "", opts := pp.tagAppFns.set {} true }] } - modifyEnv <| fun env => exampleContextExt.modifyState env fun s => {s with contexts := s.contexts.insert config.exampleContext.getId (.inline commandState state)} + modifyEnv <| fun env => exampleContextExt.modifyState env fun s => {s with contexts := s.contexts.insert config.exampleContext.getId (.inline commandState)} if config.show then ``(Block.code $(quote str.getString)) -- TODO highlighting hack else @@ -494,16 +494,17 @@ open SubVerso.Highlighting Highlighted in def lean : CodeBlockExpanderOf LeanBlockConfig | config, str => withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"lean block") <| withoutAsync do let x := config.exampleContext - let (commandState, state) ← match exampleContextExt.getState (← getEnv) |>.contexts.find? x.getId with - | some (.inline commandState state) => pure (commandState, state) + let commandState ← match exampleContextExt.getState (← getEnv) |>.contexts.find? x.getId with + | some (.inline commandState) => pure (commandState) | some (.subproject ..) => throwErrorAt x "Expected an example context for inline Lean, but found a subproject" | some (.module ..) => throwErrorAt x "Expected an example context for inline Lean, but found a module" | none => throwErrorAt x "Can't find example context" let (context, startPos) ← strLitInputContext str.raw (← getFileName) + let state := { pos := startPos } -- Process with empty messages to avoid duplicate output let s ← withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"Elaborating commands") <| - IO.processCommands context { state with pos := startPos } { commandState with messages.unreported := {} } + IO.processCommands context state { commandState with messages.unreported := {} } for t in s.commandState.infoState.trees do pushInfoTree t @@ -524,7 +525,7 @@ def lean : CodeBlockExpanderOf LeanBlockConfig if config.keep && !config.error then modifyEnv fun env => exampleContextExt.modifyState env fun st => {st with - contexts := st.contexts.insert x.getId (.inline {s.commandState with messages := {} } s.parserState) + contexts := st.contexts.insert x.getId (.inline {s.commandState with messages := {} }) } if let some infoName := config.name then modifyEnv fun env => messageContextExt.modifyState env fun st => {st with @@ -629,8 +630,8 @@ private def leanInlineImpl : RoleExpanderOf LeanInlineConfig let `(inline|code( $str:str )) := code | throwErrorAt code "Expected an inline code element" let x := config.exampleContext - let (commandState, _) ← match exampleContextExt.getState (← getEnv) |>.contexts.find? x.getId with - | some (.inline commandState state) => pure (commandState, state) + let commandState ← match exampleContextExt.getState (← getEnv) |>.contexts.find? x.getId with + | some (.inline commandState) => pure commandState | some (.subproject ..) => throwErrorAt x "Expected an example context for inline Lean, but found a subproject" | some (.module ..) => throwErrorAt x "Expected an example context for inline Lean, but found a module" | none => throwErrorAt x "Can't find example context" From 659135402a1997218260ea77aca846932f0a27df Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Feb 2026 19:39:25 +0100 Subject: [PATCH 4/4] fix for VersoManual.imports --- src/verso-manual/VersoManual/Imports.lean | 3 ++- src/verso/Verso/Parser.lean | 2 ++ src/verso/Verso/SyntaxUtils.lean | 7 +++++++ 3 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/verso-manual/VersoManual/Imports.lean b/src/verso-manual/VersoManual/Imports.lean index ff6ced63b..05aba97bc 100644 --- a/src/verso-manual/VersoManual/Imports.lean +++ b/src/verso-manual/VersoManual/Imports.lean @@ -32,7 +32,8 @@ Parses, but does not validate, a module header. def imports : CodeBlockExpanderOf ImportsParams | { «show» } , str => do let p := Parser.whitespace >> Parser.Module.header.fn - let headerStx ← parseStrLitWith p str + -- Provenance of `str` here is from Verso parser + let headerStx ← p.parseString str (versoStyle := true) let hl ← highlight headerStx #[] {} if «show» then ``(Block.other (Block.lean $(quote hl) {}) #[Block.code $(quote str.getString)]) diff --git a/src/verso/Verso/Parser.lean b/src/verso/Verso/Parser.lean index 919513029..fcf9d0551 100644 --- a/src/verso/Verso/Parser.lean +++ b/src/verso/Verso/Parser.lean @@ -985,6 +985,8 @@ namespace Verso.Doc.Concrete open Verso.Parser open Lean Elab Term +-- Important! Both functions below expect strings in "Lean style", +-- that is to say, with positions including quotes around the string. public def stringToInlines [Monad m] [MonadError m] [MonadLog m] [MonadOptions m] [MonadEnv m] [MonadQuotation m] (s : StrLit) : m (Array Syntax) := withRef s do return (← textLine.parseString s).getArgs diff --git a/src/verso/Verso/SyntaxUtils.lean b/src/verso/Verso/SyntaxUtils.lean index 200e36e77..691108898 100644 --- a/src/verso/Verso/SyntaxUtils.lean +++ b/src/verso/Verso/SyntaxUtils.lean @@ -320,4 +320,11 @@ public def runParserCategory [Monad m] [MonadEnv m] [MonadLog m] [MonadOptions m (catName : Name) (input : StrLit) (versoStyle : Bool := true) (fileName : Option String := none) : m (Except String Syntax) := runParserCategoryGen runParserCategory.toErrorMsg catName input versoStyle fileName +/- This function can be used to check whether string are in Verso + style or in Lean style -/ +public def checkString (str : StrLit) : String := + let s := str.getString + let sz := (str.raw.getTailPos?.getD 0 |>.byteIdx) - str.raw.getPos!.byteIdx + s!"real size: {s.length}, syntax size: {sz}" + end Verso.SyntaxUtils