Scope keywords within syntax definition

Stream: lean4

[Marx]

Hey guys,
I’m wondering if it’s possible to scope keywords within a syntax definition.
My goal is to nest one syntax category inside another, and have the parser only recognize the keywords or tokens from the inner syntax category when it's currently parsing the outer syntax category.
The reason for this is that I want to avoid having certain keywords from the inner syntax category be reserved globally.
Here is a mwe:

import Lean
open Lean Elab Parser

declare_syntax_cat outer_syntax
declare_syntax_cat inner_syntax

syntax "start_syntax" withPosition(semicolonOrLinebreak)
          inner_syntax*
          withPosition(semicolonOrLinebreak)
        "end_syntax": outer_syntax

syntax "ex" num &"x" : inner_syntax
syntax outer_syntax : term

#check  start_syntax
          ex 1 x
        end_syntax

def ex := 1 -- unexpected token 'ex'; expected identifier

[Jannis Limperg]

This is currently not supported; keywords are always global. However, you can configure your inner syntax category to accept &"ex" as a 'keyword' (changes marked with !!):

import Lean
open Lean Elab Parser

declare_syntax_cat outer_syntax
declare_syntax_cat inner_syntax (behavior := both) -- !!

syntax "start_syntax" withPosition(semicolonOrLinebreak)
          inner_syntax*
          withPosition(semicolonOrLinebreak)
        "end_syntax": outer_syntax

syntax &"ex" num &"x" : inner_syntax -- !!
syntax outer_syntax : term

#check  start_syntax
          ex 1 x
        end_syntax

def ex := 1 -- unexpected token 'ex'; expected identifier

[Marx]

Oh that's great, thank you very much!