Ide_slave: better handling of Ctrl-C

 - During input and output to coqide, we postpone Ctrl-C instead of ignoring
 them. For that we use Util.interrupt and Util.check_for_interrupt.
 - During evaluation of coqide requests, a Ctrl-C directly raises Sys.break,
 which is more reliable than waiting for the next Util.check_for_interrupt

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

4 files changed, 44 insertions, 35 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 89129b8c3..aea560eed 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -119,7 +119,7 @@ let is_in_loadpath coqtop s = eval_call coqtop (Ide_intf.is_in_loadpath s)
  
 let raw_interp coqtop s = eval_call coqtop (Ide_intf.raw_interp s)
 
-let interp coqtop b s = eval_call coqtop (Ide_intf.interp b s)
+let interp coqtop b s = eval_call coqtop (Ide_intf.interp (b,s))
 
 let rewind coqtop i = eval_call coqtop (Ide_intf.rewind i)
  
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index 534f181af..a0bf5e429 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -32,7 +32,7 @@ let is_in_loadpath s : bool call =
 let raw_interp s : unit call =
   Raw_interp s
 
-let interp b s : int call =
+let interp (b,s) : int call =
   Interp (b,s)
 
 let rewind i : int call =
@@ -61,7 +61,7 @@ type 'a value =
 type handler = {
   is_in_loadpath : string -> bool;
   raw_interp : string -> unit;
-  interp : bool -> string -> int;
+  interp : bool * string -> int;
   rewind : int -> int;
   read_stdout : unit -> string;
   current_goals : unit -> goals;
@@ -74,7 +74,7 @@ let abstract_eval_call handler explain_exn c =
     let res = match c with
       | In_loadpath s -> Obj.magic (handler.is_in_loadpath s)
       | Raw_interp s -> Obj.magic (handler.raw_interp s)
-      | Interp (b,s) -> Obj.magic (handler.interp b s)
+      | Interp (b,s) -> Obj.magic (handler.interp (b,s))
       | Rewind i -> Obj.magic (handler.rewind i)
       | Read_stdout -> Obj.magic (handler.read_stdout ())
       | Cur_goals -> Obj.magic (handler.current_goals ())
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index 9d58ae033..b94846405 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -17,7 +17,7 @@ type goals =
 type 'a call
 
 val raw_interp : string -> unit call
-val interp : bool -> string -> int call
+val interp : bool * string -> int call
 val rewind : int -> int call
 val is_in_loadpath : string -> bool call
 val make_cases : string -> string list list call
@@ -38,7 +38,7 @@ type 'a value =
 type handler = {
   is_in_loadpath : string -> bool;
   raw_interp : string -> unit;
-  interp : bool -> string -> int;
+  interp : bool * string -> int;
   rewind : int -> int;
   read_stdout : unit -> string;
   current_goals : unit -> goals;
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 2c0724790..b6a7906e2 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -14,6 +14,15 @@ open Pp
 open Printer
 open Namegen
 
+(** Signal handling: we postpone ^C during input and output phases,
+    but make it directly raise a Sys.Break during evaluation of the request. *)
+
+let catch_break = ref false
+
+let init_signal_handler () =
+  let f _ = if !catch_break then raise Sys.Break else Util.interrupt := true in
+  Sys.set_signal Sys.sigint (Sys.Signal_handle f)
+
 let prerr_endline _ = ()
 
 let coqide_known_option table = List.mem table [
@@ -247,7 +256,7 @@ let raw_interp s =
 let user_error_loc l s =
     raise (Loc.Exc_located (l, Util.UserError ("CoqIde", s)))
 
-let interp verbosely s =
+let interp (verbosely,s) =
   prerr_endline "Starting interp...";
   prerr_endline s;
   let pa = parsable_of_string s in
@@ -511,35 +520,35 @@ let explain_exn e =
   toploc,(Cerrors.explain_exn exc)
 
 let eval_call c =
-  let rec handle_exn = function
-    | Vernac.DuringCommandInterp (loc,inner) -> handle_exn inner
-    | Vernacexpr.Drop -> None, "Drop is not allowed by coqide!"
-    | Vernacexpr.Quit -> None, "Quit is not allowed by coqide!"
-    | e ->
-      let (l,pp) = explain_exn e in
-      l, string_of_ppcmds pp
+  let rec handle_exn e =
+    catch_break := false;
+    match e with
+      | Vernac.DuringCommandInterp (loc,inner) -> handle_exn inner
+      | Vernacexpr.Drop -> None, "Drop is not allowed by coqide!"
+      | Vernacexpr.Quit -> None, "Quit is not allowed by coqide!"
+      | e ->
+	let (l,pp) = explain_exn e in
+	l, string_of_ppcmds pp
+  in
+  let interruptible f x =
+    catch_break := true;
+    Util.check_for_interrupt ();
+    let r = f x in
+    catch_break := false;
+    r
   in
   let handler = {
-    Ide_intf.is_in_loadpath = is_in_loadpath;
-    Ide_intf.raw_interp = raw_interp;
-    Ide_intf.interp = interp;
-    Ide_intf.rewind = rewind;
-    Ide_intf.read_stdout = read_stdout;
-    Ide_intf.current_goals = current_goals;
-    Ide_intf.current_status = current_status;
-    Ide_intf.make_cases = make_cases }
+    Ide_intf.is_in_loadpath = interruptible is_in_loadpath;
+    Ide_intf.raw_interp = interruptible raw_interp;
+    Ide_intf.interp = interruptible interp;
+    Ide_intf.rewind = interruptible rewind;
+    Ide_intf.read_stdout = interruptible read_stdout;
+    Ide_intf.current_goals = interruptible current_goals;
+    Ide_intf.current_status = interruptible current_status;
+    Ide_intf.make_cases = interruptible make_cases }
   in
   Ide_intf.abstract_eval_call handler handle_exn c
 
-(** Signal handling: we ignore ^C during input and output phases,
-    but make it raise a Sys.Break during evaluation of the phrase.
-    TODO: how could we avoid dying if a ^C is received during a handle_exn ?
-*)
-
-let catch_break = function
-  | true -> Sys.catch_break true
-  | false -> Sys.set_signal Sys.sigint Sys.Signal_ignore
-
 (** Exceptions during eval_call should be converted into Ide_intf.Fail
     messages by explain_exn above. Otherwise, we die badly, after having
     tried to send a last message to the ide: trying to recover from errors
@@ -548,12 +557,12 @@ let catch_break = function
     a different request could hang the ide... *)
 
 let loop () =
-  catch_break false;
-  try while true do
+  init_signal_handler ();
+  catch_break := false;
+  try
+    while true do
       let q = (Marshal.from_channel: in_channel -> 'a Ide_intf.call) stdin in
-      catch_break true;
       let r = eval_call q in
-      catch_break false;
       Marshal.to_channel !orig_stdout r []; flush !orig_stdout
     done
   with e ->