diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml index fef74f2b59fad29b353e4749c25040ac90f92ea6..789dba0ab627fa5717f964644804d085334cb7bb 100644 --- a/src/session/itp_server.ml +++ b/src/session/itp_server.ml @@ -1346,6 +1346,16 @@ end Ident.Hid.clear th_to_node_ID; Hfile.clear file_to_node_ID + let notify_parsing_errors l = + List.iter + (function (loc,rel_loc,s) -> + P.notify (Message (Parse_Or_Type_Error(loc,rel_loc,s)))) + l + + (* Save the last parsing errors that occured. Report them when an invalid + command (transformation/etc) is entered before reloading. *) + let parsing_errors = ref [] + let reload_session () : unit = let d = get_server_data () in (* interrupt all running provers and unfocus before reload *) @@ -1356,16 +1366,16 @@ end let l = reload_files d.cont ~shape_version:(Some Termcode.current_shape_version) in - reset_and_send_the_whole_tree (); match l with | [] -> (* TODO: try to restore the previous focus : focused_node := old_focus; *) + (* Only reset the tree when there is no errors (for efficiency of ide) *) + parsing_errors := []; + reset_and_send_the_whole_tree (); P.notify (Message (Information "Session refresh successful")) | l -> - List.iter - (function (loc,rel_loc,s) -> - P.notify (Message (Parse_Or_Type_Error(loc,rel_loc,s)))) - l + parsing_errors := l; + notify_parsing_errors l let replay ~valid_only nid : unit = let d = get_server_data () in @@ -1598,6 +1608,14 @@ end (* Check that the request does not refer to obsolete node_ids *) if not (request_is_valid r) then begin + if !parsing_errors <> [] then begin + (* There were parsing errors and no reloads. *) + P.notify (Message (Error "Cannot handle this command while the \ + parsing error is not resolved. You can try \ + reloading the session or removing detached \ + files.")); + notify_parsing_errors !parsing_errors + end; (* 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.