open_locale scoping

Stream: general

[Reid Barton]

If open_locale appears inside a section/namespace, are its effects scoped to that section/namespace?

[Floris van Doorn]

Yes, it has the same effect as writing

local notation ...
local attribute ...

in that spot

[Simon Hudon]

How did you manage that?

[Simon Hudon]

Oh, I see, nevermind :P

[Floris van Doorn]

for others wondering the same: it's calling emit_code_here to run exactly those commands.