Commit dd2cf206 authored by MARCHE Claude's avatar MARCHE Claude

more generic handling of command line

parent f3afc687
......@@ -157,9 +157,6 @@ val list_transforms_l : unit -> (string * Pp.formatted) list
val named : string -> 'a trans -> 'a trans
(** give transformation a name without registering *)
val apply_transform : string -> Env.env -> task -> task list
(** apply a registered 1-to-1 or a 1-to-n, directly *)
(** {2 Transformations with arguments}
These transformations take strings as arguments. For a more "typed" version,
......@@ -174,5 +171,18 @@ type trans_with_args_l = string list -> Env.env -> task tlist
val register_transform_with_args : desc:Pp.formatted -> string -> trans_with_args -> unit
val register_transform_with_args_l : desc:Pp.formatted -> string -> trans_with_args_l -> unit
(** {2 handling of all forms of transformations} *)
type gentrans =
| Trans_one of Task.task trans
| Trans_list of Task.task tlist
| Trans_with_args of trans_with_args
| Trans_with_args_l of trans_with_args_l
val lookup_trans : Env.env -> string -> gentrans
val apply_transform : string -> Env.env -> task -> task list
(** apply a registered 1-to-1 or a 1-to-n, directly.*)
val apply_transform_args : string -> Env.env -> string list -> task -> task list
(** apply a registered 1-to-1 or a 1-to-n or a trans with args, directly *)
......@@ -343,14 +343,14 @@ let callback_update_tree_transform ses row_reference = fun status ->
build_subtree_from_trans ses row_reference trans_id
| _ -> ()
let apply_transform ses =
let apply_transform ses t args =
match !current_selected_index with
| IproofNode id ->
let row_ref = Hpn.find pn_id_to_gtree id in (* TODO exception *)
let callback =
callback_update_tree_transform ses row_ref
in
C.schedule_transformation cont id "cut" ["0=0"] ~callback
C.schedule_transformation cont id t args ~callback
| _ -> printf "Error: Give the name of the transformation@."
......@@ -439,16 +439,22 @@ let test_schedule_proof_attempt ses =
let clear_command_entry () = command_entry#set_text ""
open Session_user_interface
let interp cmd =
match cmd with
match interp cont.controller_env cmd with
| Transform(s,_t,args) ->
clear_command_entry ();
apply_transform cont.controller_session s args
| Query s ->
message_zone#buffer#set_text s
| Other(s,_args) ->
match s with
| "s" -> clear_command_entry ();
run_strategy_on_task "1"
| "t" -> clear_command_entry ();
apply_transform cont.controller_session
| "c" -> clear_command_entry ();
test_schedule_proof_attempt cont.controller_session
| _ -> message_zone#buffer#set_text ("unknown command '"^cmd^"'")
| _ -> message_zone#buffer#set_text ("unknown command '"^s^"'")
let (_ : GtkSignal.id) =
command_entry#connect#activate
......
......@@ -84,3 +84,90 @@ let strategies env config =
loaded_strategies := strategies;
strategies
| l -> l
(**** interpretation of command-line *********************)
let sort_pair (x,_) (y,_) = String.compare x y
let list_transforms _args =
let l =
List.rev_append (Trans.list_transforms ()) (Trans.list_transforms_l ())
in
let print_trans_desc fmt (x,r) =
fprintf fmt "@[<hov 2>%s@\n@[<hov>%a@]@]" x Pp.formatted r
in
Pp.string_of (Pp.print_list Pp.newline2 print_trans_desc)
(List.sort sort_pair l)
let commands =
[
"list-transforms", "list available transformations", list_transforms;
(*
"list-provers", "list available provers", list_provers;
"list-strategies", "list available strategies", list_strategies;
"print", "<s> print the declaration where s was defined", test_print_id;
"search", "<s> print some declarations where s appear", test_search_id;
"r", "reload the session (test only)", test_reload;
"rp", "replay", test_replay;
"s", "save the current session", test_save_session;
"ng", "go to the next goal", then_print (move_to_goal_ret_p next_node);
"pg", "go to the prev goal", then_print (move_to_goal_ret_p prev_node);
"gu", "go to the goal up", then_print (move_to_goal_ret_p zipper_up);
"gd", "go to the goal down", then_print (move_to_goal_ret_p zipper_down);
"gr", "go to the goal right", then_print (move_to_goal_ret_p zipper_right);
"gl", "go to the goal left", then_print (move_to_goal_ret_p zipper_left)
*)
]
let commands_table = Stdlib.Hstr.create 17
let () =
List.iter
(fun (c,_,f) -> Stdlib.Hstr.add commands_table c f)
commands
let split_args s =
let args = ref [] in
let b = Buffer.create 17 in
let state = ref 0 in
for i = 0 to String.length s - 1 do
let c = s.[i] in
match !state, c with
| 0,' ' -> ()
| 0,'"' -> state := 1
| 0,_ -> Buffer.add_char b c; state := 2
| 1,'"' -> args := Buffer.contents b :: !args; Buffer.clear b; state := 0
| 1,_ -> Buffer.add_char b c
| 2,' ' -> args := Buffer.contents b :: !args; Buffer.clear b; state := 0
| 2,_ -> Buffer.add_char b c
| _ -> assert false
done;
begin
match !state with
| 0 -> ()
| 1 -> args := Buffer.contents b :: !args (* TODO : report missing '"' *)
| 2 -> args := Buffer.contents b :: !args
| _ -> assert false
end;
match List.rev !args with
| a::b -> a,b
| [] -> "",[]
type command =
| Transform of string * Trans.gentrans * string list
| Query of string
| Other of string * string list
let interp env s =
let cmd,args = split_args s in
try
let f = Stdlib.Hstr.find commands_table cmd in
Query (f args)
with Not_found ->
try
let t = Trans.lookup_trans env cmd in
Transform (cmd,t,args)
with Trans.UnknownTrans _ ->
Other(cmd,args)
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