From c7a1d46b8e37a57f7ff04bcd517cafeea97c2778 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 3 May 2021 08:57:32 +0200
Subject: [PATCH] [wp] Print script name in TIP
---
src/plugins/wp/GuiGoal.ml | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index f4ddd156c27..77dbf180519 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -546,6 +546,11 @@ 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 "%a@." ProofSession.pp_script_for main ;
+ text#hrule ;
+ end ;
scripter#tree proof ;
text#hrule ;
text#printf "%t@." (printer#goal (ProofEngine.head proof)) ;
--
GitLab