aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/ideutils.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-21 16:12:31 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-21 16:12:31 +0000
commit08642139dc3edf2caf94e7f246c15644daca16ad (patch)
tree11c772236ad3fa7ad0e20607760fb66f8e829a8e /ide/ideutils.mli
parent64643bc2889ba26007cea65e3bf8917a8595d7ed (diff)
Win32: if we make coqide console-free, then stderr/stdout/sdtin shouldn't be used
This is an adaptation of commit r13751 of branch 8.3 Even if coqide.exe keeps its console by default for the moment, we try to allow turning it off (for instance via the mkwinapp tool) : for that we need to be cautious about the use of functions like prerr_endline. Since stderr doesn't exists in this settings, such functions trigger a Sys_error "bad file descriptor". This patch protects many access to std** by a (try ... with _ ->()). Nota: with camlp5 < 6.02.1, Print Grammar was also generating such a Sys_error. TODO: we should try to figure a way of displaying messages (both debug and early/late error message). A log file ? A popup ? diplay in the response buffer ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14040 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/ideutils.mli')
-rw-r--r--ide/ideutils.mli6
1 files changed, 5 insertions, 1 deletions
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