Factored out IDE goal structure.

The more structured goal record type of CoqIDE is also useful for other
interfaces (in particular, for PIDE). To support this, the datatype was
factored out to the Proof module. In addition, the record gains a type
parameter, to allow interfaces to adapt the output to their needs.

To accommodate this type, the Proof module also gains the
map_structured_proof that takes a Proof.proof and a function on the
individual goals (in the context of an evar map) and produces a
structured goal based on the goal transformer.

1 files changed, 15 insertions, 0 deletions

diff --git a/proofs/proof.mli b/proofs/proof.mli
index ff1253e7c..85b508447 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -49,6 +49,21 @@ val proof : proof ->
   * Goal.goal list
   * Evd.evar_map
 
+(* Generic records structured like the return type of proof *)
+type 'a pre_goals = {
+  fg_goals : 'a list;
+  (** List of the focussed goals *)
+  bg_goals : ('a list * 'a list) list;
+  (** Zipper representing the unfocussed background goals *)
+  shelved_goals : 'a list;
+  (** List of the goals on the shelf. *)
+  given_up_goals : 'a list;
+  (** List of the goals that have been given up *)
+}
+
+val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals)
+
+
 (*** General proof functions ***)
 
 val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof