Commit 08905714 authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'ide_pref_change' into 'master'

Ide pref change

Closes #418

See merge request !293
parents 8a9442c7 c4a22404
......@@ -79,6 +79,7 @@ IDE
* Read only file can now be displayed and removed by right clicking on their
tab titles
* Colors for error can now be edited in the why3.conf more precisely
* Most of the preferences can now be changed for the current session
Realizations
* added experimental realizations for new Set theories in both Isabelle and Coq
......
......@@ -503,7 +503,7 @@ let detect_exec env data exec_name =
interactive = (match data.kind with ITP -> true | ATP -> false);
extra_options = [];
extra_drivers = [];
added_at_startup = false;
detected_at_startup = false;
} in
(* if unknown, temporarily put the prover away *)
if not (good || old) then begin
......@@ -535,8 +535,13 @@ let detect_exec env data exec_name =
let detect_exec env data acc exec_name =
try
let prover_config = detect_exec env data exec_name in
known_version env exec_name;
add_prover_with_uniq_id prover_config acc
if Mprover.mem prover_config.prover acc then
(* Avoid adding manually added provers twice *)
acc
else begin
known_version env exec_name;
add_prover_with_uniq_id prover_config acc
end
with
| Skip -> acc
| Discard -> known_version env exec_name; acc
......@@ -630,8 +635,11 @@ let provers_from_detected_provers config =
(Some detected.version))
(get_detected_provers config);
let detected = run_auto_detection' env config in
let manually_added = get_provers config in
let detected =
Whyconf.Mprover.map (fun c -> { c with added_at_startup = true }) detected
Mprover.map (fun c -> if Mprover.mem c.prover manually_added
then c else
{ c with detected_at_startup = true }) detected
in
generate_builtin_config (env,detected) config
......
......@@ -138,7 +138,7 @@ type config_prover = {
interactive : bool;
extra_options : string list;
extra_drivers : string list;
added_at_startup : bool;
detected_at_startup : bool;
}
type config_editor = {
......@@ -477,7 +477,7 @@ let load_prover (provers,shortcuts) section =
interactive = get_bool ~default:false section "interactive";
extra_options = [];
extra_drivers = [];
added_at_startup = false;
detected_at_startup = false;
} provers in
let lshort = get_stringl section ~default:[] "shortcut" in
let shortcuts = add_prover_shortcuts shortcuts prover lshort in
......@@ -836,7 +836,7 @@ let set_main config main =
let set_provers config ?shortcuts provers =
let shortcuts = Opt.get_def config.prover_shortcuts shortcuts in
let rc_config =
let provers = Mprover.filter (fun _ c -> not c.added_at_startup) provers in
let provers = Mprover.filter (fun _ c -> not c.detected_at_startup) provers in
set_provers_shortcuts config.config shortcuts provers;
in
{config with
......
......@@ -132,7 +132,7 @@ type config_prover = {
interactive : bool; (* Interactive theorem prover *)
extra_options: string list;
extra_drivers: string list;
added_at_startup : bool; (* added at startup or present in the user configuration *)
detected_at_startup : bool; (* detected at startup *)
}
val get_complete_command : config_prover -> with_steps:bool -> string
......
......@@ -257,7 +257,7 @@ let load_config config original_config =
session_nb_processes = Whyconf.running_provers_max main;
}
let save_config t =
let get_config t =
Debug.dprintf debug "[config] saving IDE config file@.";
(* taking original config, without the extra_config *)
let config = t.original_config in
......@@ -275,6 +275,8 @@ let save_config t =
let config = set_provers config (get_provers t.config) in
(* copy also the possibly changed policies *)
let config = set_policies config (get_policies t.config) in
(* Set editors *)
let config = set_editors config (get_editors t.config) in
let ide = empty_section in
let ide = set_int ide "window_height" t.window_height in
let ide = set_int ide "window_width" t.window_width in
......@@ -303,8 +305,10 @@ let save_config t =
let ide = set_string ide "search_color" t.search_color in
let ide = set_string ide "iconset" t.iconset in
let ide = set_stringl ide "hidden_prover" t.hidden_provers in
let config = Whyconf.set_section config "ide" ide in
Whyconf.save_config config
Whyconf.set_section config "ide" ide
let save_config t =
Whyconf.save_config (get_config t)
let config,load_config =
let config = ref None in
......@@ -1275,8 +1279,10 @@ let preferences ~parent (c : t) =
c.config <- Whyconf.set_main c.config
(Whyconf.set_limits (Whyconf.get_main c.config)
c.session_time_limit c.session_mem_limit c.session_nb_processes);
save_config ()
| `CLOSE | `DELETE_EVENT -> ()
save_config ();
Itp_server.set_partial_config (get_config (config ()))
| `CLOSE | `DELETE_EVENT ->
Itp_server.set_partial_config (get_config (config ()))
end;
dialog#destroy ()
......
......@@ -1919,6 +1919,69 @@ object (self)
m
end
(*****************************************************************)
(* "Tools" submenus for strategies, provers, and transformations *)
(*****************************************************************)
let string_of_desc desc =
let print_trans_desc fmt (x,r) =
fprintf fmt "@[<hov 2>%s@\n%a@]" x Pp.formatted r
in Glib.Markup.escape_text (Pp.string_of print_trans_desc desc)
let parse_shortcut_as_key s =
let (key,modi) as r = GtkData.AccelGroup.parse s in
begin if key = 0 then
Debug.dprintf debug "Shortcut '%s' cannot be parsed as a key@." s
else
let name = GtkData.AccelGroup.name ~key ~modi in
Debug.dprintf debug "Shortcut '%s' parsed as key '%s'@." s name
end;
r
let add_submenu_strategy (str_fac: menu_factory) (con_fac: menu_factory) (shortcut,strategy) =
let callback () =
Debug.dprintf debug "interp command '%s'@." strategy;
interp strategy
in
let name = String.map (function '_' -> ' ' | c -> c) strategy in
let tooltip = "run strategy " ^ strategy ^ " on selected goal" in
let accel_path = "<Why3-Main>/Tools/Strategies/" ^ name in
let (key, modi) = parse_shortcut_as_key shortcut in
let (_ : GMenu.menu_item) = str_fac#add_item name
~use_mnemonic:false ~accel_path ~key ~modi ~tooltip ~callback in
let (_ : GMenu.menu_item) = con_fac#add_item name
~use_mnemonic:false ~accel_path ~add_accel:false ~tooltip ~callback in
()
let hide_context_provers, add_submenu_prover =
(* Set of context provers menu items *)
let context_provers = Hstr.create 16 in
(* After preferences for hidden provers are set, actualize provers allowed in
the context_factory *)
let hide_context_provers () =
Hstr.iter (fun k i ->
if List.mem k gconfig.hidden_provers then
i#misc#hide ()
else
i#misc#show ()) context_provers in
let add_submenu_prover (pro_fac: menu_factory) (con_fac: menu_factory)
(shortcut,prover_name,prover_parseable_name) =
let callback () =
Debug.dprintf debug "interp command '%s'@." prover_parseable_name;
interp prover_parseable_name
in
let tooltip = "run prover " ^ prover_name ^ " on selected goal" in
let accel_path = "<Why3-Main>/Tools/Provers/" ^ prover_name in
let (key,modi) = parse_shortcut_as_key shortcut in
let (_ : GMenu.menu_item) = pro_fac#add_item prover_name
~use_mnemonic:false ~accel_path ~key ~modi ~tooltip ~callback in
let (i : GMenu.menu_item) = con_fac#add_item prover_name
~use_mnemonic:false ~accel_path ~add_accel:false ~tooltip ~callback in
Hstr.add context_provers prover_parseable_name i;
if List.mem prover_parseable_name gconfig.hidden_provers then
i#misc#hide() in
hide_context_provers, add_submenu_prover
(*************)
(* Main menu *)
(*************)
......@@ -1945,6 +2008,8 @@ let (_: GMenu.menu_item) =
let (_: GMenu.menu_item) =
let callback () =
Gconfig.preferences ~parent:main_window gconfig;
(* hide/show provers in contextual menu *)
hide_context_provers ();
(* Source view tags *)
Opt.iter (fun (_, v) -> update_tags gconfig v) (find_current_file_view ());
(* Update message zone tags *)
......@@ -2260,55 +2325,6 @@ let (_ : GMenu.menu_item) =
"About"
~callback:(show_about_window ~parent:main_window)
(*****************************************************************)
(* "Tools" submenus for strategies, provers, and transformations *)
(*****************************************************************)
let string_of_desc desc =
let print_trans_desc fmt (x,r) =
fprintf fmt "@[<hov 2>%s@\n%a@]" x Pp.formatted r
in Glib.Markup.escape_text (Pp.string_of print_trans_desc desc)
let parse_shortcut_as_key s =
let (key,modi) as r = GtkData.AccelGroup.parse s in
begin if key = 0 then
Debug.dprintf debug "Shortcut '%s' cannot be parsed as a key@." s
else
let name = GtkData.AccelGroup.name ~key ~modi in
Debug.dprintf debug "Shortcut '%s' parsed as key '%s'@." s name
end;
r
let add_submenu_strategy (shortcut,strategy) =
let callback () =
Debug.dprintf debug "interp command '%s'@." strategy;
interp strategy
in
let name = String.map (function '_' -> ' ' | c -> c) strategy in
let tooltip = "run strategy " ^ strategy ^ " on selected goal" in
let accel_path = "<Why3-Main>/Tools/Strategies/" ^ name in
let (key, modi) = parse_shortcut_as_key shortcut in
let (_ : GMenu.menu_item) = strategies_factory#add_item name
~use_mnemonic:false ~accel_path ~key ~modi ~tooltip ~callback in
let (_ : GMenu.menu_item) = context_factory#add_item name
~use_mnemonic:false ~accel_path ~add_accel:false ~tooltip ~callback in
()
let add_submenu_prover (shortcut,prover_name,prover_parseable_name) =
let callback () =
Debug.dprintf debug "interp command '%s'@." prover_parseable_name;
interp prover_parseable_name
in
let tooltip = "run prover " ^ prover_name ^ " on selected goal" in
let accel_path = "<Why3-Main>/Tools/Provers/" ^ prover_name in
let (key,modi) = parse_shortcut_as_key shortcut in
let (_ : GMenu.menu_item) = provers_factory#add_item prover_name
~use_mnemonic:false ~accel_path ~key ~modi ~tooltip ~callback in
if not (List.mem prover_parseable_name gconfig.hidden_provers) then
let (_ : GMenu.menu_item) = context_factory#add_item prover_name
~use_mnemonic:false ~accel_path ~add_accel:false ~tooltip ~callback in
()
let init_completion provers transformations strategies commands =
(* add the names of all the the transformations *)
List.iter add_completion_entry transformations;
......@@ -2334,7 +2350,7 @@ let init_completion provers transformations strategies commands =
let menu_provers =
List.filter (fun (_, _, s) -> not (Strings.ends_with s "counterexamples"))
provers_sorted in
List.iter add_submenu_prover menu_provers;
List.iter (add_submenu_prover provers_factory context_factory) menu_provers;
context_factory#add_separator ();
let all_strings =
List.fold_left (fun acc (shortcut,strategy) ->
......@@ -2345,7 +2361,7 @@ let init_completion provers transformations strategies commands =
[] strategies
in
List.iter add_completion_entry all_strings;
List.iter add_submenu_strategy strategies;
List.iter (add_submenu_strategy strategies_factory context_factory) strategies;
command_entry_completion#set_text_column completion_col;
(* Adding a column which contains the description of the
......
......@@ -84,6 +84,12 @@ type controller =
controller_running_proof_attempts : unit Hpan.t;
}
let set_partial_config cont c =
let open Whyconf in
let config = set_editors cont.controller_config (get_editors c) in
let config = set_provers config (get_provers c) in
cont.controller_config <- config
let session_max_tasks = ref 1
let set_session_max_tasks n =
......
......@@ -195,6 +195,9 @@ val remove_subtree: notification:notifier -> removed:notifier ->
val get_undetached_children_no_pa: Session_itp.session -> any -> any list
val set_partial_config: controller -> Whyconf.config -> unit
(** edit a minimal part of the configuration that should be safe to edit during
execution of the server (provers config, editors) *)
(** {2 Scheduled jobs} *)
......
......@@ -16,7 +16,6 @@ open Controller_itp
open Server_utils
open Itp_communication
(**********************************)
(* list unproven goal and related *)
(**********************************)
......@@ -97,6 +96,28 @@ let print_ext_any task (lang:string) print_any =
| print_ext_any -> print_ext_any task print_any
| exception Not_found -> print_any
type server_data =
{ (* task_driver : Driver.driver; *)
cont : Controller_itp.controller;
send_source: bool;
(* If true the server is parametered to send source mlw files as
notifications *)
global_infos : Itp_communication.global_information;
}
let server_data = ref None
let get_server_data () =
match !server_data with
| None ->
Format.eprintf "get_server_data(): fatal error, server not yet initialized@.";
exit 1
| Some x -> x
let set_partial_config c =
let d = get_server_data () in
Controller_itp.set_partial_config d.cont c
module Make (S:Controller_itp.Scheduler) (Pr:Protocol) = struct
module C = Controller_itp.Make(S)
......@@ -360,24 +381,6 @@ let () =
*)
]
type server_data =
{ (* task_driver : Driver.driver; *)
cont : Controller_itp.controller;
send_source: bool;
(* If true the server is parametered to send source mlw files as
notifications *)
global_infos : Itp_communication.global_information;
}
let server_data = ref None
let get_server_data () =
match !server_data with
| None ->
Format.eprintf "get_server_data(): fatal error, server not yet initialized@.";
exit 1
| Some x -> x
(* fresh gives new fresh "names" for node_ID using a counter.
reset resets the counter so that we can regenerate node_IDs as if session
was fresh *)
......@@ -602,6 +605,7 @@ module P = struct
end
(*********************)
(* File input/output *)
(*********************)
......@@ -1349,7 +1353,6 @@ end
Debug.dprintf debug_strat "[strategy_exec] strategy '%s' not found@." s
(* ----------------- Clean session -------------------- *)
let clean nid =
let d = get_server_data () in
......
......@@ -29,6 +29,11 @@ end
*)
val add_registered_lang: string -> (Task.task -> any_pp Pp.pp -> any_pp Pp.pp) -> unit
(* Used to update the config after preferences are changed in the ide.
This is not usable by other IDEs (webide): in the long term a
request/notification could be added for this kind of interaction. *)
val set_partial_config: Whyconf.config -> unit
module Make (S:Controller_itp.Scheduler) (P:Protocol) : sig
(* This function is used to change the registered function for
......
......@@ -168,7 +168,7 @@ let main () =
let config =
if !autoprovers
then
let config = Whyconf.set_provers config Mprover.empty in
let config = Whyconf.set_provers config (Whyconf.get_provers config) in
let config = Whyconf.set_load_default_config !partial_config config in
let env = Autodetection.run_auto_detection config in
if !partial_config then
......
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