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

5 files changed, 64 insertions, 110 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index a351107d91..70bc4d1cd1 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 89040aa5f7..41c9546d1f 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 c909a559ff..a96ed31c76 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 475b8f8a42..c7b231bf35 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 c84887d1aa..701203061f 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