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.

5 files changed, 46 insertions, 27 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index e99956738..1df9d0fc3 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -198,20 +198,7 @@ let goals () =
   if not (String.is_empty s) then msg_info (str s);
   try
     let pfts = Proof_global.give_me_the_proof () in
-    let (goals, zipper, shelf, given_up, sigma) = Proof.proof pfts in
-    let fg = List.map (process_goal sigma) goals in
-    let map_zip (lg, rg) =
-      let lg = List.map (process_goal sigma) lg in
-      let rg = List.map (process_goal sigma) rg in
-      (lg, rg)
-    in
-    let bg = List.map map_zip zipper in
-    let shelf = List.map (process_goal sigma) shelf in
-    let given_up = List.map (process_goal sigma) given_up in
-    Some { Interface.fg_goals = fg;
-           Interface.bg_goals = bg;
-           shelved_goals = shelf;
-           given_up_goals = given_up; }
+    Some (Proof.map_structured_proof pfts process_goal)
   with Proof_global.NoCurrentProof -> None
 
 let evars () =
diff --git a/ide/interface.mli b/ide/interface.mli
index 43f728a1d..34f08663d 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -39,16 +39,7 @@ type status = {
   (** An id describing the state of the current proof. *)
 }
 
-type goals = {
-  fg_goals : goal list;
-  (** List of the focussed goals *)
-  bg_goals : (goal list * goal list) list;
-  (** Zipper representing the unfocussed background goals *)
-  shelved_goals : goal list;
-  (** List of the goals on the shelf. *)
-  given_up_goals : goal list;
-  (** List of the goals that have been given up *)
-}
+type goals =  goal Proof.pre_goals
 
 type hint = (string * string) list
 (** A list of tactics applicable and their appearance *)
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 8c7aeeb8c..62ebaf4d9 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -129,7 +129,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
   match goals with
   | None -> ()
     (* No proof in progress *)
-  | Some { Interface.fg_goals = []; bg_goals = bg; shelved_goals; given_up_goals; } ->
+  | Some { Proof.fg_goals = []; bg_goals = bg; shelved_goals; given_up_goals; } ->
     let bg = flatten (List.rev bg) in
     let evars = match evars with None -> [] | Some evs -> evs in
     begin match (bg, shelved_goals,given_up_goals, evars) with
@@ -168,7 +168,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
       in
       List.iter iter bg
     end
-  | Some { Interface.fg_goals = fg } ->
+  | Some { Proof.fg_goals = fg } ->
     mode view fg hints
 
 let proof_view () =
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 067111d59..7d953d570 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -131,10 +131,36 @@ let proof p =
   let given_up = p.given_up in
   (goals,stack,shelf,given_up,sigma)
 
+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 *)
+}
+
+let map_structured_proof pfts process_goal: 'a pre_goals =
+  let (goals, zipper, shelf, given_up, sigma) = proof pfts in
+  let fg = List.map (process_goal sigma) goals in
+  let map_zip (lg, rg) =
+    let lg = List.map (process_goal sigma) lg in
+    let rg = List.map (process_goal sigma) rg in
+    (lg, rg)
+  in
+  let bg = List.map map_zip zipper in
+  let shelf = List.map (process_goal sigma) shelf in
+  let given_up = List.map (process_goal sigma) given_up in
+    { fg_goals = fg;
+      bg_goals = bg;
+      shelved_goals = shelf;
+      given_up_goals = given_up; }
+
 let rec unroll_focus pv = function
   | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
   | [] -> pv
-
 (* spiwack: a proof is considered completed even if its still focused, if the focus
    doesn't hide any goal.
    Unfocusing is handled in {!return}. *)
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