Command elab starting a tactic proof

Stream: lean4

[Patrick Massot]

I have trouble writing a macro that prepend a tactic sequence with some tactic. The goal is to hide a call to docs#ProofWidgets.withPanelWidgets.

import ProofWidgets.Component.Panel.SelectionPanel

open ProofWidgets

-- The following example, copied from the ProofWidget demo folder, works
example (h : 2 + 2 = 5) : 2 + 2 = 4 := by
  with_panel_widgets [SelectionPanel]
  -- See a widget here :-)
  rfl

section
open Lean Meta Elab Command

open Lean.Parser.Term (bracketedBinder)

elab "exercise : " concl:term "Proof:" prf:tacticSeq : command => do
elabCommand (← `(command|example : $concl := by
      with_panel_widgets [SelectionPanel]
      $prf))
end


exercise : True
Proof:
  -- No widget here :-(
  trivial


exercise : True
Proof:
  with_panel_widgets [SelectionPanel]
  -- See a widget here
  trivial