Commit d0d5849b authored by MARCHE Claude's avatar MARCHE Claude

Various improvements in IDEs

- handling missing queries and notifications
- turn strategie messages into true debug messages
- trying to grab the focus in the entry zone as much as possible
- write_file put in sysutil
parent d0e1f7b5
......@@ -539,7 +539,9 @@ let interpNotif (n: notification) =
TaskList.onclick_do_something (string_of_int nid);
sendRequest (Get_task (string_of_int nid))
| File_contents (_f,_s) ->
assert false (* TODO *)
PE.error_print_msg "Notification File_contents not handled yet"
| Next_Unproven_Node_Id (_nid1,_nid2) ->
PE.error_print_msg "Notification Next_Unproven_Node_Id not handled yet"
| Task (nid, task) ->
Hashtbl.add TaskList.printed_task_list (string_of_int nid) task
| Remove nid ->
......
......@@ -833,9 +833,12 @@ let on_selected_row r =
let (_ : GtkSignal.id) =
goals_view#selection#connect#after#changed ~callback:
(fun () ->
match get_selected_row_references () with
| [r] -> on_selected_row r
| _ -> ())
begin
match get_selected_row_references () with
| [r] -> on_selected_row r
| _ -> ()
end (* ;
command_entry#misc#grab_focus () *))
let remove_item: GMenu.menu_item =
file_factory#add_item "Remove"
......@@ -1009,7 +1012,11 @@ let if_selected_alone id f =
if i = id || Some i = get_parent id then f id
| _ -> ()
let treat_notification n = match n with
let treat_notification n =
(* temporary: this should be better executed each time
one clicks on the tree view *)
command_entry#misc#grab_focus ();
match n with
| Node_change (id, uinfo) ->
begin
match uinfo with
......@@ -1032,6 +1039,11 @@ let treat_notification n = match n with
goals_view#selection#select_iter iter)
| New_node (id, parent_id, typ, name, detached) ->
begin
let name =
if typ = NGoal then
List.hd (Strings.rev_split '.' name)
else name
in
try
let parent = get_node_row parent_id in
ignore (new_node ~parent id name typ false detached)
......
......@@ -434,9 +434,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
let d = get_server_data() in
let fn = Sysutil.absolutize_filename
(Session_itp.get_dir d.cont.controller_session) f in
let oc = open_out fn in
Printf.fprintf oc "%s\n" file_content; (* TODO replace this *)
close_out oc;
Sysutil.write_file fn file_content;
P.notify (Message (File_Saved f))
with Invalid_argument s ->
P.notify (Message (Error s))
......@@ -856,6 +854,8 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
(* ----------------- run strategy -------------------- *)
let debug_strat = Debug.register_flag "strategy_exec" ~desc:"Trace strategies execution"
let run_strategy_on_task nid s =
let d = get_server_data () in
let unproven_goals = unproven_goals_below_id d.cont (any_from_node_ID nid) in
......@@ -863,16 +863,16 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
let st = List.filter (fun (_,c,_,_) -> c=s) l in
match st with
| [(n,_,_,st)] ->
Format.printf "running strategy '%s'@." n;
Debug.dprintf debug_strat "[strategy_exec] running strategy '%s'@." n;
let callback sts =
Format.printf "Strategy status: %a@." print_strategy_status sts
Debug.dprintf debug_strat "[strategy_exec] strategy status: %a@." print_strategy_status sts
in
let callback_pa = callback_update_tree_proof d.cont in
let callback_tr st = callback_update_tree_transform st in
List.iter (fun id ->
C.run_strategy_on_goal d.cont id st ~callback_pa ~callback_tr ~callback ~notification:notify_change_proved)
unproven_goals
| _ -> Format.printf "Strategy '%s' not found@." s
| _ -> Debug.dprintf debug_strat "[strategy_exec] strategy '%s' not found@." s
(* ----------------- Save session --------------------- *)
let save_session () =
......
......@@ -116,6 +116,7 @@ let convert_request_constructor (r: ide_request) =
| Strategy_req _ -> String "Strategy_req"
| Open_session_req _ -> String "Open_session_req"
| Add_file_req _ -> String "Add_file_req"
| Save_file_req _ -> String "Save_file_req"
| Set_max_tasks_req _ -> String "Set_max_tasks_req"
| Get_file_contents _ -> String "Get_file_contents"
| Get_task _ -> String "Get_task"
......@@ -156,6 +157,9 @@ let print_request_to_json (r: ide_request): Json_base.value =
| Add_file_req f ->
Obj ["ide_request", cc r;
"file", String f]
| Save_file_req (f,_) ->
Obj ["ide_request", cc r;
"file", String f]
| Set_max_tasks_req n ->
Obj ["ide_request", cc r;
"tasks", Int n]
......@@ -203,7 +207,7 @@ let convert_constructor_message (m: message_notification) =
| Parse_Or_Type_Error _ -> String "Parse_Or_Type_Error"
| Error _ -> String "Error"
| Open_File_Error _ -> String "Open_File_Error"
| File_Saved _ -> String "File_Saved"
let convert_message (m: message_notification) =
let cc = convert_constructor_message in
......@@ -249,6 +253,9 @@ let convert_message (m: message_notification) =
| Open_File_Error s ->
Obj ["mess_notif", cc m;
"open_error", String s]
| File_Saved s ->
Obj ["mess_notif", cc m;
"information", String s]
let print_notification_to_json (n: notification): Json_base.value =
let cc = convert_notification_constructor in
......@@ -525,8 +532,7 @@ let parse_message j =
| _ -> raise NotMessage
exception NotNotification
exception NotNotification of string
let parse_notification constr l =
match constr, l with
......@@ -551,13 +557,19 @@ let parse_notification constr l =
| "Task", ["node_ID", Int nid;
"task", String s] ->
Task (nid, s)
| _ -> raise NotNotification
| "Next_Unproven_Node_Id", [ "node_ID", Int nid1;
"node_ID", Int nid2 ] ->
Next_Unproven_Node_Id (nid1, nid2)
| "File_contents", [ "file", String f;
"content", String s ] ->
File_contents(f,s)
| s, _ -> raise (NotNotification ("<from parse_notification> " ^ s))
let parse_notification_json j =
match j with
| Obj (("notification", String constr) :: l) ->
parse_notification constr l
| _ -> raise NotNotification
| _ -> raise (NotNotification "<from parse_notification_json>")
let parse_json_object (s: string) =
let lb = Lexing.from_string s in
......
open Format
(* TODO: all occurences of Format.eprintf in this file should be
replaced by proper server notifications *)
open Session_itp
exception NotADirectory of string
......@@ -16,13 +21,13 @@ let cont_from_session_dir cont dir =
end
else
begin
eprintf "'%s' does not exist. \
Format.eprintf "[session server info] '%s' does not exist. \
Creating directory of that name for the project@." dir;
Unix.mkdir dir 0o777
end;
(* we load the session *)
let ses,use_shapes = load_session dir in
eprintf "using shapes: %a@." pp_print_bool use_shapes;
Format.eprintf "[session server info] using shapes: %b@." use_shapes;
(* create the controller *)
Controller_itp.init_controller ses cont;
(* update the session *)
......@@ -51,7 +56,7 @@ let list_transforms () =
let list_transforms_query _cont _args =
let l = list_transforms () in
let print_trans_desc fmt (x,r) =
fprintf fmt "@[<hov 2>%s@\n@[<hov>%a@]@]" x Pp.formatted r
Format.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)
......@@ -116,10 +121,9 @@ type query =
let help_on_queries fmt commands =
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
let p fmt (c,help) = Format.fprintf fmt "%20s : %s" c help in
Format.fprintf fmt "%a" (Pp.print_list Pp.newline p) l
(* TODO remove reference to eprintf in this *)
let strategies env config loaded_strategies =
match !loaded_strategies with
| [] ->
......@@ -132,11 +136,11 @@ let strategies env config loaded_strategies =
let code = st.Whyconf.strategy_code in
let code = Strategy_parser.parse2 env config code in
let shortcut = st.Whyconf.strategy_shortcut in
Format.eprintf "[Why3shell] Strategy '%s' loaded.@." name;
Format.eprintf "[session server info] Strategy '%s' loaded.@." name;
(name, shortcut, st.Whyconf.strategy_desc, code) :: acc
with Strategy_parser.SyntaxError msg ->
Format.eprintf
"[Why3shell warning] Loading strategy '%s' failed: %s@." name msg;
"[session server warning] Loading strategy '%s' failed: %s@." name msg;
acc)
[]
strategies
......@@ -157,7 +161,7 @@ let return_prover name config =
(** all provers that have the name/version/altern name *)
let provers = Whyconf.filter_provers config fp in
if Whyconf.Mprover.is_empty provers then begin
(*Format.eprintf "Prover corresponding to %s has not been found@." name;*)
Format.eprintf "Prover corresponding to %s has not been found@." name;
None
end else
Some (snd (Whyconf.Mprover.choose provers))
......
......@@ -62,6 +62,11 @@ let file_contents_buf f =
let file_contents f = Buffer.contents (file_contents_buf f)
let write_file f c =
let oc = open_out f in
output_string oc c;
close_out oc
let open_temp_file ?(debug=false) filesuffix usefile =
let file,cout = Filename.open_temp_file "why" filesuffix in
try
......
......@@ -33,6 +33,9 @@ val file_contents_buf : string -> Buffer.t
(* put the content of a file in a formatter *)
val file_contents_fmt : string -> Format.formatter -> unit
(* [write_file f c] writes the content [c] into the file [f] *)
val write_file : string -> string -> unit
val open_temp_file :
?debug:bool -> (* don't remove the file *)
string -> (string -> out_channel -> 'a) -> 'a
......
......@@ -102,6 +102,7 @@ let treat_message_notification fmt msg = match msg with
| Replay_Info s -> fprintf fmt "%s@." s
| Query_Info (_id, s) -> fprintf fmt "%s@." s
| Query_Error (_id, s) -> fprintf fmt "%s@." s
| File_Saved s -> fprintf fmt "%s@." s
| Help s -> fprintf fmt "%s@. Additionally for shell:\n\
goto n -> focuse on n\n\
ng -> next node\n\
......
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