Commit 42bf61bd authored by MARCHE Claude's avatar MARCHE Claude
Browse files

fix issue #37

parent 2b407fe3
......@@ -354,7 +354,7 @@ let generate_auto_strategies config =
List.iter (fun s -> fprintf str_formatter "c %s 1 1000@\n" s) provers_level1;
let code = flush_str_formatter () in
let auto0 = {
strategy_name = "Auto level 0";
strategy_name = "Auto_level_0";
strategy_desc = "Automatic@ run@ of@ main@ provers";
strategy_shortcut = "0";
strategy_code = code }
......@@ -365,7 +365,7 @@ let generate_auto_strategies config =
List.iter (fun s -> fprintf str_formatter "c %s 10 4000@\n" s) provers_level1;
let code = flush_str_formatter () in
let auto1 = {
strategy_name = "Auto level 1";
strategy_name = "Auto_level_1";
strategy_desc = "Automatic@ run@ of@ main@ provers";
strategy_shortcut = "1";
strategy_code = code }
......@@ -392,7 +392,7 @@ let generate_auto_strategies config =
List.iter (fun s -> fprintf str_formatter "c %s 30 4000@\n" s) provers_level2;
let code = flush_str_formatter () in
let auto2 = {
strategy_name = "Auto level 2";
strategy_name = "Auto_level_2";
strategy_desc = "Automatic@ run@ of@ provers@ and@ most@ useful@ transformations";
strategy_shortcut = "2";
strategy_code = code }
......
......@@ -1773,8 +1773,8 @@ let add_submenu_strategy (shortcut,strategy) =
Opt.iter (fun (_,key,modi) -> i#add_accelerator ~group:tools_accel_group ~modi key)
(parse_shortcut_as_key shortcut);
let callback () =
Debug.dprintf debug "interp command '%s'@." shortcut;
interp shortcut
Debug.dprintf debug "interp command '%s'@." strategy;
interp strategy
in
connect_menu_item i ~callback
......@@ -1816,6 +1816,13 @@ let init_completion provers transformations strategies commands =
in
List.iter add_submenu_prover provers_sorted;
let all_strings =
List.fold_left (fun acc (shortcut,strategy) ->
Debug.dprintf debug "string for completion: '%s' '%s'@." shortcut strategy;
if shortcut = "" then strategy :: acc else shortcut :: strategy :: acc)
[] strategies
in
List.iter add_completion_entry all_strings;
List.iter add_submenu_strategy strategies;
command_entry_completion#set_text_column completion_col;
......
......@@ -81,7 +81,7 @@ type controller =
controller_env: Env.env;
controller_provers:
(Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
controller_strategies : (string * string * Strategy.instruction array) Stdlib.Hstr.t;
controller_strategies : (string * string * string * Strategy.instruction array) Stdlib.Hstr.t;
controller_running_proof_attempts : unit Hpan.t;
}
......
......@@ -88,7 +88,7 @@ type controller = private
controller_config : Whyconf.config;
controller_env : Env.env;
controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
controller_strategies : (string * string * Strategy.instruction array) Stdlib.Hstr.t;
controller_strategies : (string * string * string * Strategy.instruction array) Stdlib.Hstr.t;
controller_running_proof_attempts : unit Hpan.t;
}
......
......@@ -1149,7 +1149,7 @@ end
let d = get_server_data () in
let unproven_goals = unproven_goals_below_id d.cont (any_from_node_ID nid) in
try
let (n,_,st) = Hstr.find d.cont.controller_strategies s in
let (n,_,_,st) = Hstr.find d.cont.controller_strategies s in
Debug.dprintf debug_strat "[strategy_exec] running strategy '%s'@." n;
let callback sts =
Debug.dprintf debug_strat "[strategy_exec] strategy status: %a@." print_strategy_status sts
......
......@@ -148,15 +148,15 @@ let load_strategies cont =
let code = Strategy_parser.parse env config code in
let shortcut = st.Whyconf.strategy_shortcut in
Debug.dprintf debug "[session server info] Strategy '%s' loaded.@." name;
Stdlib.Hstr.add cont.Controller_itp.controller_strategies shortcut
(name, st.Whyconf.strategy_desc, code)
Stdlib.Hstr.add cont.Controller_itp.controller_strategies name
(name, shortcut, st.Whyconf.strategy_desc, code)
with Strategy_parser.SyntaxError msg ->
Format.eprintf "Fatal: loading strategy '%s' failed: %s@." name msg;
exit 1)
strategies
let list_strategies cont =
Stdlib.Hstr.fold (fun s (a,_,_) acc -> (s,a)::acc) cont.Controller_itp.controller_strategies []
Stdlib.Hstr.fold (fun _ (name,short,_,_) acc -> (short,name)::acc) cont.Controller_itp.controller_strategies []
let symbol_name s =
......
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