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
 ```
 ```
-<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>
 ```
 :::
diff --git a/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean
index 83fbfb7ce..6b69a66df 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)
@@ -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,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"
@@ -615,9 +639,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 +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
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-manual/VersoManual/InlineLean.lean b/src/verso-manual/VersoManual/InlineLean.lean
index ac367ccdb..b256edf93 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
@@ -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 73c57c6de..9cc4d3a8c 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
@@ -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
diff --git a/src/verso/Verso/Parser.lean b/src/verso/Verso/Parser.lean
index 1b6365461..fcf9d0551 100644
--- a/src/verso/Verso/Parser.lean
+++ b/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
diff --git a/src/verso/Verso/SyntaxUtils.lean b/src/verso/Verso/SyntaxUtils.lean
index 72cde7b02..691108898 100644
--- a/src/verso/Verso/SyntaxUtils.lean
+++ b/src/verso/Verso/SyntaxUtils.lean
@@ -134,6 +134,24 @@ macro_rules
   | `( `<low| ~~$e > ) => ``(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,10 +193,7 @@ 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
-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
@@ -218,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 "<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}"
@@ -270,48 +280,51 @@ 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. This expects a Verso String Literal, that is to say, positions don't include the quotes.
 -/
-public def runParserCategory
-    (env : Environment) (opts : Lean.Options) (catName : Name)
-    (input : String) (fileName : String := "<example>") :
-    Except (List (Position × String)) Syntax :=
+public def runParserCategoryGen [Monad m] [MonadEnv m] [MonadLog m] [MonadOptions m]
+  (errorFn : InputContext → ParserState → ε)
+  (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 := opts } (getTokenTable env) (mkParserState input)
-  if !s.allErrors.isEmpty then
-    Except.error (toErrorMsg ictx s)
+  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
     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 := "<example>") : 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 : 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