Cleaned up a bit goal handling in Coqtop interface. Now we have two queries : goal description, with focused and unfocused goals, and list of currently declared evars.

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

1 files changed, 24 insertions, 7 deletions

diff --git a/toplevel/interface.mli b/toplevel/interface.mli
index f472929e2b..8aa6c9200d 100644
--- a/toplevel/interface.mli
+++ b/toplevel/interface.mli
@@ -13,24 +13,35 @@
 type raw = bool
 type verbose = bool
 
+(** The type of coqtop goals *)
 type goal = {
   goal_hyp : string list;
+  (** List of hypotheses *)
   goal_ccl : string;
+  (** Goal conclusion *)
+}
+
+type evar = {
+  evar_info : string;
+  (** A string describing an evar: type, number, environment *)
 }
 
 type status = {
   status_path : string option;
+  (** Module path of the current proof *)
   status_proofname : string option;
+  (** Current proof name. [None] if no proof is in progress *)
 }
 
-type goals =
-  | No_current_proof
-  | Proof_completed
-  | Unfocused_goals of goal list
-  | Uninstantiated_evars of string list
-  | Goals of goal list
+type goals = {
+  fg_goals : goal list;
+  (** List of the focussed goals *)
+  bg_goals : goal list;
+  (** List of the background goals *)
+}
 
 type hint = (string * string) list
+(** A list of tactics applicable and their appearance *)
 
 type option_name = Goptions.option_name
 
@@ -39,11 +50,16 @@ type option_value = Goptions.option_value =
   | IntValue    of int option
   | StringValue of string
 
+(** Summary of an option status *)
 type option_state = Goptions.option_state = {
   opt_sync  : bool;
+  (** Whether an option is synchronous *)
   opt_depr  : bool;
+  (** Wheter an option is deprecated *)
   opt_name  : string;
+  (** A short string that is displayed when using [Test] *)
   opt_value : option_value;
+  (** The current value of the option *)
 }
 
 (** * Coq answers to CoqIde *)
@@ -59,7 +75,8 @@ type 'a value =
 type handler = {
   interp : raw * verbose * string -> string;
   rewind : int -> int;
-  goals : unit -> goals;
+  goals : unit -> goals option;
+  evars : unit -> evar list option;
   hints : unit -> (hint list * hint) option;
   status : unit -> status;
   get_options : unit -> (option_name * option_state) list;