From d8db59aa027b24930f3ad264b09f6adb362321f1 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 3 May 2021 13:38:27 +0200
Subject: [PATCH] [wp] Feedback on saved status for script file
---
src/plugins/wp/GuiGoal.ml | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index 77dbf180519..6fb5dd22d7e 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -548,7 +548,11 @@ class pane (gprovers : GuiConfig.provers) =
text#clear ;
let main = ProofEngine.main proof in
if ProofSession.exists main then begin
- text#printf "%a@." ProofSession.pp_script_for main ;
+ 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 ;
--
GitLab