diff options
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 24 |
1 files changed, 18 insertions, 6 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index fa6f8c37..565c9547 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pfedit.ml 6947 2005-04-20 16:18:41Z coq $ *) +(* $Id: pfedit.ml 9154 2006-09-20 17:18:18Z corbinea $ *) open Pp open Util @@ -150,6 +150,14 @@ let subtree_solved () = is_complete_proof (proof_of_pftreestate pts) & not (is_top_pftreestate pts) +let tree_solved () = + let pts = get_pftreestate () in + is_complete_proof (proof_of_pftreestate pts) + +let top_tree_solved () = + let pts = get_pftreestate () in + is_complete_proof (proof_of_pftreestate (top_of_tree pts)) + (*********************************************************************) (* Undo functions *) (*********************************************************************) @@ -243,7 +251,7 @@ let set_end_tac tac = (*********************************************************************) let start_proof na str sign concl hook = - let top_goal = mk_goal sign concl in + let top_goal = mk_goal sign concl None in let ts = { top_end_tac = None; top_goal = top_goal; @@ -253,7 +261,6 @@ let start_proof na str sign concl hook = start(na,ts); set_current_proof na - let solve_nth k tac = let pft = get_pftreestate () in if not (List.mem (-1) (cursor_of_pftreestate pft)) then @@ -309,7 +316,6 @@ let traverse_prev_unproven () = mutate prev_unproven let traverse_next_unproven () = mutate next_unproven - (* The goal focused on *) let focus_n = ref 0 let make_focus n = focus_n := n @@ -317,5 +323,11 @@ let focus () = !focus_n let focused_goal () = let n = !focus_n in if n=0 then 1 else n let reset_top_of_tree () = - let pts = get_pftreestate () in - if not (is_top_pftreestate pts) then mutate top_of_tree + mutate top_of_tree + +let reset_top_of_script () = + mutate (fun pts -> + try + up_until_matching_rule is_proof_instr pts + with Not_found -> top_of_tree pts) + |