diff options
| author | Carst Tankink | 2014-09-30 11:03:12 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-10-01 18:08:51 +0200 |
| commit | 9a3abe5b18a84733c0c01c2647108196798a761c (patch) | |
| tree | fb14d51392aa666e31ba40a0db396f7dcfd6192c /ide | |
| parent | c73a59d9a6f124d5668054a16057d0955ca43cbd (diff) | |
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.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 15 | ||||
| -rw-r--r-- | ide/interface.mli | 11 | ||||
| -rw-r--r-- | ide/wg_ProofView.ml | 4 |
3 files changed, 4 insertions, 26 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index e99956738a..1df9d0fc39 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 43f728a1df..34f08663da 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 8c7aeeb8c6..62ebaf4d9c 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 () = |