diff options
| -rw-r--r-- | ide/coq.ml | 3 | ||||
| -rw-r--r-- | ide/coqide.ml | 17 | ||||
| -rw-r--r-- | ide/coqide_main.ml4 | 14 | ||||
| -rw-r--r-- | ide/ideutils.ml | 13 | ||||
| -rw-r--r-- | ide/ideutils.mli | 6 |
5 files changed, 34 insertions, 19 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 3c7ee2de8..1acea4a9b 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -8,9 +8,6 @@ open Ideutils -let prerr_endline s = if !debug then prerr_endline s else () - - (** * Version and date *) let get_version_date () = diff --git a/ide/coqide.ml b/ide/coqide.ml index 726931cac..08c41aeaa 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -190,7 +190,7 @@ let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup; let crash_save i = (* ignore (Unix.sigprocmask Unix.SIG_BLOCK signals_to_crash);*) - Pervasives.prerr_endline "Trying to save all buffers in .crashcoqide files"; + safe_prerr_endline "Trying to save all buffers in .crashcoqide files"; let count = ref 0 in List.iter (function {script=view; analyzed_view = av } -> @@ -202,12 +202,12 @@ let crash_save i = in try if try_export filename (view#buffer#get_text ()) then - Pervasives.prerr_endline ("Saved "^filename) - else Pervasives.prerr_endline ("Could not save "^filename) - with _ -> Pervasives.prerr_endline ("Could not save "^filename)) + safe_prerr_endline ("Saved "^filename) + else safe_prerr_endline ("Could not save "^filename) + with _ -> safe_prerr_endline ("Could not save "^filename)) ) session_notebook#pages; - Pervasives.prerr_endline "Done. Please report."; + safe_prerr_endline "Done. Please report."; if i <> 127 then exit i let ignore_break () = @@ -3188,11 +3188,10 @@ let process_argv argv = try let continue,filtered = Coq.filter_coq_opts (List.tl argv) in if not continue then - (List.iter Pervasives.prerr_endline filtered; exit 0); + (List.iter safe_prerr_endline filtered; exit 0); let opts = List.filter (fun arg -> String.get arg 0 == '-') filtered in if opts <> [] then - (output_string stderr ("Illegal option: "^List.hd opts^"\n"); - exit 1); + (safe_prerr_endline ("Illegal option: "^List.hd opts); exit 1); filtered with _ -> - (output_string stderr "coqtop choked on one of your option"; exit 1) + (safe_prerr_endline "coqtop choked on one of your option"; exit 1) diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index c63db0031..9fc0f72b7 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -1,3 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + IFDEF MacInt THEN external gtk_mac_init : (string -> unit) -> (unit -> bool) -> unit = "caml_gtk_mac_init" @@ -41,9 +49,9 @@ let () = try GtkThread.main () with - | Sys.Break -> prerr_endline "Interrupted." ; flush stderr + | Sys.Break -> Ideutils.prerr_endline "Interrupted." ; flush stderr | e -> - Pervasives.prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e)); - flush stderr; + Ideutils.safe_prerr_endline + ("CoqIde unexpected error:" ^ (Printexc.to_string e)); Coqide.crash_save 127 done diff --git a/ide/ideutils.ml b/ide/ideutils.ml index a4126ae33..faaaa3742 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -31,10 +31,17 @@ let pbar = GRange.progress_bar ~pulse_step:0.2 () let debug = Flags.debug +(* On a Win32 application with no console, writing to stderr raise + a Sys_error "bad file descriptor", hence the "try" below. + Ideally, we should re-route message to a log file somewhere, or + print in the response buffer. +*) + +let safe_prerr_endline s = + try prerr_endline s;flush stderr with _ -> () + let prerr_endline s = - if !debug then (prerr_endline s;flush stderr) -let prerr_string s = - if !debug then (prerr_string s;flush stderr) + if !debug then try prerr_endline s;flush stderr with _ -> () let lib_ide_file f = Filename.concat (Filename.concat !Minilib.coqlib "ide") f diff --git a/ide/ideutils.mli b/ide/ideutils.mli index f15cd120c..fe8936877 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -30,8 +30,12 @@ val is_char_start : char -> bool val lib_ide_file : string -> string val my_stat : string -> Unix.stats option +(** safe version of Pervasives.prerr_endline + (avoid exception in win32 without console) *) +val safe_prerr_endline : string -> unit +(** debug printing *) val prerr_endline : string -> unit -val prerr_string : string -> unit + val print_id : 'a -> unit val revert_timer : GMain.Timeout.id option ref |