diff options
| -rw-r--r-- | ide/coq.ml | 25 | ||||
| -rw-r--r-- | ide/coq.mli | 5 | ||||
| -rw-r--r-- | ide/coqide.ml | 64 |
3 files changed, 47 insertions, 47 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index c81318711d..521e288cd8 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -350,6 +350,19 @@ let is_vernac_tactic_command com = let is_vernac_proof_ending_command com = List.mem ProofEndingCommand (attribute_of_vernac_command com) +type undo_info = int * int + +let open_proofs = ref [] + +let undo_info () = + let current = Pfedit.get_all_proof_names () in + let common = list_intersect current !open_proofs in + let ncommon = List.length common in + let more = List.length current - ncommon in + let less = List.length !open_proofs - ncommon in + open_proofs := current; + (more,less) + type reset_mark = | ResetToId of Names.identifier | ResetToState of Libnames.object_name @@ -357,13 +370,14 @@ type reset_mark = type reset_status = | NoReset | ResetAtSegmentStart of Names.identifier - | ResetAtStatement of Libnames.object_name option | ResetAtRegisteredObject of reset_mark type reset_info = reset_status * bool ref let reset_mark id = match Lib.has_top_frozen_state () with - | Some sp -> ResetToState sp + | Some sp -> + prerr_endline ("On top of state "^Libnames.string_of_path (fst sp)); + ResetToState sp | None -> ResetToId id let compute_reset_info = function @@ -381,13 +395,12 @@ let compute_reset_info = function | com when is_vernac_proof_ending_command com -> NoReset, ref true | VernacEndSegment _ -> NoReset, ref true - | com when is_vernac_goal_starting_command com -> - ResetAtStatement (Lib.has_top_frozen_state ()), ref false - | com when is_vernac_tactic_command com -> NoReset, ref true | _ -> (match Lib.has_top_frozen_state () with - | Some sp -> ResetAtRegisteredObject (ResetToState sp) + | Some sp -> + prerr_endline ("On top of state "^Libnames.string_of_path (fst sp)); + ResetAtRegisteredObject (ResetToState sp) | None -> NoReset), ref true let reset_initial () = diff --git a/ide/coq.mli b/ide/coq.mli index 9c95ec0595..6208fba373 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -35,9 +35,12 @@ type reset_mark = type reset_status = | NoReset | ResetAtSegmentStart of Names.identifier - | ResetAtStatement of Libnames.object_name option | ResetAtRegisteredObject of reset_mark +type undo_info = int * int + +val undo_info : unit -> undo_info + type reset_info = reset_status * bool ref val compute_reset_info : Vernacexpr.vernac_expr -> reset_info diff --git a/ide/coqide.ml b/ide/coqide.ml index a519f23979..4488cef045 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -491,6 +491,7 @@ type info = {start:GText.mark; stop:GText.mark; ast:Util.loc * Vernacexpr.vernac_expr; reset_info:Coq.reset_info; + undo_info:Coq.undo_info; } exception Size of int @@ -502,18 +503,6 @@ let is_empty () = Stack.is_empty processed_stack (* push a new Coq phrase *) -let update_on_end_of_proof () = - let lookup_lemma = function - | { reset_info = ResetAtRegisteredObject _, r } -> - prerr_endline "Toggling Frozen State info to false"; - r := false - | { reset_info = ResetAtStatement _, r } -> - prerr_endline "Toggling Reset info to true"; - r := true; raise Exit - | _ -> () - in - try Stack.iter lookup_lemma processed_stack with Exit -> () - let update_on_end_of_segment id = let lookup_section = function | { reset_info = ResetAtSegmentStart id', _ } when id = id' -> raise Exit @@ -525,11 +514,11 @@ let push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast = let x = {start = start_of_phrase_mark; stop = end_of_phrase_mark; ast = ast; - reset_info = reset_info + reset_info = reset_info; + undo_info = Coq.undo_info () } in begin match snd ast with - | com when is_vernac_proof_ending_command com -> update_on_end_of_proof () | VernacEndSegment (_,id) -> update_on_end_of_segment id | _ -> () end; @@ -537,10 +526,9 @@ let push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast = let repush_phrase reset_info x = - let x = { x with reset_info = reset_info } in + let x = { x with reset_info = reset_info; undo_info = Coq.undo_info () } in begin match snd x.ast with - | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof () | VernacEndSegment (_,id) -> update_on_end_of_segment id | _ -> () end; @@ -554,34 +542,30 @@ type backtrack = let add_undo = function (n,a,b,p as x) -> if p = 0 then (n+1,a,b,p) else x let add_abort = function (n,a,b,0) -> (0,a+1,b,0) | (n,a,b,p) -> (n,a,b,p-1) -let add_qed (n,a,b,p) = (n,a,b,p+1) +let add_qed q (n,a,b,p) = (n,a,b,p+q) let add_backtrack (n,a,b,p) b' = (n,a,b',p) -let add_proof_start (n,a,b,p) b' = (n,a,b',p-1) let pop_command undos t = let undos = - match t with - | {reset_info=ResetAtStatement _,{contents=false}} when Pfedit.refining()-> - (* An incomplete ongoing proof *) - add_abort undos - | {reset_info=_, {contents=false}} -> - (* An object inside a section *) - add_backtrack undos BacktrackToNextActiveMark - | {ast=(_,com)} when is_vernac_tactic_command com -> - (* A tactic, active if not below a Qed *) - add_undo undos - | {ast=(_,com)} when is_vernac_proof_ending_command com -> - (* Backtracking a Qed *) - add_qed undos - | {ast=(_,com)} when is_vernac_state_preserving_command com -> undos - | {reset_info=ResetAtRegisteredObject mark, _} -> - add_backtrack undos (BacktrackToMark mark) - | {reset_info=ResetAtSegmentStart id, _} -> - add_backtrack undos (BacktrackToModSec id) - | {reset_info=ResetAtStatement (Some st), _} -> - add_proof_start undos (BacktrackToMark (ResetToState st)) - | {ast=(_,com)} -> - add_backtrack undos BacktrackToNextActiveMark in + if !(snd t.reset_info) then + let (openproofs,closedproofs) = t.undo_info in + let undos = Util.iterate add_abort openproofs undos in + let undos = add_qed closedproofs undos in + match fst t.reset_info with + | _ when is_vernac_tactic_command (snd t.ast) -> + (* A tactic, active if not below a Qed *) + add_undo undos + | ResetAtRegisteredObject mark -> + add_backtrack undos (BacktrackToMark mark) + | ResetAtSegmentStart id -> + add_backtrack undos (BacktrackToModSec id) + | _ when is_vernac_state_preserving_command (snd t.ast) -> + undos + | _ -> + add_backtrack undos BacktrackToNextActiveMark + else + (* An object inside a closed section *) + add_backtrack undos BacktrackToNextActiveMark in ignore (pop ()); undos |