Permalink
Browse files

Ide_slave: do not attempt to answer broken requests

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15960 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent 8a0d8cf commit 327d2aa33230d99f1b3fc36fee9ecbc0f5ac7813 letouzey committed Nov 12, 2012
Showing with 34 additions and 52 deletions.
  1. +34 −52 toplevel/ide_slave.ml
View
86 toplevel/ide_slave.ml
@@ -270,24 +270,19 @@ let about () = {
Interface.compile_date = Coq_config.compile_date;
}
-(** Grouping all call handlers together + error handling *)
+(** When receiving the Quit call, we don't directly do an [exit 0],
+ but rather set this reference, in order to send a final answer
+ before exiting. *)
+
+let quit = ref false
-exception Quit
+(** Grouping all call handlers together + error handling *)
let eval_call c =
let rec handle_exn e =
catch_break := false;
let pr_exn e = (read_stdout ())^("\n"^(string_of_ppcmds (Errors.print e))) in
match e with
- | Quit ->
- (* Here we do send an acknowledgement message to prove everything went
- OK. *)
- let dummy = Interface.Good () in
- let xml_answer = Serialize.of_answer Serialize.quit dummy in
- let () = Xml_utils.print_xml !orig_stdout xml_answer in
- let () = flush !orig_stdout in
- let () = pr_debug "Exiting gracefully." in
- exit 0
| Errors.Drop -> None, "Drop is not allowed by coqide!"
| Errors.Quit -> None, "Quit is not allowed by coqide!"
| Vernac.DuringCommandInterp (_,inner) -> handle_exn inner
@@ -320,7 +315,7 @@ let eval_call c =
Serialize.get_options = interruptible get_options;
Serialize.set_options = interruptible set_options;
Serialize.mkcases = interruptible Vernacentries.make_cases;
- Serialize.quit = (fun () -> raise Quit);
+ Serialize.quit = (fun () -> quit := true);
Serialize.about = interruptible about;
Serialize.handle_exn = handle_exn; }
in
@@ -345,14 +340,8 @@ let slave_logger level message =
(** The main loop *)
(** Exceptions during eval_call should be converted into [Interface.Fail]
- messages by [handle_exn] above. Otherwise, we die badly, after having
- tried to send a last message to the ide: trying to recover from errors
- with the current protocol would most probably bring desynchronisation
- between coqtop and ide. With marshalling, reading an answer to
- a different request could hang the ide... *)
-
-let fail err =
- Serialize.of_value (fun _ -> assert false) (Interface.Fail (None, err))
+ messages by [handle_exn] above. Otherwise, we die badly, without
+ trying to answer malformed requests. *)
let loop () =
init_signal_handler ();
@@ -362,36 +351,29 @@ let loop () =
Vernacentries.enable_goal_printing := false;
Vernacentries.qed_display_script := false;
Flags.make_term_color false;
- try
- while true do
- let xml_answer =
- try
- let p = Xml_parser.make (Xml_parser.SChannel stdin) in
- let xml_query = Xml_parser.parse p in
- let q = Serialize.to_call xml_query in
- let () = pr_debug ("<-- " ^ Serialize.pr_call q) in
- let r = eval_call q in
- let () = pr_debug ("--> " ^ Serialize.pr_full_value q r) in
- Serialize.of_answer q r
- with
- | Xml_parser.Error (Xml_parser.Empty, _) ->
- pr_debug ("End of input, exiting");
- exit 0
- | Xml_parser.Error (err, loc) ->
- let msg = "Syntax error in query: " ^ Xml_parser.error_msg err in
- fail msg
- | Serialize.Marshal_error ->
- fail "Incorrect query."
- in
- Xml_utils.print_xml !orig_stdout xml_answer;
- flush !orig_stdout
- done
- with e ->
- let msg = Printexc.to_string e in
- let r = "Fatal exception in coqtop:\n" ^ msg in
- pr_debug ("==> " ^ r);
- (try
- Xml_utils.print_xml !orig_stdout (fail r);
+ while not !quit do
+ try
+ let p = Xml_parser.make (Xml_parser.SChannel stdin) in
+ let xml_query = Xml_parser.parse p in
+ let q = Serialize.to_call xml_query in
+ let () = pr_debug ("<-- " ^ Serialize.pr_call q) in
+ let r = eval_call q in
+ let () = pr_debug ("--> " ^ Serialize.pr_full_value q r) in
+ Xml_utils.print_xml !orig_stdout (Serialize.of_answer q r);
flush !orig_stdout
- with _ -> ());
- exit 1
+ with
+ | Xml_parser.Error (Xml_parser.Empty, _) ->
+ pr_debug "End of input, exiting gracefully.";
+ exit 0
+ | Xml_parser.Error (err, loc) ->
+ pr_debug ("Syntax error in query: " ^ Xml_parser.error_msg err);
+ exit 1
+ | Serialize.Marshal_error ->
+ pr_debug "Incorrect query.";
+ exit 1
+ | e ->
+ pr_debug ("Fatal exception in coqtop:\n" ^ Printexc.to_string e);
+ exit 1
+ done;
+ pr_debug "Exiting gracefully.";
+ exit 0

0 comments on commit 327d2aa

Please sign in to comment.