Imported Upstream version 8.3.pl2upstream/8.3.pl2

6 files changed, 24 insertions, 24 deletions

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" ;;