diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml index f4ddd156c273631c73bb02b8cd47e8c5bce39ea7..6fb5dd22d7e1c924a220c2556714929b4de685e4 100644 --- a/src/plugins/wp/GuiGoal.ml +++ b/src/plugins/wp/GuiGoal.ml @@ -546,6 +546,15 @@ class pane (gprovers : GuiConfig.provers) = on_proof_context proof begin fun () -> text#clear ; + let main = ProofEngine.main proof in + if ProofSession.exists main then begin + text#printf + (if ProofEngine.saved proof + then "%a (@{<green>saved@})@." + else "%a (@{<orange>modified@})@.") + ProofSession.pp_script_for main ; + text#hrule ; + end ; scripter#tree proof ; text#hrule ; text#printf "%t@." (printer#goal (ProofEngine.head proof)) ;