Separated the toplevel interface into a purely declarative module with associated types (interface.mli), and an applicative part processing the calls (previous ide_intf).

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

5 files changed, 77 insertions, 122 deletions

diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index 7a3afa7fbf..29594b140c 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -9,35 +9,12 @@
 (** * Interface of calls to Coq by CoqIde *)
 
 open Xml_parser
+open Interface
 
 type xml = Xml_parser.xml
 
-type 'a menu = 'a * (string * string) list
-
-type status = {
-  status_path : string option;
-  status_proofname : string option;
-}
-
-type goal = {
-  goal_hyp : string list;
-  goal_ccl : string;
-}
-
-type goals =
-  | No_current_proof
-  | Proof_completed
-  | Unfocused_goals of goal list
-  | Uninstantiated_evars of string list
-  | Goals of goal list
-
-type hint = (string * string) list
-
 (** We use phantom types and GADT to protect ourselves against wild casts *)
 
-type raw = bool
-type verbose = bool
-
 type 'a call =
   | Interp of raw * verbose * string
   | Rewind of int
@@ -57,23 +34,6 @@ let mkcases s : string list list call = MkCases s
 
 (** * Coq answers to CoqIde *)
 
-type location = (int * int) option (* start and end of the error *)
-
-type 'a value =
-  | Good of 'a
-  | Fail of (location * string)
-
-type handler = {
-  interp : raw * verbose * string -> string;
-  rewind : int -> int;
-  goals : unit -> goals;
-  hints : unit -> (hint list * hint) option;
-  status : unit -> status;
-  inloadpath : string -> bool;
-  mkcases : string -> string list list;
-  handle_exn : exn -> location * string;
-}
-
 let abstract_eval_call handler c =
   try
     let res = match c with
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index cdd86f7946..ada6ffe224 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.mli
@@ -6,34 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** * Interface of CoqIde calls to Coq *)
+(** * Applicative part of the interface of CoqIde calls to Coq *)
 
-type xml = Xml_parser.xml
-
-type goal = {
-  goal_hyp : string list;
-  goal_ccl : string;
-}
-
-type status = {
-  status_path : string option;
-  status_proofname : string option;
-}
+open Interface
 
-type goals =
-  | No_current_proof
-  | Proof_completed
-  | Unfocused_goals of goal list
-  | Uninstantiated_evars of string list
-  | Goals of goal list
-
-type hint = (string * string) list
+type xml = Xml_parser.xml
 
 type 'a call
 
-type raw = bool
-type verbose = bool
-
 (** Running a command (given as a string).
     - The 1st flag indicates whether to use "raw" mode
       (less sanity checks, no impact on the undo stack).
@@ -71,58 +51,18 @@ val inloadpath : string -> bool call
     followed by enough pattern variables. *)
 val mkcases : string -> string list list call
 
-
-(** * Coq answers to CoqIde *)
-
-type location = (int * int) option (* start and end of the error *)
-
-type 'a value =
-  | Good of 'a
-  | Fail of (location * string)
-
-(** * The structure that coqtop should implement *)
-
-type handler = {
-  interp : raw * verbose * string -> string;
-  rewind : int -> int;
-  goals : unit -> goals;
-  hints : unit -> (hint list * hint) option;
-  status : unit -> status;
-  inloadpath : string -> bool;
-  mkcases : string -> string list list;
-  handle_exn : exn -> location * string;
-}
-
 val abstract_eval_call : handler -> 'a call -> 'a value
 
 (** * XML data marshalling *)
 
 exception Marshal_error
 
-val of_bool : bool -> xml
-val to_bool : xml -> bool
-
-val of_string : string -> xml
-val to_string : xml -> string
-
-val of_int : int -> xml
-val to_int : xml -> int
-
-val of_pair : ('a -> xml) -> ('b -> xml) -> ('a * 'b) -> xml
-val to_pair : (xml -> 'a) -> (xml -> 'b) -> xml -> ('a * 'b)
-
-val of_list : ('a -> xml) -> 'a list -> xml
-val to_list : (xml -> 'a) -> xml -> 'a list
-
 val of_value : ('a -> xml) -> 'a value -> xml
 val to_value : (xml -> 'a) -> xml -> 'a value
 
 val of_call : 'a call -> xml
 val to_call : xml -> 'a call
 
-val of_goals : goals -> xml
-val to_goals : xml -> goals
-
 val of_answer : 'a call -> 'a value -> xml
 val to_answer : xml -> 'a value
 
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 60b89c2236..76cf15f798 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -14,7 +14,7 @@ open Pp
 open Printer
 open Namegen
 
-(** Ide_slave : an implementation of [Ide_intf], i.e. mainly an interp
+(** Ide_slave : an implementation of [Interface], i.e. mainly an interp
     function and a rewind function. This specialized loop is triggered
     when the -ideslave option is passed to Coqtop. Currently CoqIDE is
     the only one using this mode, but we try here to be as generic as
@@ -412,7 +412,7 @@ let process_goal sigma g =
 (*           (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
-  { Ide_intf.goal_hyp = hyps; Ide_intf.goal_ccl = ccl }
+  { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl }
 (*         hyps,(ccl,concl_next_tac sigma g)) *)
 
 let goals () =
@@ -426,15 +426,15 @@ let goals () =
       let { Evd.it = bgoals ; sigma = sigma } = Proof.V82.background_subgoals pfts in
       if bgoals = [] then
         let exl = Evarutil.non_instantiated sigma in
-        if exl = [] then Ide_intf.Proof_completed
+        if exl = [] then Interface.Proof_completed
         else
           let el = List.map (fun evar -> string_of_ppcmds (pr_evar evar)) exl in
-          Ide_intf.Uninstantiated_evars el
-      else Ide_intf.Unfocused_goals (List.map (process_goal sigma) bgoals)
+          Interface.Uninstantiated_evars el
+      else Interface.Unfocused_goals (List.map (process_goal sigma) bgoals)
     end
   else
-    Ide_intf.Goals (List.map (process_goal sigma) all_goals)
-  with Proof_global.NoCurrentProof -> Ide_intf.No_current_proof
+    Interface.Goals (List.map (process_goal sigma) all_goals)
+  with Proof_global.NoCurrentProof -> Interface.No_current_proof
 
 let hints () =
   try
@@ -470,7 +470,7 @@ let status () =
       Some (Names.string_of_id (Pfedit.get_current_proof_name ()))
     with _ -> None
   in
-  { Ide_intf.status_path = path; Ide_intf.status_proofname = proof }
+  { Interface.status_path = path; Interface.status_proofname = proof }
 
 (** Grouping all call handlers together + error handling *)
 
@@ -495,14 +495,14 @@ let eval_call c =
     r
   in
   let handler = {
-    Ide_intf.interp = interruptible interp;
-    Ide_intf.rewind = interruptible rewind;
-    Ide_intf.goals = interruptible goals;
-    Ide_intf.hints = interruptible hints;
-    Ide_intf.status = interruptible status;
-    Ide_intf.inloadpath = interruptible inloadpath;
-    Ide_intf.mkcases = interruptible Vernacentries.make_cases;
-    Ide_intf.handle_exn = handle_exn; }
+    Interface.interp = interruptible interp;
+    Interface.rewind = interruptible rewind;
+    Interface.goals = interruptible goals;
+    Interface.hints = interruptible hints;
+    Interface.status = interruptible status;
+    Interface.inloadpath = interruptible inloadpath;
+    Interface.mkcases = interruptible Vernacentries.make_cases;
+    Interface.handle_exn = handle_exn; }
   in
   (* If the messages of last command are still there, we remove them *)
   ignore (read_stdout ());
@@ -511,7 +511,7 @@ let eval_call c =
 
 (** The main loop *)
 
-(** Exceptions during eval_call should be converted into [Ide_intf.Fail]
+(** Exceptions during eval_call should be converted into [Interface.Fail]
     messages by [handle_exn] above. Otherwise, we die badly, after having
     tried to send a last message to the ide: trying to recover from errors
     with the current protocol would most probably bring desynchronisation
@@ -522,7 +522,7 @@ let pr_debug s =
   if !Flags.debug then Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s
 
 let fail err =
-  Ide_intf.of_value (fun _ -> assert false) (Ide_intf.Fail (None, err))
+  Ide_intf.of_value (fun _ -> assert false) (Interface.Fail (None, err))
 
 let loop () =
   let p = Xml_parser.make () in
diff --git a/toplevel/interface.mli b/toplevel/interface.mli
new file mode 100644
index 0000000000..b08365e7a5
--- /dev/null
+++ b/toplevel/interface.mli
@@ -0,0 +1,54 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** * Declarative part of the interface of CoqIde calls to Coq *)
+
+(** * Generic structures *)
+
+type raw = bool
+type verbose = bool
+
+type goal = {
+  goal_hyp : string list;
+  goal_ccl : string;
+}
+
+type status = {
+  status_path : string option;
+  status_proofname : string option;
+}
+
+type goals =
+  | No_current_proof
+  | Proof_completed
+  | Unfocused_goals of goal list
+  | Uninstantiated_evars of string list
+  | Goals of goal list
+
+type hint = (string * string) list
+
+(** * Coq answers to CoqIde *)
+
+type location = (int * int) option (* start and end of the error *)
+
+type 'a value =
+  | Good of 'a
+  | Fail of (location * string)
+
+(** * The structure that coqtop should implement *)
+
+type handler = {
+  interp : raw * verbose * string -> string;
+  rewind : int -> int;
+  goals : unit -> goals;
+  hints : unit -> (hint list * hint) option;
+  status : unit -> status;
+  inloadpath : string -> bool;
+  mkcases : string -> string list list;
+  handle_exn : exn -> location * string;
+}
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 8b03e93803..4df717e102 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -18,6 +18,7 @@ Mltop
 Vernacentries
 Whelp
 Vernac
+Interface
 Ide_intf
 Ide_slave
 Toplevel