[wp] Always display script name

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)) ;

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

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