quickest path from `String` to ``TSyntax `tacticSeq``

Stream: lean4

[Scott Morrison]

Suppose I have a plain old String that I suspect is a tacticSeq. How do I get there (or fail)?

import Lean

def parseAsTacticSeq (S : String) : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq := sorry

(I'm in TacticM, so can cope with whichever monad.)

[Scott Morrison]

(context: I have just captured a "Try this:" message from a MessageLog, and want to generate a new "Try this:", which requires a Syntax. Of course in an ideal world I would not have forgotten the Syntax that went into the original "Try this:", but for now I have...)

[Sebastian Ullrich]

There is no direct API for running a Parser on a string, but runParserCategory is very close - just replace the categoryParserFnImpl call with tacticSeq