diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-03 19:06:22 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-03 19:06:22 +0000 |
| commit | 321969d18e24a6c636137efd0a59a254603fce94 (patch) | |
| tree | b4994d54360cabe6f6245ce9c2d114fb1f00b93e | |
| parent | 0d87d99747d1ad6b8a69672b08a2bb5b2174adc6 (diff) | |
Redirect stdout to stderr in -ideslave
This fixes "Print Grammar" in coqide, which uses a camlp5 function
that prints to stdout, interfering with the ide-slave
communication. Camlp5 should additionnally provide a way to print to a
formatter instead of directly using stdout...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13670 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/ide_blob.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml index 3bd9462ce..c4036af9f 100644 --- a/toplevel/ide_blob.ml +++ b/toplevel/ide_blob.ml @@ -481,12 +481,17 @@ let current_status () = path ^ ", proving " ^ (Names.string_of_id (Pfedit.get_current_proof_name ())) with _ -> path +let orig_stdout = ref stdout + let init_stdout,read_stdout = let out_buff = Buffer.create 100 in let out_ft = Format.formatter_of_buffer out_buff in let deep_out_ft = Format.formatter_of_buffer out_buff in let _ = Pp_control.set_gp deep_out_ft Pp_control.deep_gp in (fun () -> + flush_all (); + orig_stdout := Unix.out_channel_of_descr (Unix.dup Unix.stdout); + Unix.dup2 Unix.stderr Unix.stdout; Pp_control.std_ft := out_ft; Pp_control.err_ft := out_ft; Pp_control.deep_ft := deep_out_ft; @@ -578,7 +583,7 @@ let loop () = while true do let q = (Safe_marshal.receive: in_channel -> 'a call) stdin in let r = eval_call q in - Safe_marshal.send stdout r + Safe_marshal.send !orig_stdout r done with | Vernacexpr.Quit -> exit 0 |