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 strLitInputContext)
+open Verso.SyntaxUtils (inputContextFromStrLit strLitInputContext)
 
 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,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
 
@@ -501,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
@@ -606,18 +630,15 @@ 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"
 
     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 +647,7 @@ private def leanInlineImpl : 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
@@ -636,7 +657,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) with
               | .error e => throwErrorAt str e
               | .ok stx => withEnableInfoTree false do
                 let t ← leveller <| Elab.Term.elabType stx

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)])

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
@@ -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

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
@@ -139,8 +139,8 @@ def syntaxError : CodeBlockExpanderOf SyntaxErrorConfig
       (kind := Lsp.SymbolKind.file)
       (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 str) with
     | .ok stx =>
       throwErrorAt str m!"Expected a syntax error for category {config.category}, but got {indentD stx}"
     | .error es =>
@@ -150,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

src/verso/Verso/Parser.lean

@@ -985,13 +985,15 @@ 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) :=
+-- 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.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