parsing two (or more) commands

Stream: lean4

[Damiano Testa]

I would like to write a command that takes a sequence of commands and parses them all. However, I am failing. Below is an example of something that goes wrong -- I do not know if there are more issues, but this is certainly stumping me!

import Lean.Elab.Command

open Lean Elab Command in
elab "elab_two " cmd1:command cmd2:command : command => do
  elabCommand cmd1
  elabCommand cmd2

namespace Nat
scoped infixr:26 " plus " => Nat.add
end Nat

section
open Nat
#eval 2 plus 3  -- 5
end

elab_two
open Nat
--  it looks like the `open Nat` is not actually persisted open...
#eval 2 plus 3
/-
function expected at
  2
term has type
  ?m.2032
-/

[Sebastian Ullrich]

open Nat makes your parser visible, but the entire elab_two command has already been parsed - it's too late

[Damiano Testa]

Ah, at least now I understand the issue!

[Damiano Testa]

Is there a fix?

[Sebastian Ullrich]

Not really, at least in general. At some point, command elaborators may be allowed to do their own parsing, which would be useful for Verso as well.

[Damiano Testa]

Ok, I'll see what I can do, thanks!