Double-backtick quotations with other syntax categories/parsers

[Kha]

Currently ``(cat| ...) is not supported, i.e. it can only be used with command/term. I'd like to wait with this change until we have unified the | notation in a single parser supporting dynamic lookups.

It also doesn't work with macro's category inference yet.

[Kha]

On the other hand, it is unlikely to work for categories other than term anyway without a massive number of custom precheck hooks. For example, even if it syntactically already supports command, we will need a custom hook for each non-macro command.

[larsk21]

This would be very helpful when referencing theorems inside tactic quotations. In the example below, there is no check that foo is actually available.

-- inside TacticM
evalTactic (← `(tactic|
  refine foo _ ?_
))