From 9a3abe5b18a84733c0c01c2647108196798a761c Mon Sep 17 00:00:00 2001 From: Carst Tankink Date: Tue, 30 Sep 2014 11:03:12 +0200 Subject: 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. --- proofs/proof.mli | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'proofs/proof.mli') 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 -- cgit v1.2.3