Tentative heuristic fix to handle lexer failures from CoqIDE when

cutting XML phrases carelessly.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16238 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 76 insertions, 54 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index d31ed9d1b..fd6de80d1 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -349,69 +349,91 @@ let is_blank s pos =
     true
   with Not_found -> false
 
-let install_input_watch handle respawner =
-  let io_chan = Glib.Io.channel_of_descr handle.cout in
-  let all_conds = [`ERR; `HUP; `IN; `NVAL; `PRI] in (* all except `OUT *)
-  let last_fragment = ref "" in
-  let rec check_errors = function
-    | [] -> ()
-    | (`IN | `PRI) :: conds -> check_errors conds
-    | e :: _ -> raise TubeError
-  in
-  let handle_intermediate_message logger xml =
-    let message = Serialize.to_message xml in
-    let level = message.Interface.message_level in
-    let content = message.Interface.message_content in
-    logger level content
+let rec check_errors = function
+| [] -> ()
+| (`IN | `PRI) :: conds -> check_errors conds
+| e :: _ -> raise TubeError
+
+let handle_intermediate_message logger xml =
+  let message = Serialize.to_message xml in
+  let level = message.Interface.message_level in
+  let content = message.Interface.message_content in
+  logger level content
+
+let handle_final_answer handle ccb xml =
+  let () = Minilib.log "Handling coqtop answer" in
+  let () = handle.waiting_for <- None in
+  with_ccb ccb { bind_ccb = fun (c, f) -> f (Serialize.to_answer xml c) }
+
+type input_state = {
+  mutable fragment : string;
+  mutable lexerror : int option;
+}
+
+let unsafe_handle_input handle state conds =
+  let chan = Glib.Io.channel_of_descr handle.cout in
+  let () = check_errors conds in
+  let s = io_read_all chan in
+  let () = if String.length s = 0 then raise TubeError in
+  let s = state.fragment ^ s in
+  let () = state.fragment <- s in
+  let ccb, logger = match handle.waiting_for with
+  | None -> raise AnswerWithoutRequest
+  | Some (c, l) -> c, l
   in
-  let handle_final_answer ccb xml =
-    Minilib.log "Handling coqtop answer";
-    handle.waiting_for <- None;
-    with_ccb ccb { bind_ccb = fun (c,f) -> f (Serialize.to_answer xml c) }
+  let lex = Lexing.from_string s in
+  let p = Xml_parser.make (Xml_parser.SLexbuf lex) in
+  let rec loop () =
+    let xml = Xml_parser.parse p in
+    let l_end = Lexing.lexeme_end lex in
+    if Serialize.is_message xml then
+      let remaining = String.sub s l_end (String.length s - l_end) in
+      let () = state.fragment <- remaining in
+      let () = state.lexerror <- None in
+      let () = handle_intermediate_message logger xml in
+      loop ()
+    else
+      (* We should have finished decoding s *)
+      let () = if not (is_blank s l_end) then raise AnswerWithoutRequest in
+      let () = state.fragment <- "" in
+      let () = state.lexerror <- None in
+      ignore (handle_final_answer handle ccb xml)
   in
-  let unsafe_handle_input conds =
-    check_errors conds;
-    let s = io_read_all io_chan in
-    if s = "" then raise TubeError;
-    let s = !last_fragment ^ s in
-    let ccb,logger = match handle.waiting_for with
-      |None -> raise AnswerWithoutRequest
-      |Some (c,l) -> c,l
+  try loop ()
+  with Xml_parser.Error _ as e ->
+    (* Parsing error at the end of s : we have only received a part of
+        an xml answer. We store the current fragment for later *)
+    let l_end = Lexing.lexeme_end lex in
+    (** Heuristic hack not to reimplement the lexer:  if ever the lexer dies
+        twice at the same place, then this is a non-recoverable error *)
+    let () = match state.lexerror with
+    | None -> ()
+    | Some loc -> if loc = l_end then raise e
     in
-    let lex = Lexing.from_string s in
-    let finished () = (Lexing.lexeme_end lex = String.length s) in
-    let p = Xml_parser.make (Xml_parser.SLexbuf lex) in
-    let xml_end = ref 0 in
-    let rec loop () =
-      let xml = Xml_parser.parse p in
-      xml_end := Lexing.lexeme_end lex;
-      if Serialize.is_message xml then
-	(handle_intermediate_message logger xml; loop ())
-      else begin
-        (* We should have finished decoding s *)
-        if not (is_blank s !xml_end) then raise AnswerWithoutRequest;
-        last_fragment := "";
-	ignore (handle_final_answer ccb xml)
-      end
-    in
-    try loop ()
-    with Xml_parser.Error _ when finished () ->
-      (* Parsing error at the end of s : we have only received a part of
-         an xml answer. We store the current fragment for later *)
-      last_fragment := String.sub s !xml_end (String.length s - !xml_end)
-  in
+    let () = state.lexerror <- Some l_end in
+    ()
+
+let install_input_watch handle respawner =
+  let io_chan = Glib.Io.channel_of_descr handle.cout in
+  let all_conds = [`ERR; `HUP; `IN; `NVAL; `PRI] in (* all except `OUT *)
+  let state = {
+    fragment = "";
+    lexerror = None;
+  } in
   let print_exception = function
-    | Xml_parser.Error e -> Xml_parser.error e
-    | Serialize.Marshal_error -> "Protocol violation"
-    | e -> Printexc.to_string e
+  | Xml_parser.Error e -> Xml_parser.error e
+  | Serialize.Marshal_error -> "Protocol violation"
+  | e -> Printexc.to_string e
   in
   let handle_input conds =
     if not handle.alive then false (* coqtop already terminated *)
     else
-      try unsafe_handle_input conds; true
+      try
+        let () = unsafe_handle_input handle state conds in
+        true
       with e ->
-	Minilib.log ("Coqtop reader failed, resetting: "^print_exception e);
-	respawner ();
+	let () = Minilib.log ("Coqtop reader failed, resetting: "^print_exception e) in
+	let () = respawner () in
 	false
   in
   ignore (Glib.Io.add_watch ~cond:all_conds ~callback:handle_input io_chan)