Commit 23db7761 authored by MARCHE Claude's avatar MARCHE Claude

detection whether session needs saving handled by the ITP server

fixes issue #147
parent dfa5a323
......@@ -559,6 +559,8 @@ let interpNotif (n: notification) =
TaskList.remove_node (string_of_int nid)
| Saved ->
PE.error_print_msg "Saved"
| Saving_needed _b ->
PE.error_print_msg "Saving_needed"
| Message m ->
begin
match m with
......
......@@ -102,16 +102,9 @@ module Protocol_why3ide = struct
end
(* True when session differs from the saved session *)
let session_needs_saving = ref false
let get_notified = Protocol_why3ide.get_notified
let send_request r =
(* If request changes the session then session needs saving *)
if modify_session r then
session_needs_saving := true;
Protocol_why3ide.send_request r
let send_request r = Protocol_why3ide.send_request r
(****************************************)
(* server instance on the GTK scheduler *)
......@@ -329,7 +322,10 @@ let files_need_saving () =
(* Ask if the user wants to save session before exit. Exit is then delayed until
the [Saved] notification is received *)
let exit_function_safe () =
if not !session_needs_saving && not (files_need_saving ()) then
send_request Check_need_saving_req
let exit_function_handler b =
if not b && not (files_need_saving ()) then
exit_function_unsafe ()
else
let answer =
......@@ -2412,11 +2408,11 @@ let treat_notification n =
complete_context_menu ();
Opt.iter select_iter goals_model#get_iter_first
| Saved ->
session_needs_saving := false;
print_message ~kind:1 ~notif_kind:"Saved action info"
"Session saved.";
if !quit_on_saved = true then
exit_function_safe ()
| Saving_needed b -> exit_function_handler b
| Message (msg) -> treat_message_notification msg
| Task (id, s, list_loc) ->
if is_selected_alone id then
......
......@@ -89,6 +89,8 @@ type notification =
next unproven node from this node *)
| Initialized of global_information
(* initial global data *)
| Saving_needed of bool
(* the session needs saving when argument is true *)
| Saved
(* the session was saved on disk *)
| Message of message_notification
......@@ -118,21 +120,11 @@ type ide_request =
| Unfocus_req
| Save_req
| Reload_req
| Check_need_saving_req
| Exit_req
| Interrupt_req
| Get_global_infos
(* Return true if the request modify the session *)
let modify_session (r: ide_request) =
match r with
| Command_req _ | Add_file_req _ | Remove_subtree _ | Copy_paste _
| Reload_req -> true
| Set_config_param _ | Set_prover_policy _ | Get_file_contents _
| Get_task _ | Save_file_req _ | Get_first_unproven_node _
| Unfocus_req | Save_req | Exit_req | Get_global_infos
| Interrupt_req -> false
(* Debugging functions *)
......@@ -155,6 +147,7 @@ let print_request fmt r =
| Unfocus_req -> fprintf fmt "unfocus"
| Save_req -> fprintf fmt "save"
| Reload_req -> fprintf fmt "reload"
| Check_need_saving_req -> fprintf fmt "check need saving"
| Exit_req -> fprintf fmt "exit"
| Interrupt_req -> fprintf fmt "interrupt"
| Get_global_infos -> fprintf fmt "get_global_infos"
......@@ -201,6 +194,7 @@ let print_notify fmt n =
| Remove _ni -> fprintf fmt "remove"
| Next_Unproven_Node_Id (ni, nj) -> fprintf fmt "next unproven node_id from %d is %d" ni nj
| Initialized _gi -> fprintf fmt "initialized"
| Saving_needed b -> fprintf fmt "saving needed=%b" b
| Saved -> fprintf fmt "saved"
| Message msg ->
print_msg fmt msg
......
......@@ -99,8 +99,10 @@ type notification =
next unproven node from this node *)
| Initialized of global_information
(** initial global data *)
| Saving_needed of bool
(** the session needs saving when argument is true *)
| Saved
(** the session was saved on disk *)
(** the session was just saved on disk *)
| Message of message_notification
(** an informative message, can be an error message *)
| Dead of string
......@@ -136,13 +138,11 @@ type ide_request =
| Unfocus_req
| Save_req
| Reload_req
| Check_need_saving_req
| Exit_req
| Interrupt_req
| Get_global_infos
(* Return true if the request modify the session *)
val modify_session: ide_request -> bool
val print_request: Format.formatter -> ide_request -> unit
val print_msg: Format.formatter -> message_notification -> unit
......
......@@ -489,7 +489,7 @@ let get_modified_node n =
| Remove nid -> Some nid
| Next_Unproven_Node_Id (_, nid) -> Some nid
| Initialized _ -> None
| Saved -> None
| Saved | Saving_needed _ -> None
| Message _ -> None
| Dead _ -> None
| Task (nid, _, _) -> Some nid
......@@ -927,22 +927,24 @@ end
(* -------------------- *)
(* True when session differs from the saved session *)
let session_needs_saving = ref false
(* Add a file into the session when (Add_file_req f) is sent *)
(* Note that f is the path from execution directory to the file and fn is the
path from the session directory to the file. *)
let add_file_to_session cont f =
let fn = Sysutil.relativize_filename
(get_dir cont.controller_session) f in
let fn_exists =
try Some (get_file cont.controller_session fn)
with | Not_found -> None
in
match fn_exists with
| None ->
if (Sys.file_exists f) then
begin
match add_file cont f with
| [] ->
try
let (_ : file) = get_file cont.controller_session fn in
P.notify (Message (Information ("File already in session: " ^ fn)))
with Not_found ->
if (Sys.file_exists f) then
begin
match add_file cont f with
| [] ->
session_needs_saving := true;
let file = get_file cont.controller_session fn in
send_new_subtree_from_file file;
read_and_send (file_name file);
......@@ -957,7 +959,6 @@ end
end
else
P.notify (Message (Open_File_Error ("File not found: " ^ f)))
| Some _ -> P.notify (Message (Information ("File already in session: " ^ fn)))
(* ------------ init server ------------ *)
......@@ -1302,7 +1303,8 @@ end
(* Check if a request is valid (does not suppose existence of obsolete node_id) *)
let request_is_valid r =
match r with
| Save_req | Reload_req | Get_file_contents _ | Save_file_req _
| Save_req | Check_need_saving_req | Reload_req
| Get_file_contents _ | Save_file_req _
| Interrupt_req | Add_file_req _ | Set_config_param _ | Set_prover_policy _
| Exit_req | Get_global_infos | Itp_communication.Unfocus_req -> true
| Get_first_unproven_node ni ->
......@@ -1321,101 +1323,95 @@ end
(* ----------------- treat_request -------------------- *)
let treat_request r =
let d = get_server_data () in
(* Check that the request does not refer to obsolete node_ids *)
if not (request_is_valid r) then
begin
(* These errors come from the client-server behavior of itp. They cannot
be completely avoided and could be safely ignored.
They are ignored if a debug flag is not added.
*)
if Debug.test_flag Debug.stack_trace then
raise Not_found;
if Debug.test_flag debug then
P.notify (Message (Error (Pp.string_of
(fun fmt r -> Format.fprintf fmt
"The following request refer to obsolete node_ids:\n %a\n"
Itp_communication.print_request r) r)))
end
else
try (
match r with
| Get_global_infos ->
let d= get_server_data () in
Debug.dprintf debug "sending initialization infos@.";
P.notify (Initialized d.global_infos)
| Save_req -> save_session ()
| Reload_req -> reload_session ()
let treat_request d r =
match r with
| Get_global_infos ->
Debug.dprintf debug "sending initialization infos@.";
P.notify (Initialized d.global_infos)
| Save_req ->
save_session ();
session_needs_saving := false
| Reload_req ->
reload_session ();
session_needs_saving := true
| Get_first_unproven_node ni ->
notify_first_unproven_node d ni
| Remove_subtree nid -> remove_node nid
| Copy_paste (from_id, to_id) ->
let from_any = any_from_node_ID from_id in
let to_any = any_from_node_ID to_id in
begin
try
C.copy_paste
~notification:(notify_change_proved d.cont)
~callback_pa:(callback_update_tree_proof d.cont)
~callback_tr:(callback_update_tree_transform)
d.cont from_any to_any
with C.BadCopyPaste ->
P.notify (Message (Error "invalid copy"))
end
notify_first_unproven_node d ni
| Remove_subtree nid ->
remove_node nid;
session_needs_saving := true
| Copy_paste (from_id, to_id) ->
let from_any = any_from_node_ID from_id in
let to_any = any_from_node_ID to_id in
begin
try
C.copy_paste
~notification:(notify_change_proved d.cont)
~callback_pa:(callback_update_tree_proof d.cont)
~callback_tr:(callback_update_tree_transform)
d.cont from_any to_any;
session_needs_saving := true
with C.BadCopyPaste ->
P.notify (Message (Error "invalid copy"))
end
| Get_file_contents f ->
read_and_send f
read_and_send f
| Save_file_req (name, text) ->
save_file name text;
| Get_task(nid,b,loc) -> send_task nid b loc
| Interrupt_req -> C.interrupt ()
save_file name text
| Check_need_saving_req ->
P.notify (Saving_needed !session_needs_saving)
| Get_task(nid,b,loc) ->
send_task nid b loc
| Interrupt_req ->
C.interrupt ()
| Command_req (nid, cmd) ->
begin
let snid = try Some(any_from_node_ID nid) with Not_found -> None in
match interp commands_table d.cont snid cmd with
| Transform (s, _t, args) -> apply_transform nid s args
| Query s -> P.notify (Message (Query_Info (nid, s)))
| Prove (p, limit) ->
schedule_proof_attempt nid p limit
let snid = try Some(any_from_node_ID nid) with Not_found -> None in
begin
match interp commands_table d.cont snid cmd with
| Transform (s, _t, args) ->
apply_transform nid s args;
session_needs_saving := true
| Query s ->
P.notify (Message (Query_Info (nid, s)))
| Prove (p, limit) ->
schedule_proof_attempt nid p limit;
session_needs_saving := true
| Strategies st ->
run_strategy_on_task nid st
| Edit p -> schedule_edition nid p
| Bisect -> schedule_bisection nid
| Replay valid_only -> replay ~valid_only snid
| Clean -> clean snid
| Mark_Obsolete -> mark_obsolete snid
run_strategy_on_task nid st;
session_needs_saving := true
| Edit p ->
schedule_edition nid p;
session_needs_saving := true
| Bisect ->
schedule_bisection nid;
session_needs_saving := true
| Replay valid_only ->
replay ~valid_only snid;
session_needs_saving := true
| Clean ->
clean snid;
session_needs_saving := true
| Mark_Obsolete ->
mark_obsolete snid;
session_needs_saving := true
| Focus_req ->
let d = get_server_data () in
let s = d.cont.controller_session in
let any = any_from_node_ID nid in
let focus_on =
match any with
| APa pa -> APn (Session_itp.get_proof_attempt_parent s pa)
| _ -> any
in
focused_node := Focus_on [focus_on];
reset_and_send_the_whole_tree ()
let d = get_server_data () in
let s = d.cont.controller_session in
let any = any_from_node_ID nid in
let focus_on =
match any with
| APa pa -> APn (Session_itp.get_proof_attempt_parent s pa)
| _ -> any
in
focused_node := Focus_on [focus_on];
reset_and_send_the_whole_tree ()
| Server_utils.Unfocus_req -> unfocus ()
| Help_message s -> P.notify (Message (Information s))
| QError s -> P.notify (Message (Query_Error (nid, s)))
| Other (s, _args) ->
P.notify (Message (Information ("Unknown command: "^s)))
P.notify (Message (Information ("Unknown command: "^s)))
end
| Add_file_req f ->
add_file_to_session d.cont f;
(* let f = Sysutil.relativize_filename
(Session_itp.get_dir d.cont.controller_session) f in
read_and_send f *)
()
(*
| Open_session_req file_or_dir_name ->
let b = init_cont file_or_dir_name in
if b then
reload_session ()
else
() (* Eventually print debug here *)
*)
add_file_to_session d.cont f
| Set_config_param(s,i) ->
begin
match s with
......@@ -1429,16 +1425,40 @@ end
Controller_itp.set_session_prover_upgrade_policy c p u
| Unfocus_req -> unfocus ()
| Exit_req -> exit 0
)
with
| C.TransAlreadyExists (name,args) ->
P.notify (Message (Error
(Pp.sprintf "Transformation %s with arg [%s] already exists" name args)))
| e when not (Debug.test_flag Debug.stack_trace)->
P.notify (Message (Error (Pp.string_of
(fun fmt (r,e) -> Format.fprintf fmt
"There was an unrecoverable error during treatment of request:\n %a\nwith exception: %a"
print_request r Exn_printer.exn_printer e ) (r, e))))
let treat_request r =
let d = get_server_data () in
(* Check that the request does not refer to obsolete node_ids *)
if not (request_is_valid r) then
begin
(* These errors come from the client-server behavior of itp. They cannot
be completely avoided and could be safely ignored.
They are ignored if a debug flag is not added.
*)
if Debug.test_flag Debug.stack_trace then
raise Not_found;
if Debug.test_flag debug then
P.notify (Message (Error (Pp.string_of
(fun fmt r -> Format.fprintf fmt
"The following request refer to obsolete node_ids:\n %a\n"
Itp_communication.print_request r) r)))
end
else
try treat_request d r
with
| C.TransAlreadyExists (name,args) ->
P.notify
(Message
(Error
(Pp.sprintf "Transformation %s with arg [%s] already exists"
name args)))
| e when not (Debug.test_flag Debug.stack_trace)->
P.notify
(Message
(Error
(Pp.sprintf
"There was an unrecoverable error during treatment of request:\n %a\nwith exception: %a"
print_request r Exn_printer.exn_printer e)))
let treat_requests () : bool =
List.iter treat_request (P.get_requests ());
......
......@@ -137,6 +137,7 @@ let convert_notification_constructor n =
| Next_Unproven_Node_Id (_, _) -> String "Next_Unproven_Node_Id"
| Initialized _ -> String "Initialized"
| Saved -> String "Saved"
| Saving_needed _ -> String "Saving_needed"
| Message _ -> String "Message"
| Dead _ -> String "Dead"
| Task _ -> String "Task"
......@@ -169,6 +170,7 @@ let convert_request_constructor (r: ide_request) =
| Get_first_unproven_node _ -> String "Get_first_unproven_node"
| Unfocus_req -> String "Unfocus_req"
| Save_req -> String "Save_req"
| Check_need_saving_req -> String "Check_need_saving_req"
| Reload_req -> String "Reload_req"
| Exit_req -> String "Exit_req"
| Interrupt_req -> String "Interrupt_req"
......@@ -220,7 +222,8 @@ let print_request_to_json (r: ide_request): Json_base.json =
"node_ID2", Int to_id]
| Get_first_unproven_node id ->
convert_record ["ide_request", cc r;
"node_ID", Int id]
"node_ID", Int id]
| Check_need_saving_req
| Unfocus_req
| Save_req
| Reload_req
......@@ -384,9 +387,12 @@ let print_notification_to_json (n: notification): json =
"infos", convert_infos infos]
| Saved ->
convert_record ["notification", cc n]
| Saving_needed b ->
convert_record ["notification", cc n;
"need_saving", Bool b]
| Message m ->
convert_record ["notification", cc n;
"message", convert_message m]
"message", convert_message m]
| Dead s ->
convert_record ["notification", cc n;
"message", String s]
......
......@@ -250,6 +250,8 @@ let treat_notification fmt n =
fprintf fmt "Initialized@."
| Saved -> (* TODO *)
fprintf fmt "got a Saved notification not yet supported@."
| Saving_needed _b -> (* TODO *)
fprintf fmt "got a Saving_needed notification not yet supported@."
| Message (msg) -> treat_message_notification fmt msg
| Dead _s -> (* TODO *)
fprintf fmt "got a Dead notification not yet supported@."
......
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