From 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Tue, 19 Apr 2011 16:44:20 +0200 Subject: Imported Upstream version 8.3.pl2 --- ide/coq.ml | 10 +++------- ide/coq_icon.rc | 1 + ide/coqide.ml | 20 ++++++++++---------- ide/ideutils.ml | 10 +++++++--- ide/ideutils.mli | 3 ++- ide/utils/configwin_messages.ml | 4 +--- 6 files changed, 24 insertions(+), 24 deletions(-) create mode 100644 ide/coq_icon.rc (limited to 'ide') diff --git a/ide/coq.ml b/ide/coq.ml index 4996661a..bb08e2af 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq.ml 13431 2010-09-18 08:15:29Z herbelin $ *) +(* $Id: coq.ml 13751 2010-12-24 09:56:05Z letouzey $ *) open Vernac open Vernacexpr @@ -27,10 +27,6 @@ open Termops open Namegen open Ideutils -let prerr_endline s = if !debug then prerr_endline s else () - -let output = ref (Format.formatter_of_out_channel stdout) - let msg m = let b = Buffer.create 103 in Pp.msg_with (Format.formatter_of_buffer b) m; @@ -394,7 +390,7 @@ let compute_reset_info loc_ast = } let reset_initial () = - prerr_endline "Reset initial called"; flush stderr; + prerr_endline "Reset initial called"; Vernacentries.abort_refine Lib.reset_initial () let reset_to sp = @@ -412,7 +408,7 @@ let interp_with_options verbosely options s = let pe = Pcoq.Gram.Entry.parse Pcoq.main_entry pa in (* Temporary hack to make coqide.byte work (WTF???) - now with less screen * pollution *) - Pervasives.prerr_string " \r"; Pervasives.flush stderr; + (try Pervasives.prerr_string " \r"; Pervasives.flush stderr with _ -> ()); match pe with | None -> assert false | Some((loc,vernac) as last) -> diff --git a/ide/coq_icon.rc b/ide/coq_icon.rc new file mode 100644 index 00000000..f873e7de --- /dev/null +++ b/ide/coq_icon.rc @@ -0,0 +1 @@ +large ICON ide/coq.ico diff --git a/ide/coqide.ml b/ide/coqide.ml index fdf33c39..ce4f0666 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqide.ml 13708 2010-12-13 14:49:29Z gmelquio $ *) +(* $Id: coqide.ml 13751 2010-12-24 09:56:05Z letouzey $ *) open Preferences open Vernacexpr @@ -200,7 +200,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 } -> @@ -212,12 +212,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 () = @@ -3202,7 +3202,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); "\nCoq is developed by the Coq Development Team\ \n(INRIA - CNRS - University Paris 11 and partners)\ \nWeb site: " ^ Coq_config.wwwcoq ^ - "\nFeature wish or bug report: http://logical.saclay.inria.fr/coq-bugs\ + "\nFeature wish or bug report: http://coq.inria.fr/bugs\ \n\ \nCredits for CoqIDE, the Integrated Development Environment for Coq:\ \n\ @@ -3332,10 +3332,10 @@ let start () = try GtkThread.main () with - | Sys.Break -> prerr_endline "Interrupted." ; flush stderr + | Sys.Break -> prerr_endline "Interrupted." | e -> - Pervasives.prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e)); - flush stderr; + safe_prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e)); + flush_all (); crash_save 127 done diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 138bf5f6..8b7840e3 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ideutils.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: ideutils.ml 13751 2010-12-24 09:56:05Z letouzey $ *) open Preferences @@ -31,12 +31,16 @@ let set_location = ref (function s -> failwith "not ready") let pbar = GRange.progress_bar ~pulse_step:0.2 () +(* On a Win32 application with no console, writing to stderr raise + a Sys_error "bad file descriptor" *) +let safe_prerr_endline msg = try prerr_endline msg with _ -> () + let debug = Flags.debug let prerr_endline s = - if !debug then (prerr_endline s;flush stderr) + if !debug then try (prerr_endline s;flush stderr) with _ -> () let prerr_string s = - if !debug then (prerr_string s;flush stderr) + if !debug then try (prerr_string s;flush stderr) with _ -> () let lib_ide_file f = let coqlib = Envars.coqlib () in diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 9af4fb43..ade460c6 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ideutils.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: ideutils.mli 13751 2010-12-24 09:56:05Z letouzey $ i*) val async : ('a -> unit) -> 'a -> unit val sync : ('a -> 'b) -> 'a -> 'b @@ -34,6 +34,7 @@ val is_char_start : char -> bool val lib_ide_file : string -> string val my_stat : string -> Unix.stats option +val safe_prerr_endline : string -> unit val prerr_endline : string -> unit val prerr_string : string -> unit val print_id : 'a -> unit diff --git a/ide/utils/configwin_messages.ml b/ide/utils/configwin_messages.ml index f8984462..26f5b61b 100644 --- a/ide/utils/configwin_messages.ml +++ b/ide/utils/configwin_messages.ml @@ -30,9 +30,7 @@ let version = "1.2";; let html_config = "Configwin bindings configurator for html parameters" -let home = - try Sys.getenv "HOME" - with Not_found -> "" +let home = System.home let mCapture = "Capture";; let mType_key = "Type key" ;; -- cgit v1.2.3