Ending a command

Stream: lean4

[Mac]

Is there a correct way to end a command? My use case is following:

namespace Internal
scoped macro "foo" : command => `(#print "foo")
end Internal

section
open Internal -- error: unknown namespace 'foo'
foo
end

section
open Internal
section end
foo -- works
end

Since foo is not a keyword until the scoped macro is opened into the current namespace, I need a way to tell the command to end so that I can use foo immediately afterwards. Using section end as a separator works, but is rather esoteric and ugly. Is there a better way?

[Leonardo de Moura]

@Mac I have a fix for this. We can use the colGt helper parser when defining the open command. We used the same trick in some of the tactic parsers.

[Leonardo de Moura]

@Mac Pushed a fix. Both

open Internal
foo

and

open Internal in
foo

work now.

[Mac]

Cool! Thanks!