From 73a9e73952d249fa4aef3ab984a7fff30ee67be2 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 4 Jan 2022 16:25:29 +0100
Subject: [PATCH] [wp] Always display script name
---
src/plugins/wp/GuiGoal.ml | 8 +++++---
src/plugins/wp/ProofSession.ml | 9 ++++-----
src/plugins/wp/ProofSession.mli | 1 -
3 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index 5f3a55b090e..c1a83ee641d 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -547,14 +547,16 @@ class pane (gprovers : GuiConfig.provers) =
begin fun () ->
text#clear ;
let main = ProofEngine.main proof in
- if ProofSession.exists main then begin
+ if ProofSession.exists main then
text#printf
(if ProofEngine.saved proof
then "%a (@{<green>saved@})@."
else "%a (@{<orange>modified@})@.")
+ ProofSession.pp_script_for main
+ else
+ text#printf "%a (@{<blue>not created@})@."
ProofSession.pp_script_for main ;
- text#hrule ;
- end ;
+ text#hrule ;
scripter#tree proof ;
text#hrule ;
text#printf "%t@." (printer#goal (ProofEngine.head proof)) ;
diff --git a/src/plugins/wp/ProofSession.ml b/src/plugins/wp/ProofSession.ml
index 2839d1012fc..c1c8af78ef2 100644
--- a/src/plugins/wp/ProofSession.ml
+++ b/src/plugins/wp/ProofSession.ml
@@ -61,12 +61,11 @@ let get wpo =
let pp_file fmt s = Filepath.Normalized.(pretty fmt (of_string s))
-let pp_script fmt = function
- | NoScript -> Format.pp_print_string fmt "no script file"
+let pp_script_for fmt wpo =
+ match get wpo with
| Script f -> Format.fprintf fmt "script '%a'" pp_file f
- | Deprecated f -> Format.fprintf fmt "script '%a' (deprecated)" pp_file f
-
-let pp_script_for fmt wpo = pp_script fmt (get wpo)
+ | Deprecated f -> Format.fprintf fmt "(deprecated) script '%a'" pp_file f
+ | _ -> Format.fprintf fmt "script '%a'" pp_file @@ filename ~force:false wpo
let exists wpo =
match get wpo with NoScript -> false | Script _ | Deprecated _ -> true
diff --git a/src/plugins/wp/ProofSession.mli b/src/plugins/wp/ProofSession.mli
index 86372425758..58d2badb9a9 100644
--- a/src/plugins/wp/ProofSession.mli
+++ b/src/plugins/wp/ProofSession.mli
@@ -25,7 +25,6 @@ type script =
| Script of string
| Deprecated of string
-val pp_script : Format.formatter -> script -> unit
val pp_script_for : Format.formatter -> Wpo.t -> unit
val get : Wpo.t -> script
--
GitLab