summaryrefslogtreecommitdiff
path: root/proofs/pfedit.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/pfedit.ml')
-rw-r--r--proofs/pfedit.ml24
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)
+