refactor: use parser restarting API instead of whitespace padding

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
 ```
 ```
-<p> a b c </p>
+<p> a b c  </p>
 ```
 :::
 
@@ -690,7 +692,7 @@ A description item is a line that starts with zero or more spaces, followed by a
 
     <dt>  Item 2 </dt>
   <dd>
-    <p> Description of item 2 </p>
+    <p> Description of item 2  </p>
   </dd>
    </dl>
 ```
@@ -729,7 +731,7 @@ But not this one.
   <p> So is this one. </p>
 </blockquote>
 
-<p> But not this one. </p>
+<p> But not this one.  </p>
 ```
 :::
 
@@ -941,6 +943,7 @@ Hyperlinks consist of the link text in square brackets followed by the target in
   <a href="https://lean-lang.org">
     Lean
   </a>
+
 </p>
 ```
 :::
@@ -987,7 +990,9 @@ This makes it possible to represent values that begin or end with back-ticks:
 `` `quotedName ``
 ```
 ```
-<p> <code>"`quotedName"</code> </p>
+<p>
+  <code>"`quotedName"</code>
+</p>
 ```
 :::
 or with spaces:
@@ -996,7 +1001,9 @@ or with spaces:
 ``  one space  ``
 ```
 ```
-<p> <code>" one space "</code> </p>
+<p>
+  <code>" one space "</code>
+</p>
 ```
 :::
 
@@ -1011,6 +1018,7 @@ Images require both alternative text and an address for the image:
   <img
     src="image.png"
     alt="Alt text"/>
+
 </p>
 ```
 :::
@@ -1057,6 +1065,7 @@ $`\frac{1}{2}`-powered syntax]
     <math contents="\\frac{1}{2}"/>
     -powered syntax
   </ref>
+
 </p>
 ```
 :::
@@ -1071,6 +1080,7 @@ This one takes a single inline code element without needing square brackets:
   <lean >
     <code>"2 + f 4"</code>
   </lean>
+
 </p>
 ```
 :::

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)
+open Verso.SyntaxUtils (inputContextFromStrLit)
 
 open SubVerso.Examples (loadExamples Example)
 open SubVerso.Examples.Messages (messagesMatch)
@@ -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
@@ -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
@@ -447,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
@@ -457,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
@@ -471,12 +494,15 @@ 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 := Parser.mkInputContext (← parserInputString str) (← getFileName)
+
+    -- XXX: note state above unused, remove once we verify everything is fine
+    let (pos, context) ← inputContextFromStrLit str
+    let state := { pos }
     -- Process with empty messages to avoid duplicate output
     let s ←
       withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"Elaborating commands") <|
@@ -501,7 +527,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
@@ -607,18 +633,15 @@ def leanInline : 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"
 
     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 :=
@@ -627,7 +650,7 @@ def leanInline : RoleExpanderOf LeanInlineConfig
         Elab.Term.withLevelNames us
       else id
 
-    match Parser.runParserCategory env `term altStr (← getFileName) 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
@@ -637,7 +660,7 @@ def leanInline : 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) with
               | .error e => throwErrorAt str e
               | .ok stx => withEnableInfoTree false do
                 let t ← leveller <| Elab.Term.elabType stx

src/verso-manual/VersoManual/Imports.lean

@@ -31,9 +31,9 @@ Parses, but does not validate, a module header.
 @[code_block]
 def imports : CodeBlockExpanderOf ImportsParams
   | { «show» } , str => do
-    let altStr ← parserInputString str
     let p := Parser.whitespace >> Parser.Module.header.fn
-    let headerStx ← p.parseString altStr
+    -- 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)])

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 (parserInputString runParserCategory' SyntaxError)
+open Verso.SyntaxUtils (inputContextFromStrLit)
 
 open Lean.Doc.Syntax
 open Lean.Elab.Tactic.GuardMsgs
@@ -237,13 +237,13 @@ def elabCommands (config : LeanBlockConfig) (str : StrLit)
     let origScopes := origScopes.modifyHead fun sc =>
       { sc with opts := pp.tagAppFns.set (Elab.async.set sc.opts false) true }
 
-    let altStr ← parserInputString str
+    let (pos, ictx) ← inputContextFromStrLit str
 
-    let ictx := Parser.mkInputContext altStr (← getFileName)
-    let cctx : Command.Context := { fileName := ← getFileName, fileMap := FileMap.ofString altStr, snap? := none, cancelTk? := none}
+    let fileMap ← getFileMap
+    let cctx : Command.Context := { fileName := ← getFileName, fileMap, snap? := none, cancelTk? := none}
 
     let mut cmdState : Command.State := {env := ← getEnv, maxRecDepth := ← MonadRecDepth.getMaxRecDepth, scopes := origScopes}
-    let mut pstate := {pos := 0, recovering := false}
+    let mut pstate := {pos}
     let mut cmds := #[]
 
     repeat
@@ -346,8 +346,6 @@ Elaborates the provided Lean term in the context of the current Verso module.
 def leanTerm : CodeBlockExpanderOf LeanInlineConfig
   | config, str => withoutAsync <| do
 
-    let altStr ← parserInputString str
-
     let leveller :=
       if let some us := config.universes then
         let us :=
@@ -356,7 +354,7 @@ def leanTerm : CodeBlockExpanderOf LeanInlineConfig
         Elab.Term.withLevelNames us
       else id
 
-    match Parser.runParserCategory (← getEnv) `term altStr (← getFileName) with
+    match (← SyntaxUtils.runParserCategory `term str) with
     | .error e => throwErrorAt str e
     | .ok stx =>
       let (newMsgs, tree) ← do
@@ -365,15 +363,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
@@ -423,7 +421,6 @@ def leanInline : RoleExpanderOf LeanInlineConfig
       | throwError "Expected exactly one argument"
     let `(inline|code( $term:str )) := arg
       | throwErrorAt arg "Expected code literal with the example name"
-    let altStr ← parserInputString term
 
     let leveller :=
       if let some us := config.universes then
@@ -433,7 +430,7 @@ def leanInline : RoleExpanderOf LeanInlineConfig
         Elab.Term.withLevelNames us
       else id
 
-    match Parser.runParserCategory (← getEnv) `term altStr (← getFileName) with
+    match (← SyntaxUtils.runParserCategory `term term) with
     | .error e => throwErrorAt term e
     | .ok stx =>
 
@@ -443,15 +440,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
@@ -514,9 +511,8 @@ def inst : RoleExpanderOf LeanBlockConfig
       | throwError "Expected exactly one argument"
     let `(inline|code( $term:str )) := arg
       | throwErrorAt arg "Expected code literal with the example name"
-    let altStr ← parserInputString term
 
-    match Parser.runParserCategory (← getEnv) `term altStr (← getFileName) with
+    match (← SyntaxUtils.runParserCategory `term term) with
     | .error e => throwErrorAt term e
     | .ok stx =>
       let (newMsgs, tree) ← do

src/verso-manual/VersoManual/InlineLean/Signature.lean

@@ -15,7 +15,6 @@ open SubVerso.Highlighting
 open Verso Genre Manual ArgParse Doc Elab
 open Verso Output Html
 open Verso Code Highlighted WebAssets
-open Verso.SyntaxUtils
 open Lean Elab
 
 namespace Verso.Genre.Manual.InlineLean
@@ -59,11 +58,9 @@ end
 @[code_block]
 def signature : CodeBlockExpanderOf SignatureConfig
   | {«show»}, str => withoutAsync do
-    let altStr ← parserInputString str
     let col? := (← getRef).getPos? |>.map (← getFileMap).utf8PosToLspPos |>.map (·.character)
 
-
-    match Parser.runParserCategory (← getEnv) `signature_spec altStr (← getFileName) with
+    match (← SyntaxUtils.runParserCategory `signature_spec str) with
     | .error e => throwError e
     | .ok stx =>
       let `(signature_spec|$[$kw]? $name:declId $sig:declSig) := stx