diff options
| -rw-r--r-- | ide/ide_slave.ml | 15 | ||||
| -rw-r--r-- | ide/interface.mli | 11 | ||||
| -rw-r--r-- | ide/wg_ProofView.ml | 4 | ||||
| -rw-r--r-- | proofs/proof.ml | 28 | ||||
| -rw-r--r-- | proofs/proof.mli | 15 |
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 |