Showing syntax in generated documentation

Stream: lean4

[Raghuram]

I was looking at https://leanprover-community.github.io/mathlib4_docs/Init/Tactics.html and thought it would be nice if instead of showing the generated ParserDescr declarations, it showed the actual syntax of the tactic/etc. being defined. For example, even the direct source code

syntax (name := rewriteSeq) "rewrite " (config)? rwRuleSeq (location)? : tactic

is (seems to be?) more useful than def Lean.Parser.Tactic.rewriteSeq : Lean.ParserDescr.

Is this plausible/desirable/feasible?

[Henrik Böving]

If it is possible right now I do not know how to do it (otherwise I would already have done it). That does however not mean it cannot be done. The elaborator for these syntax declarations would have to store the information about the original syntax somewhere :tm: so doc-gen can fetch it.

[Gabriel Ebner]

The ParserDescr definitions are easy to parse, there's no need to keep the original syntax around.

[Henrik Böving]

Should we have delaborators for ParserDescr then?

[Henrik Böving]

So i started on this:

import Lean

open Lean PrettyPrinter

abbrev StxUnexpander := TSyntax `term → UnexpandM (TSyntax `stx)
def unexpandCat : StxUnexpander
  | `(ParserDescr.cat $cat $prec) =>
    let prec : TSyntax `prec := ⟨prec.raw⟩
    `(stx| $cat:$prec)
  | _ => throw ()

But I'm running into the issue that Lean does not like the antiquotations this way of course because they could also be interpreted as "$cat with this stx category". Is there a way to create this syntax node nicely none the less? Or do I have to write some manual Syntax.node stuff here?

[Sebastian Ullrich]

You can work around that by making the kind of the first antiquotation explicit

$cat:ident:$prec