Constructing `docComment`

Stream: metaprogramming / tactics

[Leni Aniva]

How can I programmatically construct a TSyntax Lean.Parser.Command.docComment`?

Is the only option to use Parser.runParserCategory?

[Chris Bailey]

I remember seeing this defined in a package:

def Lean.mkDocComment (s : String) :=
  mkNode ``Parser.Command.docComment #[mkAtom "/--", mkAtom (s ++ "-/")]

/- Lean.mkDocComment "some text" : Lean.TSyntax `Lean.Parser.Command.docComment -/
#check Lean.mkDocComment "some text"

[Leni Aniva]

Chris Bailey said:

I remember seeing this defined in a package:

def Lean.mkDocComment (s : String) :=
  mkNode ``Parser.Command.docComment #[mkAtom "/--", mkAtom (s ++ "-/")]

/- Lean.mkDocComment "some text" : Lean.TSyntax `Lean.Parser.Command.docComment -/
#check Lean.mkDocComment "some text"

This seems to work well! Thanks!