aboutsummaryrefslogtreecommitdiff
path: root/ide/ideutils.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/ideutils.ml')
-rw-r--r--ide/ideutils.ml6
1 files changed, 4 insertions, 2 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index f4fd73d6fd..a3fd090840 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -148,13 +148,15 @@ let set_highlight_timer f =
(* Get back the standard coq out channels *)
-let read_stdout,clear_stdout =
+let init_stdout,read_stdout,clear_stdout =
let out_buff = Buffer.create 100 in
let out_ft = Format.formatter_of_buffer out_buff in
+ (fun () ->
Pp_control.std_ft := out_ft;
- Pp_control.err_ft := out_ft;
+ Pp_control.err_ft := out_ft),
(fun () -> Format.pp_print_flush out_ft ();
let r = Buffer.contents out_buff in
+ prerr_endline "Output from Coq is: "; prerr_endline r;
Buffer.clear out_buff; r),
(fun () ->
Format.pp_print_flush out_ft (); Buffer.clear out_buff)