Ide_intf: slight reorganisation of the IDE api

 - merge raw_interp with interp (with one more flag)
 - merge read_stdout with interp, which now return a string
 - shorter command names

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14454 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 171 insertions, 170 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 739435df4..0d0894213 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -102,15 +102,11 @@ object(self)
       in
       try
         result#buffer#set_text
-          (match Coq.raw_interp coqtop phrase with
+          (match Coq.interp coqtop ~raw:true phrase with
              | Ide_intf.Fail (l,str) ->
                  ("Error while interpreting "^phrase^":\n"^str)
-             | Ide_intf.Good () ->
-                 match Coq.read_stdout coqtop with
-                   | Ide_intf.Fail (l,str) ->
-                       ("Error while fetching "^phrase^"results:\n"^str)
-                   | Ide_intf.Good results ->
-                       ("Result for command " ^ phrase ^ ":\n" ^ results))
+             | Ide_intf.Good results ->
+                 ("Result for command " ^ phrase ^ ":\n" ^ results))
       with e ->
 	let s = Printexc.to_string e in
 	assert (Glib.Utf8.validate s);
diff --git a/ide/coq.ml b/ide/coq.ml
index dbb0d8ac3..a5b2d38ab 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -199,13 +199,12 @@ let eval_call coqtop (c:'a Ide_intf.call) =
   flush coqtop.cin;
   (Marshal.from_channel: in_channel -> 'a Ide_intf.value) coqtop.cout
 
-let interp coqtop b s = eval_call coqtop (Ide_intf.interp (b,s))
-let raw_interp coqtop s = eval_call coqtop (Ide_intf.raw_interp s)
-let read_stdout coqtop = eval_call coqtop Ide_intf.read_stdout
+let interp coqtop ?(raw=false) ?(verbose=true) s =
+  eval_call coqtop (Ide_intf.interp (raw,verbose,s))
 let rewind coqtop i = eval_call coqtop (Ide_intf.rewind i)
-let is_in_loadpath coqtop s = eval_call coqtop (Ide_intf.is_in_loadpath s)
-let make_cases coqtop s = eval_call coqtop (Ide_intf.make_cases s)
-let current_status coqtop = eval_call coqtop Ide_intf.current_status
+let inloadpath coqtop s = eval_call coqtop (Ide_intf.inloadpath s)
+let mkcases coqtop s = eval_call coqtop (Ide_intf.mkcases s)
+let status coqtop = eval_call coqtop Ide_intf.status
 
 module PrintOpt =
 struct
@@ -227,8 +226,8 @@ struct
     List.fold_left
       (fun acc cmd -> 
          let str = (if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "." in
-         match raw_interp coqtop str with
-           | Ide_intf.Good () -> acc
+         match interp coqtop ~raw:true ~verbose:false str with
+           | Ide_intf.Good _ -> acc
            | Ide_intf.Fail (l,errstr) ->  Ide_intf.Fail (l,"Could not eval \""^str^"\": "^errstr)
       )
       (Ide_intf.Good ())
@@ -242,8 +241,8 @@ struct
     state_hack (Ide_intf.Good ())
 end
 
-let current_goals coqtop =
+let goals coqtop =
   match PrintOpt.enforce_hack coqtop with
-    | Ide_intf.Good () -> eval_call coqtop Ide_intf.current_goals
+    | Ide_intf.Good () -> eval_call coqtop Ide_intf.goals
     | Ide_intf.Fail str -> Ide_intf.Fail str
 
diff --git a/ide/coq.mli b/ide/coq.mli
index 04155ac40..685bfcac3 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -45,14 +45,13 @@ val interrupter : (int -> unit) ref
 
 (** * Calls to Coqtop, cf [Ide_intf] for more details *)
 
-val interp : coqtop -> bool -> string -> unit Ide_intf.value
-val raw_interp : coqtop -> string -> unit Ide_intf.value
-val read_stdout : coqtop -> string Ide_intf.value
+val interp :
+  coqtop -> ?raw:bool -> ?verbose:bool -> string -> string Ide_intf.value
 val rewind : coqtop -> int -> unit Ide_intf.value
-val is_in_loadpath : coqtop -> string -> bool Ide_intf.value
-val make_cases : coqtop -> string -> string list list Ide_intf.value
-val current_status : coqtop -> string Ide_intf.value
-val current_goals : coqtop -> Ide_intf.goals Ide_intf.value
+val status : coqtop -> string Ide_intf.value
+val goals : coqtop -> Ide_intf.goals Ide_intf.value
+val inloadpath : coqtop -> string -> bool Ide_intf.value
+val mkcases : coqtop -> string -> string list list Ide_intf.value
 
 (** A specialized version of [raw_interp] dedicated to
     set/unset options. *)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 0f5321486..7a714b1d0 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -829,7 +829,7 @@ object(self)
         else
           (fun _ _ -> ()) in
       try
-        match Coq.current_goals !mycoqtop with
+        match Coq.goals !mycoqtop with
           | Ide_intf.Fail (l,str) ->
             self#set_message ("Error in coqtop :\n"^str)
           | Ide_intf.Good goals ->
@@ -842,7 +842,7 @@ object(self)
 
   method show_goals = self#show_goals_full
 
-  method private send_to_coq ct verbosely phrase show_output show_error localize =
+  method private send_to_coq ct verbose phrase show_output show_error localize =
     let display_output msg =
       self#insert_message (if show_output then msg else "") in
     let display_error (loc,s) =
@@ -873,16 +873,11 @@ object(self)
       prerr_endline "Send_to_coq starting now";
       (* It's important here to work with [ct] and not [!mycoqtop], otherwise
          we could miss a restart of coqtop and continue sending it orders. *)
-      match Coq.interp ct verbosely phrase with
+      match Coq.interp ct ~verbose phrase with
         | Ide_intf.Fail (l,str) -> sync display_error (l,str); None
-        | Ide_intf.Good () ->
-	  match Coq.read_stdout ct with
-            | Ide_intf.Fail (l,str) -> sync display_error (l,str); None
-            | Ide_intf.Good msg ->
-              sync display_output msg;
-	      (** TODO: Restore someday the access to Decl_mode.get_damon_flag,
-		  and also detect the use of admit, and then return Unsafe *)
-              Some Safe
+        | Ide_intf.Good msg -> sync display_output msg; Some Safe
+          (* TODO: Restore someday the access to Decl_mode.get_damon_flag,
+	     and also detect the use of admit, and then return Unsafe *)
     with
       | End_of_file -> (* Coqtop has died, let's trigger a reset_initial. *)
         raise RestartCoqtop
@@ -1253,24 +1248,22 @@ object(self)
       (input_view#event#connect#key_press ~callback:self#active_keypress_handler);
     prerr_endline "CONNECTED active : ";
     print_id (match act_id with Some x -> x | None -> assert false);
-    match
-      filename
-    with
+    match filename with
       | None -> ()
       | Some f ->
 	let dir = Filename.dirname f in
 	let ct = !mycoqtop in
-	match Coq.is_in_loadpath ct dir with
+	match Coq.inloadpath ct dir with
 	  | Ide_intf.Fail (_,str) ->
 	    self#set_message
 	      ("Could not determine lodpath, this might lead to problems:\n"^str)
 	  | Ide_intf.Good true -> ()
 	  | Ide_intf.Good false ->
 	    let cmd = Printf.sprintf "Add LoadPath \"%s\". "  dir in
-	    match Coq.interp ct false cmd with
+	    match Coq.interp ct cmd with
 	      | Ide_intf.Fail (l,str) ->
 		self#set_message ("Couln't add loadpath:\n"^str)
-	      | Ide_intf.Good () -> ()
+	      | Ide_intf.Good _ -> ()
   end
 
   method private electric_paren tag =
@@ -2180,7 +2173,7 @@ let main files =
         ignore (f av);
         pop_info ();
         push_info
-          (match Coq.current_status !(current.toplvl) with
+          (match Coq.status !(current.toplvl) with
             | Ide_intf.Fail (l,str) ->
 	      "Oops, problem while fetching coq status."
             | Ide_intf.Good str -> str)
@@ -2195,7 +2188,7 @@ let main files =
     let w = get_current_word () in
     let cur_ct = !(session_notebook#current_term.toplvl) in
     try
-      match Coq.make_cases cur_ct w with
+      match Coq.mkcases cur_ct w with
         | Ide_intf.Fail _ -> raise Not_found
         | Ide_intf.Good cases ->
           let print_branch c l =
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index 7f3e59324..5374b06df 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -16,24 +16,23 @@ type goals =
 
 (** We use phantom types and GADT to protect ourselves against wild casts *)
 
+type raw = bool
+type verbose = bool
+
 type 'a call =
-  | In_loadpath of string
-  | Raw_interp of string
-  | Interp of bool * string
+  | Interp of raw * verbose * string
   | Rewind of int
-  | Read_stdout
-  | Cur_goals
-  | Cur_status
-  | Cases of string
-
-let interp (b,s) : unit call = Interp (b,s)
-let raw_interp s : unit call = Raw_interp s
-let read_stdout : string call = Read_stdout
+  | Goals
+  | Status
+  | InLoadPath of string
+  | MkCases of string
+
+let interp (r,b,s) : string call = Interp (r,b,s)
 let rewind i : unit call = Rewind i
-let is_in_loadpath s : bool call = In_loadpath s
-let current_goals : goals call = Cur_goals
-let current_status : string call = Cur_status
-let make_cases s : string list list call = Cases s
+let goals : goals call = Goals
+let status : string call = Status
+let inloadpath s : bool call = InLoadPath s
+let mkcases s : string list list call = MkCases s
 
 (** * Coq answers to CoqIde *)
 
@@ -44,27 +43,23 @@ type 'a value =
   | Fail of (location * string)
 
 type handler = {
-  interp : bool * string -> unit;
-  raw_interp : string -> unit;
-  read_stdout : unit -> string;
+  interp : raw * verbose * string -> string;
   rewind : int -> unit;
-  is_in_loadpath : string -> bool;
-  current_goals : unit -> goals;
-  current_status : unit -> string;
-  make_cases : string -> string list list;
+  goals : unit -> goals;
+  status : unit -> string;
+  inloadpath : string -> bool;
+  mkcases : string -> string list list;
 }
 
 let abstract_eval_call handler explain_exn c =
   try
     let res = match c with
-      | In_loadpath s -> Obj.magic (handler.is_in_loadpath s)
-      | Raw_interp s -> Obj.magic (handler.raw_interp s)
-      | Interp (b,s) -> Obj.magic (handler.interp (b,s))
+      | Interp (r,b,s) -> Obj.magic (handler.interp (r,b,s))
       | Rewind i -> Obj.magic (handler.rewind i)
-      | Read_stdout -> Obj.magic (handler.read_stdout ())
-      | Cur_goals -> Obj.magic (handler.current_goals ())
-      | Cur_status -> Obj.magic (handler.current_status ())
-      | Cases s -> Obj.magic (handler.make_cases s)
+      | Goals -> Obj.magic (handler.goals ())
+      | Status -> Obj.magic (handler.status ())
+      | InLoadPath s -> Obj.magic (handler.inloadpath s)
+      | MkCases s -> Obj.magic (handler.mkcases s)
     in Good res
   with e ->
     let (l,str) = explain_exn e in
@@ -73,15 +68,30 @@ let abstract_eval_call handler explain_exn c =
 (** * Debug printing *)
 
 let pr_call = function
-  | In_loadpath s -> "In_loadpath["^s^"]"
-  | Raw_interp s -> "Raw_interp["^s^"]"
-  | Interp (b,s) -> "Interp["^(if b then "true" else "false")^","^s^"]"
-  | Rewind i -> "Rewind["^(string_of_int i)^"]"
-  | Read_stdout -> "Read_stdout"
-  | Cur_goals -> "Cur_goals"
-  | Cur_status -> "Cur_status"
-  | Cases s -> "Cases["^s^"]"
-
-let pr_value = function
-  | Good _ -> "Good"
-  | Fail (_,str) -> "Fail["^str^"]"
+  | Interp (r,b,s) ->
+    let raw = if r then "RAW" else "" in
+    let verb = if b then "" else "SILENT" in
+    "INTERP"^raw^verb^" ["^s^"]"
+  | Rewind i -> "REWIND "^(string_of_int i)
+  | Goals -> "GOALS"
+  | Status -> "STATUS"
+  | InLoadPath s -> "INLOADPATH "^s
+  | MkCases s -> "MKCASES "^s
+
+let pr_value_gen pr = function
+  | Good v -> "GOOD " ^ pr v
+  | Fail (_,str) -> "FAIL ["^str^"]"
+
+let pr_value v = pr_value_gen (fun _ -> "") v
+
+let pr_string s = "["^s^"]"
+let pr_bool b = if b then "true" else "false"
+
+let pr_full_value call value =
+  match call with
+    | Interp _ -> pr_value_gen pr_string (Obj.magic value)
+    | Rewind i -> pr_value value
+    | Goals -> pr_value value (* TODO *)
+    | Status -> pr_value_gen pr_string (Obj.magic value)
+    | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value)
+    | MkCases s -> pr_value value (* TODO *)
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index bd92460f2..211b34e13 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -16,34 +16,36 @@ type goals =
 
 type 'a call
 
-(** Running a command. The boolean is a verbosity flag.
-    Output will be fetch later via [read_stdout]. *)
-val interp : bool * string -> unit call
-
-(** Running a command with no impact on the undo stack,
-    such as a query or a Set/Unset.
-    Output will be fetch later via [read_stdout]. *)
-val raw_interp : string -> unit call
-
-(** What messages have been displayed by coqtop recently ? *)
-val read_stdout : string call
+type raw = bool
+type verbose = bool
+
+(** Running a command (given as a string).
+    - The 1st flag indicates whether to use "raw" mode
+      (less sanity checks, no impact on the undo stack).
+      Suitable e.g. for queries, or for the Set/Unset
+      of display options that coqide performs all the time.
+    - The 2nd flag controls the verbosity.
+    - The returned string contains the messages produced
+      by this command, but not the updated goals (they are
+      to be fetch by a separated [current_goals]). *)
+val interp : raw * verbose * string -> string call
 
 (** Backtracking by a certain number of phrases. *)
 val rewind : int -> unit call
 
-(** Is a file present somewhere in Coq's loadpath ? *)
-val is_in_loadpath : string -> bool call
+(** Fetching the list of current goals *)
+val goals : goals call
+
+(** The status, for instance "Ready in SomeSection, proving Foo" *)
+val status : string call
+
+(** Is a directory part of Coq's loadpath ? *)
+val inloadpath : string -> bool call
 
 (** Create a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
     followed by enough pattern variables. *)
-val make_cases : string -> string list list call
-
-(** The status, for instance "Ready in SomeSection, proving Foo" *)
-val current_status : string call
-
-(** Fetching the list of current goals *)
-val current_goals : goals call
+val mkcases : string -> string list list call
 
 
 (** * Coq answers to CoqIde *)
@@ -54,15 +56,15 @@ type 'a value =
   | Good of 'a
   | Fail of (location * string)
 
+(** * The structure that coqtop should implement *)
+
 type handler = {
-  interp : bool * string -> unit;
-  raw_interp : string -> unit;
-  read_stdout : unit -> string;
+  interp : raw * verbose * string -> string;
   rewind : int -> unit;
-  is_in_loadpath : string -> bool;
-  current_goals : unit -> goals;
-  current_status : unit -> string;
-  make_cases : string -> string list list;
+  goals : unit -> goals;
+  status : unit -> string;
+  inloadpath : string -> bool;
+  mkcases : string -> string list list;
 }
 
 val abstract_eval_call :
@@ -73,3 +75,4 @@ val abstract_eval_call :
 
 val pr_call : 'a call -> string
 val pr_value : 'a value -> string
+val pr_full_value : 'a call -> 'a value -> string
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index c7667f030..616cd5b09 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -25,6 +25,27 @@ let init_signal_handler () =
 
 let prerr_endline _ = ()
 
+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;
+     set_binary_mode_out !orig_stdout true;
+     set_binary_mode_in stdin true;
+  ),
+  (fun () -> Format.pp_print_flush out_ft ();
+             let r = Buffer.contents out_buff in
+             Buffer.clear out_buff; r)
+
 let coqide_known_option table = List.mem table [
   ["Printing";"Implicit"];
   ["Printing";"Coercions"];
@@ -242,41 +263,42 @@ let compute_reset_info loc_ast =
     loc_ast = loc_ast;
   }
 
-let parsable_of_string s =
-  Pcoq.Gram.parsable (Stream.of_string s)
+(** Check whether a command is forbidden by CoqIDE *)
+
+let coqide_cmd_checks (loc,ast) =
+  let user_error s =
+    raise (Loc.Exc_located (loc, Util.UserError ("CoqIde", str s)))
+  in
+  if is_vernac_debug_command ast then
+    user_error "Debug mode not available within CoqIDE";
+  if is_vernac_navigation_command ast then
+    user_error "Use CoqIDE navigation instead";
+  if is_vernac_known_option_command ast then
+    user_error "Use CoqIDE display menu instead";
+  if is_vernac_query_command ast then
+    msgerrnl (str "Warning: query commands should not be inserted in scripts")
+
+let raw_eval_expr = Vernac.eval_expr
 
 let eval_expr loc_ast =
   let rewind_info = compute_reset_info loc_ast in
-  Vernac.eval_expr loc_ast;
+  raw_eval_expr loc_ast;
   Stack.push rewind_info com_stk
 
-let raw_interp s =
-  Vernac.eval_expr (Vernac.parse_sentence (parsable_of_string s,None))
-
-let user_error_loc l s =
-    raise (Loc.Exc_located (l, Util.UserError ("CoqIde", s)))
-
-let interp (verbosely,s) =
+let interp (raw,verbosely,s) =
   prerr_endline "Starting interp...";
   prerr_endline s;
-  let pa = parsable_of_string s in
-  try
-    let (loc,vernac) = Vernac.parse_sentence (pa,None) in
-    if is_vernac_debug_command vernac then
-      user_error_loc loc (str "Debug mode not available within CoqIDE");
-    if is_vernac_navigation_command vernac then
-      user_error_loc loc (str "Use CoqIDE navigation instead");
-    if is_vernac_known_option_command vernac then
-      user_error_loc loc (str "Use CoqIDE display menu instead");
-    if is_vernac_query_command vernac then
-      msgerrnl (str "Warning: query commands should not be inserted in scripts");
-    if not (is_vernac_goal_printing_command vernac) then
-      (* Verbose if in small step forward and not a tactic *)
-      Flags.make_silent (not verbosely);
-    eval_expr (loc,vernac);
-    Flags.make_silent true;
-    prerr_endline ("...Done with interp of : "^s);
-  with Vernac.End_of_input -> assert false
+  let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+  let loc_ast = Vernac.parse_sentence (pa,None) in
+  if not raw then coqide_cmd_checks loc_ast;
+  (* Verbose if command is not a tactic and IDE said to be verbose
+     (i.e. we're in small step forward mode) *)
+  Flags.make_silent
+    (is_vernac_goal_printing_command (snd loc_ast) || not verbosely);
+  if raw then raw_eval_expr loc_ast else eval_expr loc_ast;
+  Flags.make_silent true;
+  prerr_endline ("...Done with interp of : "^s);
+  read_stdout ()
 
 let rewind count =
   let undo_ops = Hashtbl.create 31 in
@@ -333,7 +355,7 @@ let rewind count =
   in
   do_rewind count NoReset current_proofs None
 
-let is_in_loadpath dir =
+let inloadpath dir =
   Library.is_in_load_paths (System.physical_path_of_string dir)
 
 let string_of_ppcmds c =
@@ -388,7 +410,7 @@ let concl_next_tac sigma concl =
     "right"
   ])
 
-let current_goals () =
+let goals () =
   try
     let pfts =
       Proof_global.give_me_the_proof ()
@@ -430,7 +452,7 @@ let current_goals () =
   with Proof_global.NoCurrentProof ->
     Ide_intf.Message "" (* quick hack to have a clean message screen *)
 
-let current_status () =
+let status () =
   (** We remove the initial part of the current [dir_path]
       (usually Top in an interactive session, cf "coqtop -top"),
       and display the other parts (opened sections and modules) *)
@@ -447,27 +469,6 @@ let current_status () =
   in
   "Ready"^path^proof
 
-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;
-     set_binary_mode_out !orig_stdout true;
-     set_binary_mode_in stdin true;
-  ),
-  (fun () -> Format.pp_print_flush out_ft ();
-             let r = Buffer.contents out_buff in
-             Buffer.clear out_buff; r)
-
 let explain_exn e =
   let toploc,exc =
     match e with
@@ -480,6 +481,8 @@ let explain_exn e =
   toploc,(Errors.print exc)
 
 let eval_call c =
+  (* If the messages of last command are still there, we remove them *)
+  ignore (read_stdout ());
   let rec handle_exn e =
     catch_break := false;
     match e with
@@ -498,14 +501,12 @@ let eval_call c =
     r
   in
   let handler = {
-    Ide_intf.is_in_loadpath = interruptible is_in_loadpath;
-    Ide_intf.raw_interp = interruptible raw_interp;
     Ide_intf.interp = interruptible interp;
     Ide_intf.rewind = interruptible rewind;
-    Ide_intf.read_stdout = interruptible read_stdout;
-    Ide_intf.current_goals = interruptible current_goals;
-    Ide_intf.current_status = interruptible current_status;
-    Ide_intf.make_cases = interruptible Vernacentries.make_cases }
+    Ide_intf.goals = interruptible goals;
+    Ide_intf.status = interruptible status;
+    Ide_intf.inloadpath = interruptible inloadpath;
+    Ide_intf.mkcases = interruptible Vernacentries.make_cases }
   in
   Ide_intf.abstract_eval_call handler handle_exn c
 
@@ -529,7 +530,7 @@ let loop () =
       let q = (Marshal.from_channel: in_channel -> 'a Ide_intf.call) stdin in
       pr_debug ("<-- " ^ Ide_intf.pr_call q);
       let r = eval_call q in
-      pr_debug ("--> " ^ Ide_intf.pr_value r);
+      pr_debug ("--> " ^ Ide_intf.pr_full_value q r);
       Marshal.to_channel !orig_stdout r []; flush !orig_stdout
     done
   with e ->