diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml index 5f3a55b090e876ed2c3454b29e6fdce536e4ce80..c1a83ee641dcd71777e066c6881750463dc89171 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 2839d1012fc2a4bf2ad2f8e4ed61f7aacb63f572..c1c8af78ef229da15cb6dc6b87d70545410cfc0c 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 86372425758114ec4fbe5d1c68a7d2f44162418c..58d2badb9a9b1f0dffff75431815077363d5cd21 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