Commit e8e631c9 authored by MARCHE Claude's avatar MARCHE Claude

strategies: key shortcuts

parent ebd28e68
......@@ -134,24 +134,26 @@ type config_strategy = {
strategy_name : string;
strategy_desc : Pp.formatted;
strategy_code : string array;
strategy_shortcut : string;
}
(* a default set of strategies *)
let default_strategies =
List.map
(fun (name,desc,instrs) ->
(fun (name,desc,shortcut,instrs) ->
let s = ref Rc.empty_section in
s := Rc.set_string !s "name" name;
s := Rc.set_string !s "desc" desc;
s := Rc.set_string !s "shortcut" shortcut;
for i = 0 to Array.length instrs - 1 do
s := Rc.set_string !s ("l" ^ (string_of_int i)) instrs.(i);
done;
!s)
[ "Split", "Split@ conjunctions@ in@ goal",
[ "Split", "Split@ conjunctions@ in@ goal", "s",
[|"t split_goal_wp 1"|];
"Inline", "Inline@ function@ symbols@ once",
"Inline", "Inline@ function@ symbols@ once", "i",
[|"t inline_goal 1"|];
"Blaster", "The@ blaster",
"My mini-blaster", "A@ simple@ blaster", "b",
[|"c Alt-Ergo,0.95.2 1 1000";
"c CVC4,1.4 1 1000";
"t split_goal_wp 0";
......@@ -470,6 +472,7 @@ let load_strategy strategies section =
try
let name = get_string section "name" in
let desc = get_string section "desc" in
let shortcut = get_string ~default:"" section "shortcut" in
let desc = Scanf.format_from_string desc "" in
let code = ref [] and i = ref 0 in
try
......@@ -485,6 +488,7 @@ let load_strategy strategies section =
{ strategy_name = name;
strategy_desc = desc;
strategy_code = Array.of_list (List.rev !code);
strategy_shortcut = shortcut;
}
strategies
with
......
......@@ -183,6 +183,7 @@ type config_strategy = {
strategy_name : string;
strategy_desc : Pp.formatted;
strategy_code : string array;
strategy_shortcut : string;
}
val get_strategies : config -> config_strategy Mstr.t
......
......@@ -1459,6 +1459,40 @@ let strategies () :
let loaded_strategies = ref []
let load_shortcut s =
if String.length s <> 1 then None else
try
let key = match String.get s 0 with
| 'a' -> GdkKeysyms._a
| 'b' -> GdkKeysyms._b
| 'c' -> GdkKeysyms._c
| 'd' -> GdkKeysyms._d
| 'e' -> GdkKeysyms._e
| 'f' -> GdkKeysyms._f
| 'g' -> GdkKeysyms._g
| 'h' -> GdkKeysyms._h
| 'i' -> GdkKeysyms._i
| 'j' -> GdkKeysyms._j
| 'k' -> GdkKeysyms._k
| 'l' -> GdkKeysyms._l
| 'm' -> GdkKeysyms._m
| 'n' -> GdkKeysyms._n
| 'o' -> GdkKeysyms._o
| 'p' -> GdkKeysyms._p
| 'q' -> GdkKeysyms._q
| 'r' -> GdkKeysyms._r
| 's' -> GdkKeysyms._s
| 't' -> GdkKeysyms._t
| 'u' -> GdkKeysyms._u
| 'v' -> GdkKeysyms._v
| 'w' -> GdkKeysyms._w
| 'x' -> GdkKeysyms._x
| 'y' -> GdkKeysyms._y
| 'z' -> GdkKeysyms._z
| _ -> raise Not_found
in Some(s,key)
with Not_found -> None
let strategies () =
match !loaded_strategies with
| [] ->
......@@ -1471,15 +1505,17 @@ let strategies () =
try
let code = st.Whyconf.strategy_code in
let len = Array.length code in
let shortcut = load_shortcut st.Whyconf.strategy_shortcut in
let code = Array.map (M.parse_instr (env_session()) len) code in
Format.eprintf "Strategy '%s' loaded.@." name;
(name, st.Whyconf.strategy_desc,code, None) :: acc
(name, st.Whyconf.strategy_desc,code, shortcut) :: acc
with M.SyntaxError msg ->
Format.eprintf "Loading strategy '%s' failed: %s@." name msg;
acc)
[]
strategies
in
let strategies = List.rev strategies in
loaded_strategies := strategies;
strategies
| l -> l
......
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