diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-21 16:12:47 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-21 16:12:47 +0000 |
commit | c9febd2450c40dbc46182662ccdc1567050d0222 (patch) | |
tree | 2ff96f95a3f58f15aed292c02a62ec28816c265b | |
parent | eacf0de87bf18631610f0fae9af192583f27a88b (diff) |
Coqide: try to avoid displaying error messages on coqide's console
In Win32, these messages may trigger some Sys_error if we try to
turn coqide into a true windows app (no console). To be continued...
The best way would be probably to re-route the whole stdout and stderr
to something else via dup2, but to what ? A log file ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14043 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | ide/coq.ml | 12 | ||||
-rw-r--r-- | ide/coqide.ml | 15 | ||||
-rw-r--r-- | ide/coqide_main.ml4 | 2 | ||||
-rw-r--r-- | ide/ideutils.ml | 6 | ||||
-rw-r--r-- | ide/preferences.ml | 12 |
5 files changed, 25 insertions, 22 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 1acea4a9b..d595fbc91 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -73,11 +73,11 @@ let check_connection args = | _ -> raise (Coqtop_output lines) with | End_of_file -> - Pervasives.prerr_endline "Cannot start connection with coqtop"; + safe_prerr_endline "Cannot start connection with coqtop"; exit 1 | Coqtop_output lines -> - Pervasives.prerr_endline "Connection with coqtop failed:"; - List.iter Pervasives.prerr_endline lines; + safe_prerr_endline "Connection with coqtop failed:"; + List.iter safe_prerr_endline lines; exit 1 (** It is tempting to merge the following function with the previous one, @@ -98,11 +98,11 @@ let check_coqlib args = | _ -> raise (Coqtop_output lines) with | End_of_file -> - Pervasives.prerr_endline "Cannot start connection with coqtop"; + safe_prerr_endline "Cannot start connection with coqtop"; exit 1 | Coqtop_output lines -> - Pervasives.prerr_endline "Connection with coqtop failed:"; - List.iter Pervasives.prerr_endline lines; + safe_prerr_endline "Connection with coqtop failed:"; + List.iter safe_prerr_endline lines; exit 1 diff --git a/ide/coqide.ml b/ide/coqide.ml index a0bd8a829..65409c2de 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1667,7 +1667,7 @@ let saveall_f () = ) session_notebook#pages let forbid_quit_to_save () = - save_pref(); + begin try save_pref() with e -> flash_info "Cannot save preferences" end; (if List.exists (function | {script=view} -> view#buffer#modified @@ -1718,7 +1718,11 @@ let forbid_quit_to_save () = let main files = (* Statup preferences *) - load_pref (); + begin + try load_pref () + with e -> + flash_info ("Could not load preferences ("^Printexc.to_string e^")."); + end; (* Main window *) let w = GWindow.window @@ -2255,7 +2259,12 @@ let main files = let _ = edit_f#add_item "_Preferences" - ~callback:(fun () -> configure ~apply:update_notebook_pos (); reset_revert_timer ()) + ~callback:(fun () -> + begin + try configure ~apply:update_notebook_pos () + with _ -> flash_info "Cannot save preferences" + end; + reset_revert_timer ()) in (* let save_prefs_m = diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index 7c0f23170..d5888ff93 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -58,7 +58,7 @@ let () = try GtkThread.main () with - | Sys.Break -> Ideutils.prerr_endline "Interrupted." ; flush stderr + | Sys.Break -> Ideutils.prerr_endline "Interrupted." | e -> Ideutils.safe_prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e)); diff --git a/ide/ideutils.ml b/ide/ideutils.ml index faaaa3742..1b2cd0f89 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -329,13 +329,11 @@ let url_for_keyword = let u = String.sub s (i + 1) (String.length s - i - 1) in Hashtbl.add ht k u with _ -> - Printf.eprintf "Warning: Cannot parse documentation index file.\n"; - flush stderr + safe_prerr_endline "Warning: Cannot parse documentation index file." done with End_of_file -> close_in cin with _ -> - Printf.eprintf "Warning: Cannot find documentation index file.\n"; - flush stderr + safe_prerr_endline "Warning: Cannot find documentation index file." end; Hashtbl.find ht : string -> string) diff --git a/ide/preferences.ml b/ide/preferences.ml index e31a5904a..97b1d00dd 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -168,7 +168,7 @@ let save_pref () = (try GtkData.AccelMap.save accel_file with _ -> ()); let p = !current in - try + let add = Minilib.Stringmap.add in let (++) x f = f x in Minilib.Stringmap.empty ++ @@ -219,12 +219,11 @@ let save_pref () = add "vertical_tabs" [string_of_bool p.vertical_tabs] ++ add "opposite_tabs" [string_of_bool p.opposite_tabs] ++ Config_lexer.print_file pref_file - with _ -> prerr_endline "Could not save preferences." let load_pref () = (try GtkData.AccelMap.load accel_file with _ -> ()); let p = !current in - try + let m = Config_lexer.load_file pref_file in let np = { p with cmd_coqc = p.cmd_coqc } in let set k f = try let v = Minilib.Stringmap.find k m in f v with _ -> () in @@ -271,7 +270,7 @@ let load_pref () = v <> Coq_config.wwwcoq ^ "doc" && v <> Coq_config.wwwcoq ^ "doc/" then - prerr_endline ("Warning: Non-standard URL for Coq documentation in preference file: "^v); + (*prerr_endline ("Warning: Non-standard URL for Coq documentation in preference file: "^v);*) np.doc_url <- v); set_hd "library_url" (fun v -> np.library_url <- v); set_bool "show_toolbar" (fun v -> np.show_toolbar <- v); @@ -286,13 +285,10 @@ let load_pref () = set_bool "lax_syntax" (fun v -> np.lax_syntax <- v); set_bool "vertical_tabs" (fun v -> np.vertical_tabs <- v); set_bool "opposite_tabs" (fun v -> np.opposite_tabs <- v); - current := np; + current := np (* Format.printf "in load_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) - with e -> - prerr_endline ("Could not load preferences ("^ - (Printexc.to_string e)^").") let configure ?(apply=(fun () -> ())) () = let cmd_coqc = |