Ide: stronger separation from coqtop

 Former module Ide_blob is now divided in Ide_intf (linked both
 by coqtop and coqide) and Ide_slave (now only in coqtop).
 Ide_intf has almost no dependencies, we can now compile coqide
 with only coq_config.cm* and lib.cm(x)a

 TODO:
  - Devise a better way to display whether coqide is byte or opt
    in the about message (instead of Mltop.is_native, I display
    now the executable name, which hopefully contains opt or byte)
  - Check the late error handling in ide/coq.ml

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

12 files changed, 232 insertions, 229 deletions

diff --git a/Makefile.common b/Makefile.common
index fa76dac60..c51ca4011 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -217,10 +217,15 @@ INITPLUGINSBEST:=$(if $(OPT),$(INITPLUGINSOPT),$(INITPLUGINS))
 LINKCMO:=$(CONFIG) $(CORECMA) $(STATICPLUGINS)
 LINKCMX:=$(CONFIG:.cmo=.cmx) $(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
 
+LIBCMA:=lib/lib.cma
 IDECMA:=ide/ide.cma
+IDEINTF:=toplevel/ide_intf.cmo
 
-LINKIDE:=$(LINKCMO) $(IDECMA) ide/coqide_main.ml
-LINKIDEOPT:=$(IDEOPTDEPS) $(LINKCMX) $(IDECMA:.cma=.cmxa) ide/coqide_main_opt.ml
+IDELIBS:=$(CONFIG) $(LIBCMA) $(IDEINTF) $(IDECMA)
+IDELIBSOPT:=$(subst .cmo,.cmx,$(IDELIBS:.cma=.cmxa))
+
+LINKIDE:=$(IDELIBS) ide/coqide_main.ml
+LINKIDEOPT:=$(IDEOPTDEPS) $(IDELIBSOPT) ide/coqide_main_opt.ml
 
 # modules known by the toplevel of Coq
 
diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index a351107d9..70bc4d1cd 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -106,13 +106,13 @@ object(self)
       try
         result#buffer#set_text
           (match Coq.raw_interp coqtop phrase with
-             | Ide_blob.Fail (l,str) ->
+             | Ide_intf.Fail (l,str) ->
                  ("Error while interpreting "^phrase^":\n"^str)
-             | Ide_blob.Good () ->
+             | Ide_intf.Good () ->
                  match Coq.read_stdout coqtop with
-                   | Ide_blob.Fail (l,str) ->
+                   | Ide_intf.Fail (l,str) ->
                        ("Error while fetching "^phrase^"results:\n"^str)
-                   | Ide_blob.Good results ->
+                   | Ide_intf.Good results ->
                        ("Result for command " ^ phrase ^ ":\n" ^ results))
       with e ->
 	let (s,loc) = Coq.process_exn e in
diff --git a/ide/coq.ml b/ide/coq.ml
index 89040aa5f..41c9546d1 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,24 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Vernac
-open Vernacexpr
-open Pfedit
-open Pp
 open Util
-open Names
-open Term
-open Printer
-open Environ
-open Evarutil
-open Evd
-open Hipattern
-open Tacmach
-open Reductionops
-open Termops
-open Namegen
-open Ideutils
 open Compat
+open Pp
+open Ideutils
 
 type coqtop = {
   mutable pid : int;
@@ -69,13 +55,13 @@ 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")
+      (Filename.basename Sys.executable_name)
+      Coq_config.best
 
 let rec read_all_lines in_chan =
   try
@@ -116,20 +102,20 @@ let check_connection args =
       List.iter Pervasives.prerr_endline lines;
       exit 1
 
-let eval_call coqtop (c:'a Ide_blob.call) =
+let eval_call coqtop (c:'a Ide_intf.call) =
   Marshal.to_channel coqtop.cin c [];
   flush coqtop.cin;
-  (Marshal.from_channel: in_channel -> 'a Ide_blob.value) coqtop.cout
+  (Marshal.from_channel: in_channel -> 'a Ide_intf.value) coqtop.cout
 
-let is_in_loadpath coqtop s = eval_call coqtop (Ide_blob.is_in_loadpath s)
+let is_in_loadpath coqtop s = eval_call coqtop (Ide_intf.is_in_loadpath s)
  
-let raw_interp coqtop s = eval_call coqtop (Ide_blob.raw_interp s)
+let raw_interp coqtop s = eval_call coqtop (Ide_intf.raw_interp s)
 
-let interp coqtop b s = eval_call coqtop (Ide_blob.interp b s)
+let interp coqtop b s = eval_call coqtop (Ide_intf.interp b s)
 
-let rewind coqtop i = eval_call coqtop (Ide_blob.rewind i)
+let rewind coqtop i = eval_call coqtop (Ide_intf.rewind i)
  
-let read_stdout coqtop = eval_call coqtop Ide_blob.read_stdout
+let read_stdout coqtop = eval_call coqtop Ide_intf.read_stdout
 
 let toplvl_ctr = ref 0
 
@@ -209,56 +195,30 @@ struct
       (fun acc cmd -> 
          let str = (if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "." in
          match raw_interp coqtop str with
-           | Ide_blob.Good () -> acc
-           | Ide_blob.Fail (l,errstr) ->  Ide_blob.Fail (l,"Could not eval \""^str^"\": "^errstr)
+           | Ide_intf.Good () -> acc
+           | Ide_intf.Fail (l,errstr) ->  Ide_intf.Fail (l,"Could not eval \""^str^"\": "^errstr)
       )
-      (Ide_blob.Good ())
+      (Ide_intf.Good ())
       opt
 
-  let enforce_hack coqtop = Hashtbl.fold (fun opt v acc ->
-                                            match set coqtop opt v with
-                                              | Ide_blob.Good () -> Ide_blob.Good ()
-                                              | Ide_blob.Fail str -> Ide_blob.Fail str)
-                              state_hack (Ide_blob.Good ())
+  let enforce_hack coqtop = Hashtbl.fold
+    (fun opt v acc ->
+      match set coqtop opt v with
+        | Ide_intf.Good () -> Ide_intf.Good ()
+        | Ide_intf.Fail str -> Ide_intf.Fail str)
+    state_hack (Ide_intf.Good ())
 end
 
-let rec is_pervasive_exn = function
-  | Out_of_memory | Stack_overflow | Sys.Break -> true
-  | Error_in_file (_,_,e) -> is_pervasive_exn e
-  | Loc.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
-      | Loc.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 process_exn = function
+  | End_of_file ->
+    "Warning: End_of_file occurred (possibly a forced restart of coqtop)", None
+  | e -> Printexc.to_string e,None
 
 let goals coqtop =
   match PrintOpt.enforce_hack coqtop with
-    | Ide_blob.Good () -> eval_call coqtop Ide_blob.current_goals
-    | Ide_blob.Fail str -> Ide_blob.Fail str
+    | Ide_intf.Good () -> eval_call coqtop Ide_intf.current_goals
+    | Ide_intf.Fail str -> Ide_intf.Fail str
 
-let make_cases coqtop s = eval_call coqtop (Ide_blob.make_cases s)
+let make_cases coqtop s = eval_call coqtop (Ide_intf.make_cases s)
 
-let current_status coqtop = eval_call coqtop Ide_blob.current_status
+let current_status coqtop = eval_call coqtop Ide_intf.current_status
diff --git a/ide/coq.mli b/ide/coq.mli
index c909a559f..a96ed31c7 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -6,12 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
-open Term
-open Environ
-open Evd
-open Ide_blob
-
 val short_version : unit -> string
 val version : unit -> string
 val filter_coq_opts : string list -> bool * string list
@@ -42,25 +36,25 @@ sig
   val existential : t
   val universes : t
 
-  val set : coqtop -> t -> bool -> unit Ide_blob.value
+  val set : coqtop -> t -> bool -> unit Ide_intf.value
 end
 
-val raw_interp : coqtop -> string -> unit Ide_blob.value
+val raw_interp : coqtop -> string -> unit Ide_intf.value
 
-val interp : coqtop -> bool -> string -> int Ide_blob.value
+val interp : coqtop -> bool -> string -> int Ide_intf.value
 
-val rewind : coqtop -> int -> int Ide_blob.value
+val rewind : coqtop -> int -> int Ide_intf.value
 
-val read_stdout : coqtop -> string Ide_blob.value
+val read_stdout : coqtop -> string Ide_intf.value
 
-val is_in_loadpath : coqtop -> string -> bool Ide_blob.value
+val is_in_loadpath : coqtop -> string -> bool Ide_intf.value
 
-val make_cases : coqtop -> string -> string list list Ide_blob.value
+val make_cases : coqtop -> string -> string list list Ide_intf.value
 
 (* Message to display in lower status bar. *)
 
-val current_status : coqtop -> string Ide_blob.value
+val current_status : coqtop -> string Ide_intf.value
 
-val goals : coqtop -> goals Ide_blob.value
+val goals : coqtop -> Ide_intf.goals Ide_intf.value
 
 val msgnl : Pp.std_ppcmds -> string
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 475b8f8a4..c7b231bf3 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -319,9 +319,9 @@ let setopts ct opts v =
   List.fold_left
     (fun acc o ->
        match set ct o v with
-         | Ide_blob.Good () -> acc
-         | Ide_blob.Fail lstr -> Ide_blob.Fail lstr
-    ) (Ide_blob.Good ()) opts
+         | Ide_intf.Good () -> acc
+         | Ide_intf.Fail lstr -> Ide_intf.Fail lstr
+    ) (Ide_intf.Good ()) opts
 
 (* Reset this to None on page change ! *)
 let (last_completion:(string*int*int*bool) option ref) = ref None
@@ -788,9 +788,9 @@ object(self)
           (fun _ _ -> ()) in
         try
           match Coq.goals mycoqtop with
-            | Ide_blob.Fail (l,str) ->
+            | Ide_intf.Fail (l,str) ->
                 self#set_message ("Error in coqtop :\n"^str)
-            | Ide_blob.Good goals ->
+            | Ide_intf.Good goals ->
                 Ideproof.display
                   (Ideproof.mode_tactic menu_callback)
                   proof_view goals
@@ -830,14 +830,14 @@ object(self)
       full_goal_done <- false;
       prerr_endline "Send_to_coq starting now";
       match Coq.interp mycoqtop verbosely phrase with
-        | Ide_blob.Fail (l,str) -> sync display_error (str,l); None
-        | Ide_blob.Good r ->
+        | Ide_intf.Fail (l,str) -> sync display_error (str,l); None
+        | Ide_intf.Good r ->
             match Coq.read_stdout mycoqtop with
-              | Ide_blob.Fail (_,str) ->
+              | Ide_intf.Fail (_,str) ->
                   self#set_message
                     ("interp successful but unable to fetch goal, please report bug:\n"^str);
                   None
-              | Ide_blob.Good msg ->
+              | Ide_intf.Good msg ->
                   sync display_output msg;
                   Some (true,r)
     with
@@ -1051,10 +1051,10 @@ object(self)
     begin
       try
         match Coq.rewind mycoqtop (n_step 0) with
-          | Ide_blob.Fail (l,str) ->
+          | Ide_intf.Fail (l,str) ->
               sync self#set_message
                 ("Problem while backtracking, CoqIDE and coqtop may be out of sync, you may want to restart :\n"^str)
-          | Ide_blob.Good _ ->
+          | Ide_intf.Good _ ->
               sync (fun _ ->
                       let start =
                         if Stack.is_empty cmd_stack then input_buffer#start_iter
@@ -1192,17 +1192,17 @@ object(self)
       | None -> ()
       | Some f -> let dir = Filename.dirname f in
         match Coq.is_in_loadpath mycoqtop dir with
-          | Ide_blob.Fail (_,str) ->
+          | Ide_intf.Fail (_,str) ->
               self#set_message
                 ("Could not determine lodpath, this might lead to problems:\n"^str)
-          | Ide_blob.Good true -> ()
-          | Ide_blob.Good false ->
+          | Ide_intf.Good true -> ()
+          | Ide_intf.Good false ->
               match Coq.interp mycoqtop false
                         (Printf.sprintf "Add LoadPath \"%s\". "  dir) with
-                | Ide_blob.Fail (l,str) ->
+                | Ide_intf.Fail (l,str) ->
                     self#set_message
                       ("Couln't add loadpath:\n"^str)
-                | Ide_blob.Good _ -> ()
+                | Ide_intf.Good _ -> ()
   end
 
   method electric_handler =
@@ -2260,9 +2260,9 @@ let main files =
                                        pop_info ();
                                        push_info
                                          (match Coq.current_status current.toplvl with
-                                            | Ide_blob.Fail (l,str) ->
+                                            | Ide_intf.Fail (l,str) ->
                                                 "Oops, problem while fetching coq status."
-                                            | Ide_blob.Good str -> str)
+                                            | Ide_intf.Good str -> str)
                                        )
                                     [session_notebook#current_term]
                                 in
@@ -2502,8 +2502,8 @@ let main files =
 let cur_ct = session_notebook#current_term.toplvl in
 					    try
                                               match Coq.make_cases cur_ct w with
-                                                | Ide_blob.Fail _ -> raise Not_found
-                                                | Ide_blob.Good cases ->
+                                                | Ide_intf.Fail _ -> raise Not_found
+                                                | Ide_intf.Good cases ->
                                                     let print c = function
                                                       | [x] -> Format.fprintf c "  | %s => _@\n" x
                                                       | x::l -> Format.fprintf c "  | (%s%a) => _@\n" x
diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index c84887d1a..701203061 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
-    | Ide_blob.Message msg ->
+    | Ide_intf.Message msg ->
         view#buffer#insert msg
-    | Ide_blob.Goals g ->
+    | Ide_intf.Goals g ->
         mode view g
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b85c00714..93476f4c4 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -319,7 +319,7 @@ let init arglist =
       if !ide_slave then begin
         Flags.make_silent true;
         Pfedit.set_undo (Some 5000);
-        Ide_blob.init_stdout ()
+        Ide_slave.init_stdout ()
       end;
       if_verbose print_header ();
       init_load_path ();
@@ -354,7 +354,7 @@ let init_toplevel = init
 let start () =
   init_toplevel (List.tl (Array.to_list Sys.argv));
   if !ide_slave then
-    Ide_blob.loop ()
+    Ide_slave.loop ()
   else
     Toplevel.loop();
   (* Initialise and launch the Ocaml toplevel *)
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
new file mode 100644
index 000000000..fb8c9e94d
--- /dev/null
+++ b/toplevel/ide_intf.ml
@@ -0,0 +1,84 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <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        *)
+(************************************************************************)
+
+(** * Interface of calls to Coq by CoqIde *)
+
+type 'a menu = 'a * (string * string) list
+
+type goals =
+  | Message of string
+  | Goals of ((string menu) list * string menu) list
+
+(** We use phantom types and GADT to protect ourselves against wild casts *)
+
+type 'a call =
+  | In_loadpath of string
+  | Raw_interp of string
+  | Interp of bool * string
+  | Rewind of int
+  | Read_stdout
+  | Cur_goals
+  | Cur_status
+  | Cases of string
+
+let is_in_loadpath s : bool call =
+  In_loadpath s
+
+let raw_interp s : unit call =
+  Raw_interp s
+
+let interp b s : int call =
+  Interp (b,s)
+
+let rewind i : int call =
+  Rewind i
+
+let read_stdout : string call =
+  Read_stdout
+
+let current_goals : goals call =
+  Cur_goals
+
+let current_status : string call =
+  Cur_status
+
+let make_cases s : string list list call =
+  Cases s
+
+(** * Coq answers to CoqIde *)
+
+type 'a value =
+  | Good of 'a
+  | Fail of (Util.loc option * string)
+
+type handler = {
+  is_in_loadpath : string -> bool;
+  raw_interp : string -> unit;
+  interp : bool -> string -> int;
+  rewind : int -> int;
+  read_stdout : unit -> string;
+  current_goals : unit -> goals;
+  current_status : unit -> string;
+  make_cases : 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)
+      | 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)
+    in Good res
+  with e ->
+    let (l,str) = explain_exn e in
+    Fail (l,str)
diff --git a/toplevel/ide_blob.mli b/toplevel/ide_intf.mli
index 34879f057..2550a30cd 100644
--- a/toplevel/ide_blob.mli
+++ b/toplevel/ide_intf.mli
@@ -6,8 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
+(** * Interface of calls to Coq by CoqIde *)
 
 type 'a menu = 'a * (string * string) list
 
@@ -15,32 +14,34 @@ type goals =
   | Message of string
   | Goals of ((string menu) list * string menu) list
 
-val reinit : unit -> unit
-
-val init_stdout : unit -> unit
-
 type 'a call
 
-type 'a value =
-  | Good of 'a
-  | Fail of (Util.loc option * string)
-
-val eval_call : 'a call -> 'a value
-
 val raw_interp : string -> unit call
-
 val interp : bool -> string -> int call
-
 val rewind : int -> int call
-
 val is_in_loadpath : string -> bool call
-
 val make_cases : string -> string list list call
-
 val current_status : string call
-
 val current_goals : goals call
-
 val read_stdout : string call
 
-val loop : unit -> unit
+(** * Coq answers to CoqIde *)
+
+type 'a value =
+  | Good of 'a
+  | Fail of (Util.loc option * string)
+
+type handler = {
+  is_in_loadpath : string -> bool;
+  raw_interp : string -> unit;
+  interp : bool -> string -> int;
+  rewind : int -> int;
+  read_stdout : unit -> string;
+  current_goals : unit -> goals;
+  current_status : unit -> string;
+  make_cases : string -> string list list;
+}
+
+val abstract_eval_call :
+  handler -> (exn -> Util.loc option * string) ->
+  'a call -> 'a value
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_slave.ml
index ff8dbb2d6..5a51471aa 100644
--- a/toplevel/ide_blob.ml
+++ b/toplevel/ide_slave.ml
@@ -6,13 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
-
-
-(* All this stuff should be integrated inside Coq. Several kittens died during
- * the operation. Reading this aloud will invoke the Great Cthulhu. *)
-
 open Vernacexpr
 open Names
 open Compat
@@ -102,10 +95,10 @@ let rec attribute_of_vernac_command = function
   | VernacAddMLPath _ -> []
   | VernacDeclareMLModule _ -> []
   | VernacChdir _ -> [OtherStatePreservingCommand]
-  
+
   (* State management *)
   | VernacWriteState _ -> []
-  | VernacRestoreState _ -> [] 
+  | VernacRestoreState _ -> []
 
   (* Resetting *)
   | VernacRemoveName _ -> [NavigationCommand]
@@ -113,7 +106,7 @@ let rec attribute_of_vernac_command = function
   | VernacResetInitial -> [NavigationCommand]
   | VernacBack _ -> [NavigationCommand]
   | VernacBackTo _ -> [NavigationCommand]
-  
+
   (* Commands *)
   | VernacDeclareTacticDefinition _ -> []
   | VernacCreateHintDb _ -> []
@@ -132,20 +125,20 @@ let rec attribute_of_vernac_command = function
   | 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]
@@ -154,7 +147,7 @@ let rec attribute_of_vernac_command = function
   | VernacUndo _ -> [NavigationCommand]
   | VernacUndoTo _ -> [NavigationCommand]
   | VernacBacktrack _ -> [NavigationCommand]
-  
+
   | VernacFocus _ -> [SolveCommand]
   | VernacUnfocus -> [SolveCommand]
   | VernacShow _ -> [OtherStatePreservingCommand]
@@ -165,14 +158,14 @@ let rec attribute_of_vernac_command = function
   | VernacProofMode _ -> []
   | VernacSubproof _ -> []
   | VernacEndSubproof -> []
-  
+
   (* Toplevel control *)
   | VernacToplevelControl _ -> []
-  
+
   (* Extensions *)
   | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand]
   | VernacExtend _ -> []
-  
+
 let is_vernac_navigation_command com =
   List.mem NavigationCommand (attribute_of_vernac_command com)
 
@@ -201,8 +194,6 @@ let is_vernac_tactic_command com =
 let is_vernac_proof_ending_command com =
   List.mem ProofEndingCommand (attribute_of_vernac_command com)
 
-(* End of Necronomicon exerpts *)
-
 type reset_status =
   | NoReset
   | ResetToNextMark
@@ -346,12 +337,6 @@ 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
@@ -401,14 +386,14 @@ let concl_next_tac sigma concl =
   ])
 
 let current_goals () =
-  try 
+  try
     let pfts =
       Proof_global.give_me_the_proof ()
     in
   let { Evd.it=all_goals ; sigma=sigma } = Proof.V82.subgoals pfts in
   if all_goals = [] then
     begin
-      Message (string_of_ppcmds (
+      Ide_intf.Message (string_of_ppcmds (
         let { Evd.it = bgoals ; sigma = sigma } = Proof.V82.background_subgoals pfts in
         match bgoals with
           | [] ->
@@ -437,9 +422,10 @@ let current_goals () =
           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)
+      Ide_intf.Goals (List.map process_goal all_goals)
     end
-  with Proof_global.NoCurrentProof -> Message "" (* quick hack to have a clean message screen *)
+  with Proof_global.NoCurrentProof ->
+    Ide_intf.Message "" (* quick hack to have a clean message screen *)
 
 let id_of_name = function
   | Names.Anonymous -> id_of_string "x"
@@ -515,77 +501,32 @@ let explain_exn e =
   in
   toploc,(Cerrors.explain_exn exc)
 
-
-(**
- * Wrappers around Coq calls. We use phantom types and GADT to protect ourselves
-  * against wild casts
-  *)
-
-type 'a call =
-  | In_loadpath of string
-  | Raw_interp of string
-  | Interp of bool * string
-  | Rewind of int
-  | Read_stdout
-  | Cur_goals
-  | Cur_status
-  | Cases of string
-
-type 'a value =
-  | Good of 'a
-  | Fail of (Util.loc option * string)
-
-let eval_call c = 
-  let filter_compat_exn = function
-    | Vernac.DuringCommandInterp (loc,inner) -> inner
+let eval_call c =
+  let rec handle_exn = function
+    | Vernac.DuringCommandInterp (loc,inner) -> handle_exn inner
+    | Vernacexpr.Drop -> None, "Drop is not allowed by coqide!"
     | Vernacexpr.Quit -> raise Vernacexpr.Quit
-    | e -> e
+    | e ->
+      let (l,pp) = explain_exn e in
+      l,string_of_ppcmds pp
   in
-  try Good (match c with
-              | In_loadpath s -> Obj.magic (is_in_loadpath s)
-              | Raw_interp s -> Obj.magic (raw_interp s)
-              | Interp (b,s) -> Obj.magic (interp b s)
-              | Rewind i -> Obj.magic (rewind i)
-              | Read_stdout -> Obj.magic (read_stdout ())
-              | Cur_goals -> Obj.magic (current_goals ())
-              | Cur_status -> Obj.magic (current_status ())
-              | Cases s -> Obj.magic (make_cases s))
-  with e ->
-    let (l,pp) = explain_exn (filter_compat_exn e) in
-    (* force evaluation of format stream *)
-    Fail (l,string_of_ppcmds pp)
-
-let is_in_loadpath s : bool call =
-  In_loadpath s
-
-let raw_interp s : unit call =
-  Raw_interp s
-
-let interp b s : int call =
-  Interp (b,s)
-
-let rewind i : int call =
-  Rewind i
-
-let read_stdout : string call =
-  Read_stdout
-
-let current_goals : goals call =
-  Cur_goals
-
-let current_status : string call =
-  Cur_status
-
-let make_cases s : string list list call =
-  Cases s
-
-(* End of wrappers *)
+  let handler = {
+    Ide_intf.is_in_loadpath = is_in_loadpath;
+    Ide_intf.raw_interp = raw_interp;
+    Ide_intf.interp = interp;
+    Ide_intf.rewind = rewind;
+    Ide_intf.read_stdout = read_stdout;
+    Ide_intf.current_goals = current_goals;
+    Ide_intf.current_status = current_status;
+    Ide_intf.make_cases = make_cases }
+  in
+  Ide_intf.abstract_eval_call handler handle_exn c
 
 let loop () =
   Sys.catch_break true;
   try
     while true do
-      let q = (Marshal.from_channel: in_channel -> 'a call) stdin in
+      let q = (Marshal.from_channel: in_channel -> 'a Ide_intf.call) stdin in
       let r = eval_call q in
       Marshal.to_channel !orig_stdout r [];
       flush !orig_stdout
diff --git a/toplevel/ide_slave.mli b/toplevel/ide_slave.mli
new file mode 100644
index 000000000..272616ae3
--- /dev/null
+++ b/toplevel/ide_slave.mli
@@ -0,0 +1,17 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <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        *)
+(************************************************************************)
+
+(** Specialize loop of Coqtop for interaction with CoqIde *)
+
+val reinit : unit -> unit
+
+val init_stdout : unit -> unit
+
+val eval_call : 'a Ide_intf.call -> 'a Ide_intf.value
+
+val loop : unit -> unit
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 7443edefd..8b03e9380 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -18,7 +18,8 @@ Mltop
 Vernacentries
 Whelp
 Vernac
-Ide_blob
+Ide_intf
+Ide_slave
 Toplevel
 Usage
 Coqinit