deporting Coq specific code from ide to toplevel.

Still messy.

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

7 files changed, 23 insertions, 484 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 92dcd8222..beb8ebb52 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -104,9 +104,9 @@ object(self)
 	then com ^ " " else com ^ " " ^ entry#text ^" . "
       in
       try
-	ignore(Coq.interp Coq.dummy_coqtop false phrase);
+	Coq.raw_interp Coq.dummy_coqtop phrase;
 	result#buffer#set_text
-	  ("Result for command " ^ phrase ^ ":\n" ^ Ideutils.read_stdout ())
+	  ("Result for command " ^ phrase ^ ":\n" ^ (Coq.read_stdout Coq.dummy_coqtop))
       with e ->
 	let (s,loc) = Coq.process_exn e in
 	assert (Glib.Utf8.validate s);
diff --git a/ide/coq.ml b/ide/coq.ml
index e79d315a9..80e2da562 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -77,326 +77,17 @@ let version () =
     (if Mltop.is_native then "native" else "bytecode")
     (if Coq_config.best="opt" then "native" else "bytecode")
 
-let is_in_loadpath coqtop dir =
-  Library.is_in_load_paths (System.physical_path_of_string dir)
+let is_in_loadpath coqtop = Ide_blob.is_in_loadpath
+ 
+let reset_initial = Ide_blob.reinit
 
-let user_error_loc l s =
-  raise (Loc.Exc_located (l, Util.UserError ("CoqIde", s)))
+let raw_interp coqtop = Ide_blob.raw_interp
 
-let known_options = ref []
-
-let prepare_option (l,dft) =
-  known_options := l :: !known_options;
-  let set = (String.concat " " ("Set"::l)) ^ "." in
-  let unset = (String.concat " " ("Unset"::l)) ^ "." in
-  if dft then unset,set else set,unset
-
-let coqide_known_option table = List.mem table !known_options
-
-type command_attribute =
-    NavigationCommand | QueryCommand | DebugCommand | KnownOptionCommand
-  | OtherStatePreservingCommand | GoalStartingCommand | SolveCommand
-  | ProofEndingCommand
-
-let rec attribute_of_vernac_command = function
-  (* Control *)
-  | VernacTime com -> attribute_of_vernac_command com
-  | VernacTimeout(_,com) -> attribute_of_vernac_command com
-  | VernacFail com -> attribute_of_vernac_command com
-  | VernacList _ -> [] (* unsupported *)
-  | VernacLoad _ -> []
-
-  (* Syntax *)
-  | VernacTacticNotation _ -> []
-  | VernacSyntaxExtension _ -> []
-  | VernacDelimiters _ -> []
-  | VernacBindScope _ -> []
-  | VernacOpenCloseScope _ -> []
-  | VernacArgumentsScope _ -> []
-  | VernacInfix _ -> []
-  | VernacNotation _ -> []
-
-  (* Gallina *)
-  | VernacDefinition (_,_,DefineBody _,_) -> []
-  | VernacDefinition (_,_,ProveBody _,_) -> [GoalStartingCommand]
-  | VernacStartTheoremProof _ -> [GoalStartingCommand]
-  | VernacEndProof _ -> [ProofEndingCommand]
-  | VernacExactProof _ -> [ProofEndingCommand]
-
-  | VernacAssumption _ -> []
-  | VernacInductive _ -> []
-  | VernacFixpoint _ -> []
-  | VernacCoFixpoint _ -> []
-  | VernacScheme _ -> []
-  | VernacCombinedScheme _ -> []
-
-  (* Modules *)
-  | VernacDeclareModule _ -> []
-  | VernacDefineModule _  -> []
-  | VernacDeclareModuleType _ -> []
-  | VernacInclude _ -> []
-
-  (* Gallina extensions *)
-  | VernacBeginSection _ -> []
-  | VernacEndSegment _ -> []
-  | VernacRequire _ -> []
-  | VernacImport _ -> []
-  | VernacCanonical _ -> []
-  | VernacCoercion _ -> []
-  | VernacIdentityCoercion _ -> []
-
-  (* Type classes *)
-  | VernacInstance _ -> []
-  | VernacContext _ -> []
-  | VernacDeclareInstance _ -> []
-  | VernacDeclareClass _ -> []
-
-  (* Solving *)
-  | VernacSolve _ -> [SolveCommand]
-  | VernacSolveExistential _ -> [SolveCommand]
-
-  (* Auxiliary file and library management *)
-  | VernacRequireFrom _ -> []
-  | VernacAddLoadPath _ -> []
-  | VernacRemoveLoadPath _ -> []
-  | VernacAddMLPath _ -> []
-  | VernacDeclareMLModule _ -> []
-  | VernacChdir _ -> [OtherStatePreservingCommand]
-
-  (* State management *)
-  | VernacWriteState _ -> []
-  | VernacRestoreState _ -> []
-
-  (* Resetting *)
-  | VernacRemoveName _ -> [NavigationCommand]
-  | VernacResetName _ -> [NavigationCommand]
-  | VernacResetInitial -> [NavigationCommand]
-  | VernacBack _ -> [NavigationCommand]
-  | VernacBackTo _ -> [NavigationCommand]
-
-  (* Commands *)
-  | VernacDeclareTacticDefinition _ -> []
-  | VernacCreateHintDb _ -> []
-  | VernacHints _ -> []
-  | VernacSyntacticDefinition _ -> []
-  | VernacDeclareImplicits _ -> []
-  | VernacDeclareReduction _ -> []
-  | VernacReserve _ -> []
-  | VernacGeneralizable _ -> []
-  | VernacSetOpacity _ -> []
-  | VernacSetOption (_,["Ltac";"Debug"], _) -> [DebugCommand]
-  | VernacSetOption (_,o,BoolValue true) | VernacUnsetOption (_,o) ->
-      if coqide_known_option o then [KnownOptionCommand] else []
-  | VernacSetOption _ -> []
-  | VernacRemoveOption _ -> []
-  | VernacAddOption _ -> []
-  | VernacMemOption _ -> [QueryCommand]
-
-  | VernacPrintOption _ -> [QueryCommand]
-  | VernacCheckMayEval _ -> [QueryCommand]
-  | VernacGlobalCheck _ -> [QueryCommand]
-  | VernacPrint _ -> [QueryCommand]
-  | VernacSearch _ -> [QueryCommand]
-  | VernacLocate _ -> [QueryCommand]
-
-  | VernacComments _ -> [OtherStatePreservingCommand]
-  | VernacNop -> [OtherStatePreservingCommand]
-
-  (* Proof management *)
-  | VernacGoal _ -> [GoalStartingCommand]
-
-  | VernacAbort _ -> [NavigationCommand]
-  | VernacAbortAll -> [NavigationCommand]
-  | VernacRestart -> [NavigationCommand]
-  | VernacSuspend -> [NavigationCommand]
-  | VernacResume _ -> [NavigationCommand]
-  | VernacUndo _ -> [NavigationCommand]
-  | VernacUndoTo _ -> [NavigationCommand]
-  | VernacBacktrack _ -> [NavigationCommand]
-
-  | VernacFocus _ -> [SolveCommand]
-  | VernacUnfocus -> [SolveCommand]
-  | VernacGo _ -> []
-  | VernacShow _ -> [OtherStatePreservingCommand]
-  | VernacCheckGuard -> [OtherStatePreservingCommand]
-  | VernacProof (Tacexpr.TacId []) -> [OtherStatePreservingCommand]
-  | VernacProof _ -> []
-
-  | VernacProofMode _ -> []
-
-  | VernacSubproof _ -> [SolveCommand]
-  | VernacEndSubproof _ -> [SolveCommand]
-
-  (* Toplevel control *)
-  | VernacToplevelControl _ -> []
-
-
-  (* Extensions *)
-  | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand]
-  | VernacExtend _ -> []
-
-let is_vernac_goal_starting_command com =
-  List.mem GoalStartingCommand (attribute_of_vernac_command com)
-
-let is_vernac_navigation_command com =
-  List.mem NavigationCommand (attribute_of_vernac_command com)
-
-let is_vernac_query_command com =
-  List.mem QueryCommand (attribute_of_vernac_command com)
-
-let is_vernac_known_option_command com =
-  List.mem KnownOptionCommand (attribute_of_vernac_command com)
-
-let is_vernac_debug_command com =
-  List.mem DebugCommand (attribute_of_vernac_command com)
-
-let is_vernac_goal_printing_command com =
-  let attribute = attribute_of_vernac_command com in
-  List.mem GoalStartingCommand attribute or
-  List.mem SolveCommand attribute
-
-let is_vernac_state_preserving_command com =
-  let attribute = attribute_of_vernac_command com in
-  List.mem OtherStatePreservingCommand attribute or
-  List.mem QueryCommand attribute
-
-let is_vernac_tactic_command com =
-  List.mem SolveCommand (attribute_of_vernac_command com)
-
-let is_vernac_proof_ending_command com =
-  List.mem ProofEndingCommand (attribute_of_vernac_command com)
-
-type reset_status =
-  | NoReset
-  | ResetToNextMark
-  | ResetAtMark of Libnames.object_name
-
-type reset_info = {
-  status : reset_status;
-  proofs : identifier list;
-  cur_prf : (identifier * int) option;
-  loc_ast : Util.loc * Vernacexpr.vernac_expr;
-}
-
-let com_stk = Stack.create ()
-
-let parsable_of_string s =
-  Pcoq.Gram.parsable (Stream.of_string s)
-
-let reset_initial coqtop =
-  prerr_endline "Reset initial called"; flush stderr;
-  Stack.clear com_stk;
-  Vernacentries.abort_refine Lib.reset_initial ()
-
-let compute_reset_info loc_ast = 
-  let status,cur_prf = match snd loc_ast with
-    | com when is_vernac_tactic_command com ->
-        NoReset,Some (Pfedit.get_current_proof_name (),Pfedit.current_proof_depth ())
-    | com when is_vernac_state_preserving_command com -> NoReset,None
-    | com when is_vernac_proof_ending_command com -> ResetToNextMark,None
-    | VernacEndSegment _ -> NoReset,None
-    | _ ->
-        (match Lib.has_top_frozen_state () with
-           | Some sp -> 
-               prerr_endline ("On top of state "^Libnames.string_of_path (fst sp));
-               ResetAtMark sp,None
-           | None -> prerr_endline "No top state"; (NoReset,None))
-  in
-  { status = status;
-    proofs = Pfedit.get_all_proof_names ();
-    cur_prf = cur_prf;
-    loc_ast = loc_ast; 
-  }
-
-let eval_expr cmd_stk loc_ast =
-  let rewind_info = compute_reset_info loc_ast in
-  Vernac.eval_expr loc_ast;
-  Stack.push rewind_info cmd_stk;
-  Stack.length cmd_stk
-
-let interp coqtop 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
-  (* Temporary hack to make coqide.byte work (WTF???) - now with less screen
-  * pollution *)
-    Pervasives.prerr_string " \r"; Pervasives.flush stderr;
-    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
-      flash_info
-        "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);
-    let stack_depth = eval_expr com_stk (loc,vernac) in
-    Flags.make_silent true;
-    prerr_endline ("...Done with interp of : "^s);
-    stack_depth
-  with Vernac.End_of_input -> assert false
-
-let rewind coqtop count =
-  let undo_ops = Hashtbl.create 31 in
-  let current_proofs = Pfedit.get_all_proof_names () in
-  let rec do_rewind count reset_op prev_proofs curprf =
-    if (count <= 0) && (reset_op <> ResetToNextMark) &&
-       (Util.list_subset prev_proofs current_proofs) then
-      (* We backtracked at least what we wanted to, we have no proof to reopen,
-       * and we don't need to find a reset mark *)
-      begin
-        Hashtbl.iter
-          (fun id depth ->
-             if List.mem id prev_proofs then begin
-               Pfedit.suspend_proof ();
-	       Pfedit.resume_proof (Util.dummy_loc,id);
-               Pfedit.undo_todepth depth
-             end)
-          undo_ops;
-        prerr_endline "OK for undos";
-        Option.iter (fun id -> if List.mem id prev_proofs then
-                       Pfedit.suspend_proof ();
-		       Pfedit.resume_proof (Util.dummy_loc,id)) curprf;
-        prerr_endline "OK for focusing";
-        List.iter
-          (fun id -> Pfedit.delete_proof (Util.dummy_loc,id))
-          (Util.list_subtract current_proofs prev_proofs);
-        prerr_endline "OK for aborts";
-        (match reset_op with
-          | NoReset -> prerr_endline "No Reset"
-          | ResetAtMark m -> (prerr_endline ("Reset at "^(Libnames.string_of_path (fst m))); Lib.reset_to_state m)
-          | ResetToNextMark -> assert false);
-        prerr_endline "OK for reset"
-      end
-    else
-      begin
-        prerr_endline "pop";
-        let coq = Stack.pop com_stk in
-        let curprf =
-          Option.map
-            (fun (curprf,depth) ->
-               (if Hashtbl.mem undo_ops curprf then Hashtbl.replace else Hashtbl.add)
-                 undo_ops curprf depth;
-               curprf)
-            coq.cur_prf in
-        do_rewind (pred count)
-          (if coq.status <> NoReset then coq.status else reset_op) coq.proofs curprf;
-        if count <= 0 then begin
-          (* we had to backtrack further to find a suitable anchor point,
-           * replaying *)
-          prerr_endline "push";
-          ignore (eval_expr com_stk coq.loc_ast);
-        end
-      end
-  in
-  do_rewind count NoReset current_proofs None;
-  Stack.length com_stk
+let interp coqtop = Ide_blob.interp
 
+let rewind coqtop = Ide_blob.rewind
+ 
+let read_stdout = Ide_blob.read_stdout
 
 module PrintOpt =
 struct
@@ -418,17 +109,12 @@ struct
     List.iter
       (fun cmd -> 
          let str = (if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "." in
-         Vernac.eval_expr (Vernac.parse_sentence (parsable_of_string str,None)))
+         Ide_blob.raw_interp str)
       opt
 
   let enforce_hack () = Hashtbl.iter (set ()) state_hack 
 end
 
-(*
-let forbid_vernac blacklist (loc,vernac) =
-  List.map (fun (test,err) -> if test vernac then err loc
- *)
-
 let rec is_pervasive_exn = function
   | Out_of_memory | Stack_overflow | Sys.Break -> true
   | Error_in_file (_,_,e) -> is_pervasive_exn e
@@ -466,132 +152,10 @@ type  tried_tactic =
   | Success of int (* nb of goals after *)
   | Failed
 
-let string_of_ppcmds c =
-  Pp.msg_with Format.str_formatter c;
-  Format.flush_str_formatter ()
-
-type 'a menu = 'a * (string * string) list
-
-type goals =
-  | Message of string
-  | Goals of ((string menu) list * string menu) list
-
-let hyp_next_tac sigma env (id,_,ast) =
-  let id_s = Names.string_of_id id in
-  let type_s = string_of_ppcmds (pr_ltype_env env ast) in
-  [
-    ("clear "^id_s),("clear "^id_s^".\n");
-    ("apply "^id_s),("apply "^id_s^".\n");
-    ("exact "^id_s),("exact "^id_s^".\n");
-    ("generalize "^id_s),("generalize "^id_s^".\n");
-    ("absurd <"^id_s^">"),("absurd "^type_s^".\n")
-  ] @ (if Hipattern.is_equality_type ast then [
-    ("discriminate "^id_s),("discriminate "^id_s^".\n");
-    ("injection "^id_s),("injection "^id_s^".\n")
-  ] else []) @ (if Hipattern.is_equality_type (snd (Reductionops.splay_prod env sigma ast)) then [
-    ("rewrite "^id_s),("rewrite "^id_s^".\n");
-    ("rewrite <- "^id_s),("rewrite <- "^id_s^".\n")
-  ] else []) @ [
-    ("elim "^id_s), ("elim "^id_s^".\n");
-    ("inversion "^id_s), ("inversion "^id_s^".\n");
-    ("inversion clear "^id_s), ("inversion_clear "^id_s^".\n")
-  ]
-
-let concl_next_tac sigma concl =
-  let expand s = (s,s^".\n") in
-  List.map expand ([
-    "intro";
-    "intros";
-    "intuition"
-  ] @ (if Hipattern.is_equality_type (Goal.V82.concl sigma concl) then [
-    "reflexivity";
-    "discriminate";
-    "symmetry"
-  ] else []) @ [
-    "assumption";
-    "omega";
-    "ring";
-    "auto";
-    "eauto";
-    "tauto";
-    "trivial";
-    "decide equality";
-    "simpl";
-    "subst";
-    "red";
-    "split";
-    "left";
-    "right"
-  ])
-
 let goals coqtop =
   PrintOpt.enforce_hack ();
-  let pfts = Pfedit.get_pftreestate () in
-  let { it=all_goals ; sigma=sigma } = Proof.V82.subgoals pfts in
-  if all_goals = [] then
-    begin
-      Message (
-        let exl = Evarutil.non_instantiated sigma in
-        if exl = [] then "Proof Completed.\n" else
-          ("No more subgoals but non-instantiated existential variables:\n"^
-             string_of_ppcmds (pr_evars_int 1 exl)))
-    end
-  else
-    begin
-      let process_goal g =
-        let env = Goal.V82.env sigma g in
-        let ccl =
-	  let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
-          string_of_ppcmds (pr_ltype_env_at_top env norm_constr) in
-        let process_hyp h_env d acc =
-	  let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in
-          (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in
-        let hyps =
-          List.rev (Environ.fold_named_context process_hyp env ~init:[]) in
-        (hyps,(ccl,concl_next_tac sigma g))
-      in
-      Goals (List.map process_goal all_goals)
-    end
-
+  Ide_blob.current_goals ()
 
-let id_of_name = function
-  | Names.Anonymous -> id_of_string "x"
-  | Names.Name x -> x
-
-let make_cases coqtop s =
-  let qualified_name = Libnames.qualid_of_string s in
-  let glob_ref = Nametab.locate qualified_name in
-  match glob_ref with
-    | Libnames.IndRef i ->
-	let {Declarations.mind_nparams = np},
-	{Declarations.mind_consnames = carr ;
-	 Declarations.mind_nf_lc = tarr }
-	= Global.lookup_inductive i
-	in
-	Util.array_fold_right2
-	  (fun n t l ->
-	     let (al,_) = Term.decompose_prod t in
-	     let al,_ = Util.list_chop (List.length al - np) al in
-	     let rec rename avoid = function
-	       | [] -> []
-	       | (n,_)::l ->
-		   let n' = next_ident_away_in_goal
-			      (id_of_name n)
-			      avoid
-		   in (string_of_id n')::(rename (n'::avoid) l)
-	     in
-	     let al' = rename [] (List.rev al) in
-	     (string_of_id n :: al') :: l
-	  )
-	  carr
-	  tarr
-	  []
-    | _ -> raise Not_found
-
-let current_status coqtop =
-  let path = msg (Libnames.pr_dirpath (Lib.cwd ())) in
-  let path = if path = "Top" then "Ready" else "Ready in " ^ String.sub path 4 (String.length path - 4) in
-  try
-    path ^ ", proving " ^ (Names.string_of_id (Pfedit.get_current_proof_name ()))
-  with _ -> path
+let make_cases coqtop = Ide_blob.make_cases
 
+let current_status = Ide_blob.current_status
diff --git a/ide/coq.mli b/ide/coq.mli
index d1568203f..231d2dc63 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -10,6 +10,7 @@ open Names
 open Term
 open Environ
 open Evd
+open Ide_blob
 
 val short_version : unit -> string
 val version : unit -> string
@@ -35,10 +36,15 @@ end
 val reset_initial : coqtop -> unit
 
 val init : unit -> string list
+
+val raw_interp : coqtop -> string -> unit
+
 val interp : coqtop -> bool -> string -> int
 
 val rewind : coqtop -> int -> int
 
+val read_stdout : coqtop -> string
+
 val process_exn : exn -> string*(Util.loc option)
 
 val is_in_loadpath : coqtop -> string -> bool
@@ -54,10 +60,4 @@ type tried_tactic =
 
 val current_status : coqtop -> string
 
-type 'a menu = 'a * (string * string) list
-
-type goals =
-  | Message of string
-  | Goals of ((string menu) list * string menu) list
-
 val goals : coqtop -> goals
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 32f2bdd71..e49434303 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -778,7 +778,7 @@ object(self)
         prerr_endline "Send_to_coq starting now";
         let r = Coq.interp Coq.dummy_coqtop verbosely phrase in
         let is_complete = true in
-        let msg = read_stdout () in
+        let msg = Coq.read_stdout Coq.dummy_coqtop in
         sync display_output msg;
         Some (is_complete,r)
       with e ->
@@ -1008,7 +1008,6 @@ object(self)
                 prerr_endline "Moving (long) start_of_input...";
                 input_buffer#move_mark ~where:start (`NAME "start_of_input");
                 self#show_goals;
-                clear_stdout ();
                 self#clear_message)
           ();
       with _ ->
@@ -3121,7 +3120,6 @@ let start () =
 		  then Pp.warning msg
 		  else failwith ("Coqide internal error: " ^ msg)));
     Command_windows.main ();
-    init_stdout ();
     main files;
     if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ());
     while true do
diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index fe8a70e01..e8f21e239 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -89,7 +89,7 @@ let mode_cesar (proof:GText.view) = function
 let display mode (view:GText.view) goals =
   view#buffer#set_text "";
   match goals with
-    | Coq.Message msg ->
+    | Ide_blob.Message msg ->
         view#buffer#insert msg
-    | Coq.Goals g ->
+    | Ide_blob.Goals g ->
         mode view g
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index aaade8aa5..46e6d43eb 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -147,26 +147,6 @@ let set_highlight_timer f =
 	Some (GMain.Timeout.add ~ms:2000
 		~callback:(fun () -> f (); highlight_timer := None; true))
 
-
-(* Get back the standard coq out channels *)
-let init_stdout,read_stdout,clear_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 () ->
-    Pp_control.std_ft := out_ft;
-    Pp_control.err_ft := out_ft;
-    Pp_control.deep_ft := deep_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)
-
-
 let last_dir = ref ""
 
 let filter_all_files () = GFile.filter
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 0d57b855e..993856a3a 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -16,8 +16,6 @@ val doc_url : unit -> string
 val browse : (string -> unit) -> string -> unit
 val browse_keyword : (string -> unit) -> string -> unit
 val byte_offset_to_char_offset : string -> int -> int
-val init_stdout : unit -> unit
-val clear_stdout : unit -> unit
 val debug : bool ref
 val disconnect_revert_timer : unit -> unit
 val disconnect_auto_save_timer : unit -> unit
@@ -36,7 +34,6 @@ val prerr_endline : string -> unit
 val prerr_string : string -> unit
 val print_id : 'a -> unit
 
-val read_stdout : unit -> string
 val revert_timer : GMain.Timeout.id option ref
 val auto_save_timer : GMain.Timeout.id option ref
 val select_file_for_open :