Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 1e2bd400 authored by MARCHE Claude's avatar MARCHE Claude

why3ide: command "help"

parent 8b24920e
...@@ -561,18 +561,18 @@ let run_strategy_on_task s = ...@@ -561,18 +561,18 @@ let run_strategy_on_task s =
let clear_command_entry () = command_entry#set_text "" let clear_command_entry () = command_entry#set_text ""
let current_id id =
match id with
| IproofNode id -> id
| _ -> assert (false) (* TODO *)
let interp cmd = let interp cmd =
let id = current_id !current_selected_index in let id =
match !current_selected_index with
| IproofNode id -> Some id
| _ -> None
in
match interp cont.controller_env id cont.controller_session cmd with match interp cont.controller_env id cont.controller_session cmd with
| Transform(s,_t,args) -> | Transform(s,_t,args) ->
clear_command_entry (); clear_command_entry ();
apply_transform cont.controller_session s args apply_transform cont.controller_session s args
| Query s -> | Query s ->
clear_command_entry ();
message_zone#buffer#set_text s message_zone#buffer#set_text s
| Other(s,args) -> | Other(s,args) ->
begin begin
...@@ -582,22 +582,29 @@ let interp cmd = ...@@ -582,22 +582,29 @@ let interp cmd =
test_schedule_proof_attempt cont.controller_session prover_config limit test_schedule_proof_attempt cont.controller_session prover_config limit
| None -> | None ->
match s with match s with
| "auto" -> | "auto" ->
let s = let s =
match args with match args with
| "2"::_ -> "2" | "2"::_ -> "2"
| _ -> "1" | _ -> "1"
in in
clear_command_entry (); clear_command_entry ();
run_strategy_on_task s run_strategy_on_task s
| _ -> message_zone#buffer#set_text ("unknown command '"^s^"'") | "help" ->
clear_command_entry ();
let text = Pp.sprintf
"Please type a command among the following (automatic completion available)@\n\
@\n\
@ <transformation name> [arguments]@\n\
@ <prover name> [<time limit> [<mem limit>]]@\n\
@ <query> [arguments]@\n\
@ auto [auto level]@\n\
@\n\
Available queries are:@\n@[%a@]" help_on_queries ()
in
message_zone#buffer#set_text text
| _ -> message_zone#buffer#set_text ("unknown command '"^s^"'")
end end
(*
match s with
| "c" -> clear_command_entry ();
test_schedule_proof_attempt cont.controller_session
| _ -> message_zone#buffer#set_text ("unknown command '"^s^"'")
*)
let (_ : GtkSignal.id) = let (_ : GtkSignal.id) =
command_entry#connect#activate command_entry#connect#activate
......
...@@ -246,6 +246,12 @@ let commands = ...@@ -246,6 +246,12 @@ let commands =
*) *)
] ]
let help_on_queries fmt () =
let l = List.rev_map (fun (c,h,_) -> (c,h)) commands in
let l = List.sort sort_pair l in
let p fmt (c,help) = fprintf fmt "%20s : %s" c help in
Format.fprintf fmt "%a" (Pp.print_list Pp.newline p) l
let commands_table = Stdlib.Hstr.create 17 let commands_table = Stdlib.Hstr.create 17
let () = let () =
List.iter List.iter
...@@ -285,17 +291,20 @@ type command = ...@@ -285,17 +291,20 @@ type command =
| Other of string * string list | Other of string * string list
let interp env id ses s = let interp env id ses s =
let task = Session_itp.get_task ses id in
let cmd,args = split_args s in let cmd,args = split_args s in
try try
let f = Stdlib.Hstr.find commands_table cmd in let f = Stdlib.Hstr.find commands_table cmd in
Query (f task args) match id with
| None -> Query "please select a goal first"
| Some id ->
let task = Session_itp.get_task ses id in
Query (f task args)
with Not_found -> with Not_found ->
try try
let t = Trans.lookup_trans env cmd in let t = Trans.lookup_trans env cmd in
Transform (cmd,t,args) Transform (cmd,t,args)
with Trans.UnknownTrans _ -> with Trans.UnknownTrans _ ->
Other(cmd,args) Other(cmd,args)
(********* Callbacks tools *******) (********* Callbacks tools *******)
......
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