diff options
author | 2011-03-30 07:18:55 +0000 | |
---|---|---|
committer | 2011-03-30 07:18:55 +0000 | |
commit | a4355384effa75c4789e6ae0afb942206e985140 (patch) | |
tree | df6561cec1f825aa22fa150dd742947a318688f3 /toplevel | |
parent | bbe52c9e9f9e6929484d8041a5fbb0c56a6a3735 (diff) |
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
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/ide_intf.ml | 6 | ||||
-rw-r--r-- | toplevel/ide_intf.mli | 4 | ||||
-rw-r--r-- | toplevel/ide_slave.ml | 67 |
3 files changed, 43 insertions, 34 deletions
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 -> |