diff --git a/src/plugins/wp/GuiConfig.ml b/src/plugins/wp/GuiConfig.ml
index 10dc553e75ed7d6a07c7fe478470f40afad26658..4e28f2e8957422a891e016663e4e583ec0d5c2fb 100644
--- a/src/plugins/wp/GuiConfig.ml
+++ b/src/plugins/wp/GuiConfig.ml
@@ -24,51 +24,29 @@
(* --- Prover List in Configuration --- *)
(* ------------------------------------------------------------------------ *)
-class provers key =
+module S = Why3.Whyconf.Sprover
+module M = Why3.Whyconf.Mprover
+
+class provers =
object(self)
- inherit [Why3.Whyconf.Sprover.t] Wutil.selector Why3.Whyconf.Sprover.empty
-
- method private load () =
- let open Gtk_helper.Configuration in
- let prover_of_conf acc = function
- | ConfList [ConfString prover_name;
- ConfString prover_version;
- ConfString prover_altern] ->
- Why3.Whyconf.Sprover.add
- Why3.Whyconf.{ prover_name; prover_version; prover_altern }
- acc
- | _ -> acc in
- try
- let data = Gtk_helper.Configuration.find key in
- match data with
- | ConfList data ->
- (List.fold_left prover_of_conf Why3.Whyconf.Sprover.empty data)
- | _ -> Why3.Whyconf.Sprover.empty
- with Not_found -> Why3.Whyconf.Sprover.empty
-
- method private save () =
- let open Gtk_helper.Configuration in
- let conf_of_prover dp = ConfList Why3.Whyconf.[ConfString dp.prover_name;
- ConfString dp.prover_version;
- ConfString dp.prover_altern] in
- Gtk_helper.Configuration.set key
- (ConfList (List.map conf_of_prover
- (Why3.Whyconf.Sprover.elements self#get)))
+ inherit [S.t] Wutil.selector S.empty
initializer
begin
- let settings = self#load () in
(** select automatically the provers set on the command line *)
- let cmdline = Wp_parameters.Provers.get () in
+ let cmdline =
+ match Wp_parameters.Provers.get () with
+ | [] -> [ "alt-ergo" ]
+ | prvs -> prvs
+ in
let selection = List.fold_left
(fun acc e ->
match Why3Provers.find_opt e with
| None -> acc
- | Some p -> Why3.Whyconf.Sprover.add p acc)
- settings cmdline
+ | Some p -> S.add p acc)
+ S.empty cmdline
in
self#set selection ;
- self#on_event self#save ;
end
end
@@ -88,13 +66,14 @@ class dp_chooser
let array = new Wpane.warray () in
object(self)
- val mutable selected = Why3.Whyconf.Mprover.empty
+ val mutable mainstream = true
+ val mutable selected = M.empty
method private enable dp e =
- selected <- Why3.Whyconf.Mprover.add dp e selected
+ selected <- M.add dp e selected
method private lookup dp =
- Why3.Whyconf.Mprover.find dp selected
+ try M.find dp selected with Not_found -> false
method private entry dp =
let text = Why3Provers.title dp in
@@ -117,23 +96,30 @@ class dp_chooser
array#update () ;
end
- method private detect () =
+ method private provers =
+ let filter p =
+ self#lookup p || not mainstream || Why3Provers.is_mainstream p
+ in S.filter filter (Why3Provers.provers_set ())
+
+ method private filter () =
begin
- self#configure (Why3Provers.provers_set ());
+ mainstream <- not mainstream ;
+ self#configure self#provers ;
end
method private apply () =
provers#set
- (Why3.Whyconf.Mprover.map_filter
+ (M.map_filter
(function
| true -> Some ()
| false -> None)
selected)
method run () =
- let dps = Why3Provers.provers_set () in
+ selected <- M.empty ;
+ let dps = self#provers in
let sel = provers#get in
- selected <- Why3.Whyconf.Mprover.merge
+ selected <- M.merge
(fun _ avail enab ->
match avail, enab with
| None, _ -> None
@@ -145,7 +131,8 @@ class dp_chooser
initializer
begin
- dialog#button ~action:(`ACTION self#detect) ~label:"Detect Provers" () ;
+ dialog#button ~action:(`ACTION self#filter) ~label:"Filter"
+ ~tooltip:"Switch to main stream / alternative solvers" () ;
dialog#button ~action:(`CANCEL) ~label:"Cancel" () ;
dialog#button ~action:(`APPLY) ~label:"Apply" () ;
array#set_entry self#entry ;
diff --git a/src/plugins/wp/GuiConfig.mli b/src/plugins/wp/GuiConfig.mli
index 8da20b6c04d036f1f4a20b67de0d800433b9c278..9d912d61ffe92012713f45d0e91441d23b6a5c29 100644
--- a/src/plugins/wp/GuiConfig.mli
+++ b/src/plugins/wp/GuiConfig.mli
@@ -24,7 +24,7 @@
(* --- WP Provers Configuration Panel --- *)
(* ------------------------------------------------------------------------ *)
-class provers : string -> [Why3.Whyconf.Sprover.t] Widget.selector
+class provers : [Why3.Whyconf.Sprover.t] Widget.selector
class dp_chooser :
main:Design.main_window_extension_points ->
diff --git a/src/plugins/wp/GuiNavigator.ml b/src/plugins/wp/GuiNavigator.ml
index 06cc23a28c451cb7ba48c8bc8d2c227e2762450b..5c04d8a2c0b6904ea815f6e2ebf5b983bdfca50f 100644
--- a/src/plugins/wp/GuiNavigator.ml
+++ b/src/plugins/wp/GuiNavigator.ml
@@ -441,8 +441,7 @@ let make (main : main_window_extension_points) =
(* --- Provers --- *)
(* -------------------------------------------------------------------------- *)
- let provers = new GuiConfig.provers "wp.provers" in
-
+ let provers = new GuiConfig.provers in
let dp_chooser = new GuiConfig.dp_chooser ~main ~provers in
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 46a1f714ab5902d7b9356ede7a3a0f879af75a54..215d8912e50e7b2cbb3160540329ddd5e50e6c63 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -94,6 +94,7 @@ let print_wp s =
let title p = Pretty_utils.sfprintf "%a" Why3.Whyconf.print_prover p
let name p = p.Why3.Whyconf.prover_name
let compare = Why3.Whyconf.Prover.compare
+let is_mainstream p = p.Why3.Whyconf.prover_altern = ""
let provers () =
Why3.Whyconf.Mprover.keys (Why3.Whyconf.get_provers (config ()))
diff --git a/src/plugins/wp/Why3Provers.mli b/src/plugins/wp/Why3Provers.mli
index 4875dbcc97b27d5081c3df090a693254ef0a5dc5..1098dc55906999c9c19cc85f11aaeb1fb02a297c 100644
--- a/src/plugins/wp/Why3Provers.mli
+++ b/src/plugins/wp/Why3Provers.mli
@@ -41,6 +41,7 @@ val compare : t -> t -> int
val provers : unit -> t list
val provers_set : unit -> Why3.Whyconf.Sprover.t
val is_available : t -> bool
+val is_mainstream : t -> bool
val has_shortcut : t -> string -> bool
(**************************************************************************)