Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 182 insertions, 681 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 1c6229b4..16a07b01 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -1,53 +1,14 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-open Vernac
-open Vernacexpr
-open Pfedit
-open Pp
-open Util
-open Names
-open Term
-open Printer
-open Environ
-open Evarutil
-open Evd
-open Decl_mode
-open Hipattern
-open Tacmach
-open Reductionops
-open Termops
-open Namegen
 open Ideutils
 
-let msg m =
-  let b =  Buffer.create 103 in
-  Pp.msg_with (Format.formatter_of_buffer b) m;
-  Buffer.contents b
-
-let msgnl m =
-  (msg m)^"\n"
-
-let init () =
-  (* To hide goal in lower window.
-     Problem: should not hide "xx is assumed"
-     messages *)
-(**)
-  Flags.make_silent true;
-  (* don't set a too large undo stack because Edit.create allocates an array *)
-  Pfedit.set_undo (Some 5000);
-(**)
-  Coqtop.init_ide ()
-
-
-let i = ref 0
+(** * Version and date *)
 
 let get_version_date () =
   let date =
@@ -55,7 +16,12 @@ let get_version_date () =
     then Coq_config.date
     else "<date not printable>" in
   try
-    let ch = open_in (Coq_config.coqsrc^"/revision") in
+    (* the following makes sense only when running with local layout *)
+    let coqroot = Filename.concat
+      (Filename.dirname Sys.executable_name)
+      Filename.parent_dir_name
+    in
+    let ch = open_in (Filename.concat coqroot "revision") in
     let ver = input_line ch in
     let rev = input_line ch in
     (ver,rev)
@@ -71,656 +37,191 @@ let version () =
       "The Coq Proof Assistant, version %s (%s)\
        \nArchitecture %s running %s operating system\
        \nGtk version is %s\
-       \nThis is the %s version (%s is the best one for this architecture and OS)\
+       \nThis is %s (%s is the best one for this architecture and OS)\
        \n"
       ver date
       Coq_config.arch Sys.os_type
       (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
-    (if Mltop.is_native then "native" else "bytecode")
-    (if Coq_config.best="opt" then "native" else "bytecode")
-
-let is_in_coq_lib dir =
-  prerr_endline ("Is it a coq theory ? : "^dir);
-  let is_same_file = same_file dir in
-  List.exists
-    (fun s ->
-      let fdir =
-        Filename.concat (Envars.coqlib ()) (Filename.concat "theories" s) in
-      prerr_endline (" Comparing to: "^fdir);
-      if is_same_file fdir then (prerr_endline " YES";true)
-      else (prerr_endline"NO";false))
-    Coq_config.theories_dirs
-
-let is_in_loadpath dir =
-  Library.is_in_load_paths (System.physical_path_of_string dir)
-
-let is_in_coq_path f =
+      (Filename.basename Sys.executable_name)
+      Coq_config.best
+
+
+(** * Initial checks by launching test coqtop processes *)
+
+let rec read_all_lines in_chan =
+  try
+    let arg = input_line in_chan in
+    arg::(read_all_lines in_chan)
+  with End_of_file -> []
+
+let filter_coq_opts args =
+  let argstr = String.concat " " (List.map Filename.quote args) in
+  let cmd = Filename.quote !Minilib.coqtop_path ^" -nois -filteropts " ^ argstr in
+  let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in
+  let filtered_args = read_all_lines oc in
+  let message = read_all_lines ec in
+  match Unix.close_process_full (oc,ic,ec) with
+    | Unix.WEXITED 0 -> true,filtered_args
+    | Unix.WEXITED 2 -> false,filtered_args
+    | _ -> false,message
+
+exception Coqtop_output of string list
+
+let check_connection args =
   try
-  let base = Filename.chop_extension (Filename.basename f) in
-  let _ = Library.locate_qualified_library false
-	    (Libnames.make_qualid Names.empty_dirpath
-	       (Names.id_of_string base)) in
-  prerr_endline (f ^ " is in coq path");
-  true
-  with _ ->
-    prerr_endline (f ^ " is NOT in coq path");
-    false
-
-let is_in_proof_mode () =
-  match Decl_mode.get_current_mode () with
-      Decl_mode.Mode_none -> false
-    | _ -> true
-
-let user_error_loc l s =
-  raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s)))
-
-type printing_state = {
-  mutable printing_implicit : bool;
-  mutable printing_coercions : bool;
-  mutable printing_raw_matching : bool;
-  mutable printing_no_notation : bool;
-  mutable printing_all : bool;
-  mutable printing_evar_instances : bool;
-  mutable printing_universes : bool;
-  mutable printing_full_all : bool
+    let argstr = String.concat " " (List.map Filename.quote args) in
+    let cmd = Filename.quote !Minilib.coqtop_path ^ " -batch " ^ argstr in
+    let ic = Unix.open_process_in cmd in
+    let lines = read_all_lines ic in
+    match Unix.close_process_in ic with
+    | Unix.WEXITED 0 -> prerr_endline "coqtop seems ok"
+    | _ -> raise (Coqtop_output lines)
+  with
+    | End_of_file ->
+      Minilib.safe_prerr_endline "Cannot start connection with coqtop";
+      exit 1
+    | Coqtop_output lines ->
+      Minilib.safe_prerr_endline "Connection with coqtop failed:";
+      List.iter Minilib.safe_prerr_endline lines;
+      exit 1
+
+(** * The structure describing a coqtop sub-process *)
+
+type coqtop = {
+  pid : int; (* Unix process id *)
+  cout : in_channel ;
+  cin : out_channel ;
+  sup_args : string list;
 }
 
-let printing_state = {
-  printing_implicit = false;
-  printing_coercions = false;
-  printing_raw_matching = false;
-  printing_no_notation = false;
-  printing_all = false;
-  printing_evar_instances = false;
-  printing_universes = false;
-  printing_full_all = false;
-}
+(** * Count of all active coqtops *)
 
-let printing_implicit_data = ["Printing";"Implicit"], false
-let printing_coercions_data = ["Printing";"Coercions"], false
-let printing_raw_matching_data = ["Printing";"Matching"], true
-let printing_no_synth_data = ["Printing";"Synth"], true
-let printing_no_notation_data = ["Printing";"Notations"], true
-let printing_all_data = ["Printing";"All"], false
-let printing_evar_instances_data = ["Printing";"Existential";"Instances"],false
-let printing_universes_data = ["Printing";"Universes"], false
-
-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
-
-let with_printing_implicit = prepare_option printing_implicit_data
-let with_printing_coercions = prepare_option printing_coercions_data
-let with_printing_raw_matching = prepare_option printing_raw_matching_data
-let with_printing_no_synth = prepare_option printing_no_synth_data
-let with_printing_no_notation = prepare_option printing_no_notation_data
-let with_printing_all = prepare_option printing_all_data
-let with_printing_evar_instances = prepare_option printing_evar_instances_data
-let with_printing_universes = prepare_option printing_universes_data
-
-let make_option_commands () =
-  let p = printing_state in
-  (if p.printing_implicit then [with_printing_implicit] else [])@
-  (if p.printing_coercions then [with_printing_coercions] else [])@
-  (if p.printing_raw_matching then [with_printing_raw_matching;with_printing_no_synth] else [])@
-  (if p.printing_no_notation then [with_printing_no_notation] else [])@
-  (if p.printing_all then [with_printing_all] else [])@
-  (if p.printing_evar_instances then [with_printing_evar_instances] else [])@
-  (if p.printing_universes then [with_printing_universes] else [])@
-  (if p.printing_full_all then [with_printing_all;with_printing_evar_instances;with_printing_universes] else [])
-
-let make_option_commands () =
-  let l = make_option_commands () in
-  List.iter (fun (a,b) -> prerr_endline a; prerr_endline b) l;
-  l
-
-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]
-
-  (* MMode *)
-  | VernacDeclProof -> [SolveCommand]
-  | VernacReturn -> [SolveCommand]
-  | VernacProofInstr _ -> [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 _ -> []
-  | 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 _ -> []
-
-  (* 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 undo_info = identifier list
-
-let undo_info () = Pfedit.get_all_proof_names ()
-
-type reset_mark = Libnames.object_name
-
-type reset_status =
-  | NoReset
-  | ResetAtSegmentStart of Names.identifier
-  | ResetAtRegisteredObject of reset_mark
-
-type reset_info = {
-  status : reset_status;
-  proofs : identifier list;
-  cur_prf : (identifier * int) option;
-  loc_ast : Util.loc * Vernacexpr.vernac_expr;
-}
+let toplvl_ctr = ref 0
+
+let toplvl_ctr_mtx = Mutex.create ()
 
-let compute_reset_info loc_ast = 
-  let status,cur_prf = match snd loc_ast with
-    | com when is_vernac_proof_ending_command com -> NoReset,None
-    | VernacEndSegment _ -> NoReset,None
-    | com when is_vernac_tactic_command com ->
-        NoReset,Some (Pfedit.get_current_proof_name (), Pfedit.current_proof_depth ())
-    | _ ->
-        (match Lib.has_top_frozen_state () with
-           | Some sp -> 
-               prerr_endline ("On top of state "^Libnames.string_of_path (fst sp));
-               ResetAtRegisteredObject sp,None
-           | None -> NoReset,None)
-  in
-  { status = status;
-    proofs = Pfedit.get_all_proof_names ();
-    cur_prf = cur_prf;
-    loc_ast = loc_ast; 
-  }
-
-let reset_initial () =
-  prerr_endline "Reset initial called";
-  Vernacentries.abort_refine Lib.reset_initial ()
-
-let reset_to sp =
-      prerr_endline
-        ("Reset called with state "^(Libnames.string_of_path (fst sp)));
-      Lib.reset_to_state sp
-
-let raw_interp s =
-  Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s))
-
-let interp_with_options verbosely options s =
-  prerr_endline "Starting interp...";
-  prerr_endline s;
-  let pa = Pcoq.Gram.parsable (Stream.of_string s) in
-  let pe = Pcoq.Gram.Entry.parse Pcoq.main_entry pa in
-  (* Temporary hack to make coqide.byte work (WTF???) - now with less screen
-  * pollution *)
-  (try Pervasives.prerr_string " \r"; Pervasives.flush stderr with _ -> ());
-  match pe with
-    | None -> assert false
-    | Some((loc,vernac) as last) ->
-	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 reset_info = compute_reset_info last in
-	List.iter (fun (set_option,_) -> raw_interp set_option) options;
-	raw_interp s;
-	Flags.make_silent true;
-	List.iter (fun (_,unset_option) -> raw_interp unset_option) options;
-	prerr_endline ("...Done with interp of : "^s);
-	reset_info
-
-let interp verbosely phrase =
-  interp_with_options verbosely (make_option_commands ()) phrase
-
-let interp_and_replace s =
-  let result = interp false s in
-  let msg = read_stdout () in
-  result,msg
-
-let rec is_pervasive_exn = function
-  | Out_of_memory | Stack_overflow | Sys.Break -> true
-  | Error_in_file (_,_,e) -> is_pervasive_exn e
-  | Stdpp.Exc_located (_,e) -> is_pervasive_exn e
-  | DuringCommandInterp (_,e) -> is_pervasive_exn e
-  | _ -> false
-
-let print_toplevel_error exc =
-  let (dloc,exc) =
-    match exc with
-      | DuringCommandInterp (loc,ie) ->
-          if loc = dummy_loc then (None,ie) else (Some loc, ie)
-      | _ -> (None, exc)
-  in
-  let (loc,exc) =
-    match exc with
-      | Stdpp.Exc_located (loc, ie) -> (Some loc),ie
-      | Error_in_file (s, (_,fname, loc), ie) -> None, ie
-      | _ -> dloc,exc
-  in
-  match exc with
-    | End_of_input  -> 	str "Please report: End of input",None
-    | Vernacexpr.Drop ->  str "Drop is not allowed by coqide!",None
-    | Vernacexpr.Quit -> str "Quit is not allowed by coqide! Use menus.",None
-    | _ ->
-	(try Cerrors.explain_exn exc with e ->
-	   str "Failed to explain error. This is an internal Coq error. Please report.\n"
-	   ++ str (Printexc.to_string  e)),
-	(if is_pervasive_exn exc then None else loc)
-
-let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc)
-
-let interp_last last =
-  prerr_string "*";
+let coqtop_zombies () =
+  Mutex.lock toplvl_ctr_mtx;
+  let res = !toplvl_ctr in
+  Mutex.unlock toplvl_ctr_mtx;
+  res
+
+
+(** * Starting / signaling / ending a real coqtop sub-process *)
+
+(** We simulate a Unix.open_process that also returns the pid of
+    the created process. Note: this uses Unix.create_process, which
+    doesn't call bin/sh, so args shouldn't be quoted. The process
+    cannot be terminated by a Unix.close_process, but rather by a
+    kill of the pid.
+
+           >--ide2top_w--[pipe]--ide2top_r-->
+    coqide                                   coqtop
+           <--top2ide_r--[pipe]--top2ide_w--<
+
+    Note: we use Unix.stderr in Unix.create_process to get debug
+    messages from the coqtop's Ide_slave loop.
+*)
+
+let open_process_pid prog args =
+  let (ide2top_r,ide2top_w) = Unix.pipe () in
+  let (top2ide_r,top2ide_w) = Unix.pipe () in
+  let pid = Unix.create_process prog args ide2top_r top2ide_w Unix.stderr in
+  assert (pid <> 0);
+  Unix.close ide2top_r;
+  Unix.close top2ide_w;
+  let oc = Unix.out_channel_of_descr ide2top_w in
+  let ic = Unix.in_channel_of_descr top2ide_r in
+  set_binary_mode_out oc true;
+  set_binary_mode_in ic true;
+  (pid,ic,oc)
+
+let spawn_coqtop sup_args =
+  Mutex.lock toplvl_ctr_mtx;
   try
-    vernac_com Vernacentries.interp last;
-    Lib.add_frozen_state()
+    let prog = !Minilib.coqtop_path in
+    let args = Array.of_list (prog :: "-ideslave" :: sup_args) in
+    let (pid,ic,oc) = open_process_pid prog args in
+    incr toplvl_ctr;
+    Mutex.unlock toplvl_ctr_mtx;
+    { pid = pid; cin = oc; cout = ic ; sup_args = sup_args }
   with e ->
-    let s,_ = process_exn e in prerr_endline ("Replay during undo failed because: "^s);
+    Mutex.unlock toplvl_ctr_mtx;
     raise e
 
-let push_phrase cmd_stk reset_info ide_payload =
-  Stack.push (ide_payload,reset_info) cmd_stk
-
-type backtrack =
-  | BacktrackToNextActiveMark
-  | BacktrackToMark of reset_mark
-  | NoBacktrack
-
-let apply_reset = function
-  | BacktrackToMark mark -> reset_to mark
-  | NoBacktrack -> ()
-  | BacktrackToNextActiveMark -> assert false
-
-let rewind sequence cmd_stk =
-  let undo_ops = Hashtbl.create 31 in
-  let current_proofs = undo_info () in
-  let pop_state cont seq coq reset_op prev_proofs curprf =
-    prerr_endline "pop";
-    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
-    let reset_op =
-      match coq.status with
-        | ResetAtRegisteredObject mark ->
-            BacktrackToMark mark
-        | _ when is_vernac_state_preserving_command (snd coq.loc_ast) ->
-            reset_op
-        | _ when is_vernac_tactic_command (snd coq.loc_ast) ->
-            reset_op
-        | _ ->
-            BacktrackToNextActiveMark in
-    cont seq reset_op coq.proofs curprf
-  in
-  let rec do_rewind seq reset_op prev_proofs curprf =
-    match seq with
-      | [] when ((reset_op <> BacktrackToNextActiveMark) &&
-                 (Util.list_subset prev_proofs current_proofs)) ->
-          begin
-            Hashtbl.iter
-              (fun id depth ->
-                 if List.mem id prev_proofs then begin
-                   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.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";
-            apply_reset reset_op;
-            prerr_endline "OK for reset"
-          end
-      | [] ->
-          begin
-            try 
-              let ide,coq = Stack.pop cmd_stk in
-              pop_state do_rewind [] coq reset_op prev_proofs curprf;
-              prerr_endline "push";
-              let reset_info = compute_reset_info coq.loc_ast in
-              interp_last coq.loc_ast;
-              push_phrase cmd_stk reset_info ide
-            with Stack.Empty -> reset_initial ()
-          end
-      | coq::rem ->
-          pop_state do_rewind rem coq reset_op prev_proofs curprf
-  in
-  do_rewind sequence NoBacktrack current_proofs None
-
-type  tried_tactic =
-  | Interrupted
-  | Success of int (* nb of goals after *)
-  | Failed
-
-type hyp = env * evar_map *
-           ((identifier * string) * constr option * constr) *
-           (string * string)
-type concl = env * evar_map * constr * string
-type meta = env * evar_map * string
-type goal = hyp list * concl
-
-let prepare_hyp sigma env ((i,c,d) as a) =
-  env, sigma,
-  ((i,string_of_id i),c,d),
-  (msg (pr_var_decl env a), msg (pr_ltype_env env d))
-
-let prepare_hyps sigma env =
-  assert (rel_context env = []);
-  let hyps =
-    fold_named_context
-      (fun env d acc -> let hyp = prepare_hyp sigma env d in hyp :: acc)
-      env ~init:[]
-  in
-  List.rev hyps
-
-let prepare_goal_main sigma g =
-  let env = evar_env g in
-  (prepare_hyps sigma env,
-   (env, sigma, g.evar_concl, msg (pr_ltype_env_at_top env g.evar_concl)))
-
-let prepare_goal sigma g =
-  let options = make_option_commands () in
-  List.iter (fun (set_option,_) -> raw_interp set_option) options;
-  let x = prepare_goal_main sigma g in
-  List.iter (fun (_,unset_option) -> raw_interp unset_option) options;
-  x
-
-let get_current_pm_goal () =
-  let pfts = get_pftreestate ()  in
-  let gls = try nth_goal_of_pftreestate 1 pfts with _ -> raise Not_found in
-  let sigma= sig_sig gls in
-  let gl = sig_it gls in
-    prepare_goal sigma gl
-
-let get_current_goals () =
-    let pfts = get_pftreestate () in
-    let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in
-    let sigma = Tacmach.evc_of_pftreestate pfts in
-    List.map (prepare_goal sigma) gls
-
-let print_no_goal () =
-  (* Fall back on standard coq goal printer for completed goal printing *)
-  msg (pr_open_subgoals ())
-
-let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
-  [("clear "^ident),("clear "^ident^".");
-
-   ("apply "^ident),
-   ("apply "^ident^".");
-
-   ("exact "^ident),
-   ("exact "^ident^".");
-
-   ("generalize "^ident),
-   ("generalize "^ident^".");
-
-   ("absurd <"^ident^">"),
-   ("absurd "^
-    pr_ast
-    ^".") ] @
-
-   (if is_equality_type ast then
-      [ "discriminate "^ident, "discriminate "^ident^".";
-	"injection "^ident, "injection "^ident^"." ]
-    else
-      []) @
-
-   (let _,t = splay_prod env sigma ast in
-    if is_equality_type t then
-      [ "rewrite "^ident, "rewrite "^ident^".";
-	"rewrite <- "^ident, "rewrite <- "^ident^"." ]
-    else
-      []) @
-
-  [("elim "^ident),
-   ("elim "^ident^".");
-
-   ("inversion "^ident),
-   ("inversion "^ident^".");
-
-   ("inversion clear "^ident),
-   ("inversion_clear "^ident^".")]
-
-let concl_menu (_,_,concl,_) =
-  let is_eq = is_equality_type concl in
-  ["intro", "intro.";
-   "intros", "intros.";
-   "intuition","intuition." ] @
-
-   (if is_eq then
-      ["reflexivity", "reflexivity.";
-       "discriminate", "discriminate.";
-       "symmetry", "symmetry." ]
-    else
-      []) @
-
-  ["assumption" ,"assumption.";
-   "omega", "omega.";
-   "ring", "ring.";
-   "auto with *", "auto with *.";
-   "eauto with *", "eauto with *.";
-   "tauto", "tauto.";
-   "trivial", "trivial.";
-   "decide equality", "decide equality.";
-
-   "simpl", "simpl.";
-   "subst", "subst.";
-
-   "red", "red.";
-   "split", "split.";
-   "left", "left.";
-   "right", "right.";
-  ]
-
-
-let id_of_name = function
-  | Names.Anonymous -> id_of_string "x"
-  | Names.Name x -> x
-
-let make_cases 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 () =
-  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 respawn_coqtop coqtop = spawn_coqtop coqtop.sup_args
+
+let interrupter = ref (fun pid -> Unix.kill pid Sys.sigint)
+let killer = ref (fun pid -> Unix.kill pid Sys.sigkill)
 
+let break_coqtop coqtop =
+  try !interrupter coqtop.pid
+  with _ -> prerr_endline "Error while sending Ctrl-C"
+
+let kill_coqtop coqtop =
+  let pid = coqtop.pid in
+  begin
+    try !killer pid
+    with _ -> prerr_endline "Kill -9 failed. Process already terminated ?"
+  end;
+  try
+    ignore (Unix.waitpid [] pid);
+    Mutex.lock toplvl_ctr_mtx; decr toplvl_ctr; Mutex.unlock toplvl_ctr_mtx
+  with _ -> prerr_endline "Error while waiting for child"
+
+(** * Calls to coqtop *)
+
+(** Cf [Ide_intf] for more details *)
+
+let p = Xml_parser.make ()
+let () = Xml_parser.check_eof p false
+
+let eval_call coqtop (c:'a Ide_intf.call) =
+  Xml_utils.print_xml coqtop.cin (Ide_intf.of_call c);
+  flush coqtop.cin;
+  let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in
+  (Ide_intf.to_answer xml : 'a Interface.value)
+
+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 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
+let hints coqtop = eval_call coqtop Ide_intf.hints
+
+module PrintOpt =
+struct
+  type t = string list
+  let implicit = ["Printing"; "Implicit"]
+  let coercions = ["Printing"; "Coercions"]
+  let raw_matching = ["Printing"; "Matching"; "Synth"]
+  let notations = ["Printing"; "Notations"]
+  let all_basic = ["Printing"; "All"]
+  let existential = ["Printing"; "Existential"; "Instances"]
+  let universes = ["Printing"; "Universes"]
+
+  let state_hack = Hashtbl.create 11
+  let _ = List.iter (fun opt -> Hashtbl.add state_hack opt false)
+            [ implicit; coercions; raw_matching; notations; all_basic; existential; universes ]
+
+  let set coqtop options =
+    let () = List.iter (fun (name, v) -> Hashtbl.replace state_hack name v) options in
+    let options = List.map (fun (name, v) -> (name, Interface.BoolValue v)) options in
+    match eval_call coqtop (Ide_intf.set_options options) with
+    | Interface.Good () -> ()
+    | _ -> raise (Failure "Cannot set options.")
+
+  let enforce_hack coqtop =
+    let elements = Hashtbl.fold (fun opt v acc -> (opt, v) :: acc) state_hack [] in
+    set coqtop elements
+
+end
+
+let goals coqtop =
+  let () = PrintOpt.enforce_hack coqtop in
+  eval_call coqtop Ide_intf.goals
+
+let evars coqtop =
+  let () = PrintOpt.enforce_hack coqtop in
+  eval_call coqtop Ide_intf.evars