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

6 files changed, 161 insertions, 117 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b85c00714f..93476f4c41 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 0000000000..fb8c9e94d3
--- /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 34879f0577..2550a30cd3 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 ff8dbb2d6e..5a51471aaf 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 0000000000..272616ae30
--- /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 7443edefdd..8b03e93803 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