aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--ide/coqide.ml82
-rw-r--r--ide/coqide.mli6
-rw-r--r--ide/coqide_main.ml417
3 files changed, 50 insertions, 55 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 9f2ea73b4..b070f5df9 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -144,46 +144,6 @@ let update_notebook_pos () =
in
session_notebook#set_tab_pos pos
-(** * Coqide's handling of signals *)
-
-(** We ignore Ctrl-C, and for most of the other catchable signals
- we launch an emergency save of opened files and then exit *)
-
-let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup;
- Sys.sigill; Sys.sigpipe; Sys.sigquit;
- (* Sys.sigsegv; Sys.sigterm;*) Sys.sigusr2]
-
-let crash_save i =
- (* ignore (Unix.sigprocmask Unix.SIG_BLOCK signals_to_crash);*)
- Minilib.log "Trying to save all buffers in .crashcoqide files";
- let count = ref 0 in
- List.iter
- (function {script=view; analyzed_view = av } ->
- (let filename = match av#filename with
- | None ->
- incr count;
- "Unnamed_coqscript_"^(string_of_int !count)^".crashcoqide"
- | Some f -> f^".crashcoqide"
- in
- try
- if try_export filename (view#buffer#get_text ()) then
- Minilib.log ("Saved "^filename)
- else Minilib.log ("Could not save "^filename)
- with _ -> Minilib.log ("Could not save "^filename))
- )
- session_notebook#pages;
- Minilib.log "Done. Please report.";
- if i <> 127 then exit i
-
-let ignore_break () =
- List.iter
- (fun i ->
- try Sys.set_signal i (Sys.Signal_handle crash_save)
- with _ -> Minilib.log "Signal ignored (normal if Win32)")
- signals_to_crash;
- Sys.set_signal Sys.sigint Sys.Signal_ignore
-
-
exception Unsuccessful
let force_reset_initial () =
@@ -1217,6 +1177,27 @@ let check_quit saveall =
| `NO | `DELETE_EVENT -> ()
end
+let crash_save exitcode =
+ Minilib.log "Starting emergency save of buffers in .crashcoqide files";
+ let idx =
+ let r = ref 0 in
+ fun () -> incr r; string_of_int !r
+ in
+ let save_page p =
+ let filename = match p.analyzed_view#filename with
+ | None -> "Unnamed_coqscript_" ^ idx () ^ ".crashcoqide"
+ | Some f -> f^".crashcoqide"
+ in
+ try
+ if try_export filename (p.script#buffer#get_text ()) then
+ Minilib.log ("Saved "^filename)
+ else Minilib.log ("Could not save "^filename)
+ with _ -> Minilib.log ("Could not save "^filename)
+ in
+ List.iter save_page session_notebook#pages;
+ Minilib.log "End emergency save";
+ exit exitcode
+
end
(** Callbacks for the File menu *)
@@ -1359,12 +1340,13 @@ let reset_autosave_timer () =
if prefs.auto_save then
autosave_timer.run ~ms:prefs.auto_save_delay ~callback:autosave_all
-(** For MacOSX : *)
+(** Export of functions used in [coqide_main] : *)
let forbid_quit_to_save () =
try FileAux.check_quit File.saveall; false
with FileAux.DontQuit -> true
+let crash_save = FileAux.crash_save
let do_load f = FileAux.load_file f
(** Callbacks for external commands *)
@@ -2180,3 +2162,21 @@ let read_coqide_args argv =
Ideutils.custom_coqtop := coqtop;
custom_project_files := project_files;
argv
+
+(** * Coqide's handling of signals *)
+
+(** The Ctrl-C (sigint) is handled as a interactive quit.
+ For most of the other catchable signals we launch
+ an emergency save of opened files and then exit. *)
+
+let signals_to_crash =
+ [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup;
+ Sys.sigill; Sys.sigpipe; Sys.sigquit; Sys.sigusr1; Sys.sigusr2]
+
+let set_signal_handlers () =
+ try
+ Sys.set_signal Sys.sigint (Sys.Signal_handle File.quit);
+ List.iter
+ (fun i -> Sys.set_signal i (Sys.Signal_handle FileAux.crash_save))
+ signals_to_crash
+ with _ -> Minilib.log "Signal ignored (normal if Win32)"
diff --git a/ide/coqide.mli b/ide/coqide.mli
index 18df1f6a0..aba75be4b 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -26,9 +26,9 @@ val forbid_quit_to_save : unit -> bool
(** Function to load of a file. *)
val do_load : string -> unit
-(** Set coqide to ignore Ctrl-C, while launching [crash_save] and
- exiting for others received signals *)
-val ignore_break : unit -> unit
+(** Set coqide to perform a clean quit at Ctrl-C, while launching
+ [crash_save] and exiting for others received signals *)
+val set_signal_handlers : unit -> unit
(** Emergency saving of opened files as "foo.v.crashcoqide",
and exit (if the integer isn't 127). *)
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 5fa3eccd2..3d14805eb 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -52,7 +52,7 @@ let () =
END
let () =
- Coqide.ignore_break ();
+ Coqide.set_signal_handlers ();
ignore (GtkMain.Main.init ())
IFDEF QUARTZ THEN
@@ -100,13 +100,8 @@ IFDEF QUARTZ THEN
osx#ready ()
END
- while true do
- try
- GtkThread.main ()
- with
- | Sys.Break -> Minilib.log "Interrupted."
- | e ->
- Minilib.log
- ("CoqIde unexpected error:" ^ (Printexc.to_string e));
- Coqide.crash_save 127
- done
+let () =
+ try GtkThread.main ()
+ with e ->
+ Minilib.log ("CoqIde unexpected error:" ^ Printexc.to_string e);
+ Coqide.crash_save 127