diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml index 5e7988978a2a4bd7ef7e975dcd002bf1ba3522ee..13abb8a0a551734fcc8d462a6881bedbc44d8284 100644 --- a/src/plugins/wp/Cache.ml +++ b/src/plugins/wp/Cache.ml @@ -37,7 +37,8 @@ let get_miss () = !miss let get_removed () = !removed let mark_cache ~mode hash = - if mode = Cleanup || Fc_config.is_gui then Hashtbl.replace cleanup hash () + if mode = Cleanup || Wp_parameters.is_interactive () then + Hashtbl.replace cleanup hash () module CACHEDIR = WpContext.StaticGenerator(Datatype.Unit) (struct diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml index f34d944f7d82ce2e7f30ccbb6898972e06390f43..da4a68995e9c678b563ec33f60aa1a4405d57529 100644 --- a/src/plugins/wp/register.ml +++ b/src/plugins/wp/register.ml @@ -389,7 +389,7 @@ let do_wpo_success ~shell ~cache goal success = Wp_parameters.feedback ~ontty:`Silent "[Generated] Goal %s (%a)" (Wpo.get_gid goal) VCS.pp_prover prover else - let gui = Frama_c_very_first.Gui_init.is_gui in + let gui = Wp_parameters.is_interactive () in let smoke = Wpo.is_smoke_test goal in let cstats = ProofEngine.consolidated ~computing:false goal in let success = Wpo.is_passed goal in @@ -874,7 +874,7 @@ let () = Cmdline.run_after_setting_files let () = Cmdline.run_after_configuring_stage Why3Provers.configure let do_prover_detect () = - if not Fc_config.is_gui && Wp_parameters.Detect.get () then + if Wp_parameters.Detect.get () && not @@ Wp_parameters.is_interactive () then let provers = Why3Provers.provers () in if provers = [] then Wp_parameters.result "No Why3 provers detected." diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml index fa160ed4b0afc590811632467727bed6a8503a56..4ee4f2b30c91469c2294c117ae99e9a1e14c356b 100644 --- a/src/plugins/wp/wp_parameters.ml +++ b/src/plugins/wp/wp_parameters.ml @@ -45,6 +45,10 @@ let on_reset f = resetdemon := f :: !resetdemon let reset () = List.iter (fun f -> f ()) !resetdemon let has_dkey (k:category) = is_debug_key_enabled k +let server = ref false +let () = Server.Main.once (fun () -> server := true) +let is_interactive () = Fc_config.is_gui || !server + (* ------------------------------------------------------------------------ *) (* --- WP Generation --- *) (* ------------------------------------------------------------------------ *) @@ -1206,17 +1210,13 @@ let base_output () = let output = let dir = OutputDir.get () in if Fc_Filepath.Normalized.is_empty dir then - if Fc_config.is_gui + if is_interactive () then make_gui_dir () else make_tmp_dir () - else begin - make_output_dir dir ; - dir - end - in + else + ( make_output_dir dir ; dir ) in base_output := Some output; - Fc_Filepath.(add_symbolic_dir "WPOUT" output) ; - output + Fc_Filepath.add_symbolic_dir "WPOUT" output ; output | Some output -> output let get_output () = diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli index ee692cfe9f0d8bdc3b200d23a2c1261db960caca..d67f4b9cff3446b8d931300685f7679b316923e6 100644 --- a/src/plugins/wp/wp_parameters.mli +++ b/src/plugins/wp/wp_parameters.mli @@ -24,6 +24,7 @@ include Plugin.S val reset : unit -> unit val hypothesis : 'a Log.pretty_printer +val is_interactive : unit -> bool (** {2 Function Selection} *)