[wp/gui] use prover selection to run command

src/plugins/wp/GuiConfig.mli

@@ -33,12 +33,4 @@ class dp_chooser :
     method run : unit -> unit (** Edit enabled provers *)
   end
 
-(*
-class dp_button : unit ->
-  object
-    inherit Widget.widget
-    method update : unit -> unit
-  end
-*)
-
 (* ------------------------------------------------------------------------ *)

src/plugins/wp/GuiNavigator.ml

@@ -91,6 +91,7 @@ class behavior
     ~(clear : Widget.button)
     ~(card : card Widget.selector)
     ~(list : GuiList.pane)
+    ~(provers : GuiConfig.provers)
     ~(goal : GuiGoal.pane)
     ~(source : GuiSource.highlighter)
     ~(popup : GuiSource.popup)
@@ -380,7 +381,7 @@ class behavior
         card#connect (fun _ -> self#details) ;
         scope#connect self#set_scope ;
         popup#on_click self#set_selection ;
-        popup#on_prove (GuiPanel.run_and_prove main) ;
+        popup#on_prove (GuiPanel.run_and_prove main provers) ;
         clear#connect self#clear ;
       end
 
@@ -505,7 +506,7 @@ let make (main : main_window_extension_points) =
     let filter = (filter :> _ Widget.selector) in
     let behavior = new behavior ~main
       ~next ~prev ~index ~scope ~filter ~clear
-      ~list ~card ~goal ~source ~popup in
+      ~list ~provers ~card ~goal ~source ~popup in
     GuiPanel.on_reload behavior#reload ;
     GuiPanel.on_update behavior#update ;
 

src/plugins/wp/GuiPanel.ml

@@ -63,8 +63,14 @@ let wp_rte_generated s =
         not mem
       else false
 
+let spawn provers vcs =
+  if not (Bag.is_empty vcs) then
+    let provers = Why3.Whyconf.Sprover.elements provers#get in
+    VC.command ~provers ~tip:true vcs
+
 let run_and_prove
     (main:Design.main_window_extension_points)
+    (provers:GuiConfig.provers)
     (selection:GuiSource.selection)
   =
   begin
@@ -72,9 +78,9 @@ let run_and_prove
       begin
         match selection with
         | S_none -> raise Stop
-        | S_fun kf -> VC.(command (generate_kf kf))
-        | S_prop ip -> VC.(command (generate_ip ip))
-        | S_call s -> VC.(command (generate_call s.s_stmt))
+        | S_fun kf -> spawn provers (VC.generate_kf kf)
+        | S_prop ip -> spawn provers (VC.generate_ip ip)
+        | S_call s -> spawn provers (VC.generate_call s.s_stmt)
       end ;
       if wp_rte_generated selection then
         main#redisplay ()

src/plugins/wp/GuiPanel.mli

@@ -27,7 +27,8 @@ val reload : unit -> unit
 val on_reload : (unit -> unit) -> unit
 
 val run_and_prove :
-  Design.main_window_extension_points -> GuiSource.selection -> unit
+  Design.main_window_extension_points ->
+  GuiConfig.provers -> GuiSource.selection -> unit
 
 val register :
   main:Design.main_window_extension_points ->

src/plugins/wp/VC.ml

@@ -96,6 +96,7 @@ let prove = Prover.prove
 let spawn = Prover.spawn ~delayed:true
 
 let server = ProverTask.server
-let command vcs = Register.do_wp_proofs_iter (fun f -> Bag.iter f vcs)
+let command ?provers ?tip vcs =
+  Register.do_wp_proofs_iter ?provers ?tip (fun f -> Bag.iter f vcs)
 
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/VC.mli

@@ -98,7 +98,9 @@ val server : ?procs:int -> unit -> Task.server
     The returned server is global to Frama-C, but the number of parallel task
     allowed will be updated to fit the [~procs] or command-line options. *)
 
-val command : t Bag.t -> unit
-(** Run the provers with the command-line interface *)
+val command : ?provers:Why3.Whyconf.prover list -> ?tip:bool -> t Bag.t -> unit
+(** Run the provers with the command-line interface.
+    If [~provers] is set, it is used for computing the list of provers to spawn.
+    If [~tip] is set, it is used to compute the script execution mode. *)
 
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/register.ml

@@ -511,7 +511,6 @@ let do_list_scheduled_result () =
 (* ------------------------------------------------------------------------ *)
 
 type mode = {
-  mutable why3ide : bool ;
   mutable tactical : bool ;
   mutable update : bool ;
   mutable depth : int ;
@@ -585,7 +584,7 @@ let dump_strategies =
                )))
 
 let default_mode () = {
-  why3ide = false ; tactical = false ; update=false ; provers = [] ;
+  tactical = false ; update=false ; provers = [] ;
   depth=0 ; width = 0 ; auto=[] ; backtrack = 0 ;
 }
 
@@ -668,11 +667,18 @@ let do_update_session mode iter =
           Wp_parameters.result "Updated session with %d new script%s to complete." f s );
     end
 
-let do_wp_proofs_iter iter =
+let do_wp_proofs_iter ?provers ?tip iter =
   let mode = default_mode () in
   compute_provers ~mode ;
   compute_auto ~mode ;
-  let spawned = mode.why3ide || mode.tactical || mode.provers <> [] in
+  begin match provers with None -> () | Some prvs ->
+    mode.provers <- List.map (fun dp -> VCS.BatchMode , VCS.Why3 dp) prvs
+  end ;
+  begin match tip with None -> () | Some tip ->
+    mode.tactical <- tip ;
+    mode.update <- tip ;
+  end ;
+  let spawned = mode.tactical || mode.provers <> [] in
   begin
     if spawned then do_list_scheduled iter ;
     spawn_wp_proofs_iter ~mode iter ;