Parser in another category breaks antiquotations

Stream: lean4 dev

[Wojciech Nawrocki]

The following example does not work. We get an error on the $(.

declare_syntax_cat mycat
syntax "$(" term ")" : mycat

syntax "abc" : term
macro_rules
  | `(term| abc) => `(term| $(Lean.Syntax.mkStrLit "abc") ) -- expected term

In my current mental model of extensible syntax, this should work because the new $( syntax lies in its own category mycat so when we're parsing a term it shouldn't cause trouble. Is this an expected error and we must be careful with declaring global syntax (so should probably always make syntax scoped), or is this a bug?

[Gabriel Ebner]

Keywords are currently global, so yes, be careful when using them in other syntax categories!

declare_syntax_cat unused
syntax "ohNo" : unused
#check ohNo -- error: expected term

[James Gallicchio]

are there plans down the road to change that? this behavior seems surprising to me

[Mac Malone]

@James Gallicchio yes, @Sebastian Ullrich has mentioned that category-local keywords is a goal. When that will happen, though, who knows.