Commit a93bf9ba authored by MARCHE Claude's avatar MARCHE Claude
Browse files

preference dialog allows to select which prover button to show

parent f2a8e7f1
...@@ -94,7 +94,7 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990 ...@@ -94,7 +94,7 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* tool why3doc * tool why3doc
* Support for several versions of the same prover * Support for several versions of the same prover
* Improved IDE: * Improved IDE:
- left scrollbar - left scrollbar + selection of shown or hidden provers
- font enlargement - font enlargement
- what else ? - what else ?
* what else ? * what else ?
......
...@@ -58,6 +58,8 @@ type t = ...@@ -58,6 +58,8 @@ type t =
original_config : Whyconf.config; original_config : Whyconf.config;
mutable altern_provers : altern_provers; mutable altern_provers : altern_provers;
mutable replace_prover : conf_replace_prover; mutable replace_prover : conf_replace_prover;
(* hidden prover buttons *)
mutable hidden_provers : string list;
} }
...@@ -77,6 +79,7 @@ type ide = { ...@@ -77,6 +79,7 @@ type ide = {
ide_error_color : string; ide_error_color : string;
ide_default_editor : string; ide_default_editor : string;
ide_replace_prover : conf_replace_prover; ide_replace_prover : conf_replace_prover;
ide_hidden_provers : string list;
} }
let default_ide = let default_ide =
...@@ -95,8 +98,9 @@ let default_ide = ...@@ -95,8 +98,9 @@ let default_ide =
ide_error_color = "orange"; ide_error_color = "orange";
ide_replace_prover = CRP_Ask; ide_replace_prover = CRP_Ask;
ide_default_editor = ide_default_editor =
try Sys.getenv "EDITOR" ^ " %f" (try Sys.getenv "EDITOR" ^ " %f"
with Not_found -> "editor %f" with Not_found -> "editor %f");
ide_hidden_provers = [];
} }
let load_ide section = let load_ide section =
...@@ -135,11 +139,13 @@ let load_ide section = ...@@ -135,11 +139,13 @@ let load_ide section =
get_string section ~default:default_ide.ide_default_editor get_string section ~default:default_ide.ide_default_editor
"default_editor"; "default_editor";
ide_replace_prover = ide_replace_prover =
match get_stringo section "replace_prover" with begin
match get_stringo section "replace_prover" with
| None -> default_ide.ide_replace_prover | None -> default_ide.ide_replace_prover
| Some "never not obsolete" -> CRP_Not_Obsolete | Some "never not obsolete" -> CRP_Not_Obsolete
| Some "ask" | Some _ -> CRP_Ask | Some "ask" | Some _ -> CRP_Ask
end;
ide_hidden_provers = get_stringl ~default:default_ide.ide_hidden_provers section "hidden_prover";
} }
...@@ -174,7 +180,11 @@ let load_config config original_config = ...@@ -174,7 +180,11 @@ let load_config config original_config =
let main = get_main config in let main = get_main config in
let ide = match get_section config "ide" with let ide = match get_section config "ide" with
| None -> default_ide | None -> default_ide
| Some s -> load_ide s in | Some s -> load_ide s
in
Format.eprintf "hidden provers : ";
List.iter (fun p -> Format.eprintf "%s" p) ide.ide_hidden_provers;
Format.eprintf "@.";
let alterns = let alterns =
List.fold_left load_altern List.fold_left load_altern
Mprover.empty (get_family config "alternative_prover") in Mprover.empty (get_family config "alternative_prover") in
...@@ -204,8 +214,10 @@ let load_config config original_config = ...@@ -204,8 +214,10 @@ let load_config config original_config =
env = env; env = env;
altern_provers = alterns; altern_provers = alterns;
replace_prover = ide.ide_replace_prover; replace_prover = ide.ide_replace_prover;
hidden_provers = ide.ide_hidden_provers;
} }
let save_altern unknown known (id,family) = let save_altern unknown known (id,family) =
let alt = empty_section in let alt = empty_section in
let alt = set_string alt "unknown_name" unknown.prover_name in let alt = set_string alt "unknown_name" unknown.prover_name in
...@@ -247,6 +259,7 @@ let save_config t = ...@@ -247,6 +259,7 @@ let save_config t =
(match t.replace_prover with (match t.replace_prover with
| CRP_Ask -> "ask" | CRP_Ask -> "ask"
| CRP_Not_Obsolete -> "never not obsolete") in | CRP_Not_Obsolete -> "never not obsolete") in
let ide = set_stringl ide "hidden_prover" t.hidden_provers in
let config = set_section config "ide" ide in let config = set_section config "ide" ide in
(* TODO: store newly detected provers ! (* TODO: store newly detected provers !
let config = set_provers config let config = set_provers config
...@@ -493,7 +506,7 @@ let alternatives_frame c (notebook:GPack.notebook) = ...@@ -493,7 +506,7 @@ let alternatives_frame c (notebook:GPack.notebook) =
in () in in () in
Mprover.iter iter c.altern_provers Mprover.iter iter c.altern_provers
let preferences c = let preferences (c : t) =
let dialog = GWindow.dialog ~title:"Why3: preferences" () in let dialog = GWindow.dialog ~title:"Why3: preferences" () in
let vbox = dialog#vbox in let vbox = dialog#vbox in
let notebook = GPack.notebook ~packing:vbox#add () in let notebook = GPack.notebook ~packing:vbox#add () in
...@@ -573,10 +586,34 @@ let preferences c = ...@@ -573,10 +586,34 @@ let preferences c =
*) *)
(** page 3 **) (** page 3 **)
let label3 = GMisc.label ~text:"Provers" () in let label3 = GMisc.label ~text:"Provers" () in
let _page3 = GMisc.label ~text:"This page should display detected provers" let page3 =
~packing:(fun w -> ignore(notebook#append_page GPack.vbox ~homogeneous:false ~packing:
~tab_label:label3#coerce w)) () (fun w -> ignore(notebook#append_page ~tab_label:label3#coerce w)) ()
in in
let provers_box =
GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
~packing:page3#add ()
in
let hidden_provers = Hashtbl.create 7 in
Mprover.iter
(fun _ p ->
let p = p.prover in
let label = p.prover_name ^ " " ^ p.prover_version in
let hidden = ref (List.mem label c.hidden_provers) in
Hashtbl.add hidden_provers label hidden;
let b =
GButton.check_button ~label ~packing:provers_box#add ()
~active:(not !hidden)
in
let (_ : GtkSignal.id) =
b#connect#toggled ~callback:
(fun () -> hidden := not !hidden;
c.hidden_provers <-
Hashtbl.fold
(fun l h acc -> if !h then l::acc else acc) hidden_provers [])
in ())
(Whyconf.get_provers c.config);
(** page 1 **) (** page 1 **)
let display_options_frame = let display_options_frame =
GBin.frame ~label:"Display options" GBin.frame ~label:"Display options"
......
...@@ -48,6 +48,7 @@ type t = ...@@ -48,6 +48,7 @@ type t =
original_config : Whyconf.config; original_config : Whyconf.config;
mutable altern_provers : prover option Mprover.t; mutable altern_provers : prover option Mprover.t;
mutable replace_prover : conf_replace_prover; mutable replace_prover : conf_replace_prover;
mutable hidden_provers : string list;
} }
val read_config : string option -> string list -> unit val read_config : string option -> string list -> unit
......
...@@ -921,15 +921,16 @@ let (_ : GMenu.image_menu_item) = ...@@ -921,15 +921,16 @@ let (_ : GMenu.image_menu_item) =
~label:"_Add file" ~callback:select_file ~label:"_Add file" ~callback:select_file
() ()
let refresh_provers = ref (fun () -> ())
let (_ : GMenu.image_menu_item) = let (_ : GMenu.image_menu_item) =
file_factory#add_image_item ~label:"_Preferences" ~callback: file_factory#add_image_item ~label:"_Preferences" ~callback:
(fun () -> (fun () ->
Gconfig.preferences gconfig; Gconfig.preferences gconfig;
M.set_maximum_running_proofs gconfig.max_running_processes sched) !refresh_provers ();
M.set_maximum_running_proofs gconfig.max_running_processes sched)
() ()
let refresh_provers = ref (fun () -> ())
let add_refresh_provers f _msg = let add_refresh_provers f _msg =
(* (*
eprintf "[Info] recording '%s' for refresh provers@." msg; eprintf "[Info] recording '%s' for refresh provers@." msg;
...@@ -1170,6 +1171,17 @@ let () = add_refresh_provers (fun () -> ...@@ -1170,6 +1171,17 @@ let () = add_refresh_provers (fun () ->
let () = let () =
let add_item_provers () = let add_item_provers () =
let provers = C.get_provers gconfig.Gconfig.config in
let provers =
C.Mprover.fold
(fun k p acc ->
let pr = p.prover in
if List.mem (pr.prover_name ^ " " ^ pr.prover_version)
gconfig.hidden_provers
then acc
else C.Mprover.add k p acc)
provers C.Mprover.empty
in
C.Mprover.iter C.Mprover.iter
(fun p _ -> (fun p _ ->
let n = Pp.string_of_wnl C.print_prover p in let n = Pp.string_of_wnl C.print_prover p in
...@@ -1191,7 +1203,7 @@ let () = ...@@ -1191,7 +1203,7 @@ let () =
b#connect#pressed b#connect#pressed
~callback:(fun () -> prover_on_selected_goals p) ~callback:(fun () -> prover_on_selected_goals p)
in ()) in ())
(C.get_provers gconfig.Gconfig.config) provers
in in
add_refresh_provers add_item_provers "Add in tools menu and provers box"; add_refresh_provers add_item_provers "Add in tools menu and provers box";
add_item_provers () add_item_provers ()
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment