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

1 files changed, 54 insertions, 0 deletions

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;
+}