diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 220 | ||||
| -rw-r--r-- | ide/coq.mli | 5 | ||||
| -rw-r--r-- | ide/coqide.ml | 84 |
3 files changed, 152 insertions, 157 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index f27117c078..c2799931a2 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -305,6 +305,8 @@ type annotated_vernac = | PureVernac of vernac_expr +let comm_stack = Stack.create () + let parsable_of_string s = Pcoq.Gram.parsable (Stream.of_string s) @@ -332,123 +334,67 @@ type reset_info = { } let compute_reset_info loc_ast = - let status = match snd loc_ast with - | com when is_vernac_tactic_command com -> NoReset - | com when is_vernac_state_preserving_command com -> NoReset - | com when is_vernac_proof_ending_command com -> NoReset - | VernacEndSegment _ -> NoReset + let status,_ = match snd loc_ast with + | com when is_vernac_tactic_command com -> + NoReset,None (*Some (Pfedit.get_current_proof_name (),Pfedit.current_proof_depth ()) *) + | com when is_vernac_state_preserving_command com -> NoReset,None + | com when is_vernac_proof_ending_command com -> NoReset,None + | VernacEndSegment _ -> NoReset,None | _ -> (match Lib.has_top_frozen_state () with | Some sp -> prerr_endline ("On top of state "^Libnames.string_of_path (fst sp)); - ResetAtMark sp - | None -> NoReset) + ResetAtMark sp,None + | None -> NoReset,None) in { status = status; proofs = Pfedit.get_all_proof_names (); loc_ast = loc_ast; } -let push_phrase cmd_stk reset_info ide_payload = - Stack.push (ide_payload,reset_info) cmd_stk - -type backtrack = - | BacktrackToNextActiveMark - | BacktrackToMark of Libnames.object_name - | NoBacktrack - -type undo_cmds = int * int * backtrack * int * identifier list - -let init_undo_cmds u = - (0,0,NoBacktrack,0,undo_info u) - -let add_undo = function (n,a,b,p,l as x) -> if p = 0 then (n+1,a,b,p,l) else x -let add_abort = function - | (n,a,b,0,l) -> (0,a+1,b,0,l) - | (n,a,b,p,l) -> (n,a,b,p-1,l) -let add_qed q (n,a,b,p,l as x) = - if q = 0 then x else (n,a,BacktrackToNextActiveMark,p+q,l) -let add_backtrack (n,a,b,p,l) b' = (n,a,b',p,l) - -let update_proofs (n,a,b,p,cur_lems) prev_lems = - let ncommon = List.length (Util.list_intersect cur_lems prev_lems) in - let openproofs = List.length cur_lems - ncommon in - let closedproofs = List.length prev_lems - ncommon in - let undos = (n,a,b,p,prev_lems) in - add_qed closedproofs (Util.iterate add_abort openproofs undos) - let eval_expr cmd_stk loc_ast ide_payload = let rewind_info = compute_reset_info loc_ast in Vernac.eval_expr loc_ast; - Stack.push (ide_payload,rewind_info) cmd_stk + Stack.push (ide_payload,rewind_info) cmd_stk; + Stack.length cmd_stk let rewind cmd_stk count = - let undo_ops = Queue.create () in + let undo_ops = Hashtbl.create count in let current_proofs = undo_info () in let rec do_rewind count reset_op prev_proofs = if (count <= 0) && (reset_op <> NoReset) && - (Util.list_subtract prev_proofs current_proofs = []) then + (Util.list_subset prev_proofs current_proofs) then (* We backtracked at least what we wanted to, we have no proof to reopen, * and we don't need to find a reset mark *) - begin(* - apply_aborts (Util.list_subtract current_proofs prev_proofs); - apply_undos undo_ops; - apply_reset reset_op*)() + begin + List.iter + (fun id -> Pfedit.delete_proof (Util.dummy_loc,id)) + (Util.list_subtract current_proofs prev_proofs);(* + Hashtbl.iter + (fun id depth -> + Pfedit.resume_proof (Util.dummy_loc,id); + Pfedit.undo_todepth depth) + undo_ops; + match reset_op with + | NoReset -> () + | ResetToMark m -> Lib.reset_to_state sp + | ResetToNextMark -> assert false + *)() end else begin let ide,coq = Stack.pop cmd_stk in - if is_vernac_tactic_command (snd coq.loc_ast) then Queue.push () undo_ops; + if is_vernac_tactic_command (snd coq.loc_ast) then Hashtbl.add undo_ops () (); do_rewind (pred count) (if coq.status <> NoReset then coq.status else reset_op) coq.proofs; if count < 0 then begin (* we had to backtrack further to find a suitable anchor point, * replaying *) - eval_expr cmd_stk coq.loc_ast ide; + ignore (eval_expr cmd_stk coq.loc_ast ide); end end in do_rewind count NoReset current_proofs -let pop_command cmd_stk undos = - let (_,t) = Stack.top cmd_stk in - let (state_info,undo_info) = t.status,t.proofs in - let undos = update_proofs undos undo_info in - ignore (Stack.pop cmd_stk); - match state_info with - | _ when is_vernac_tactic_command (snd t.loc_ast) -> - (* A tactic, active if not * below a Qed *) - add_undo undos - | ResetAtMark mark -> - add_backtrack undos (BacktrackToMark mark) - | _ when is_vernac_state_preserving_command (snd t.loc_ast) -> - undos - | _ -> - add_backtrack undos BacktrackToNextActiveMark - -(* appelle Pfedit.delete_current_proof a fois -* * utiliser Vernacentries.vernac_abort a la place ? *) -let apply_aborts a = - if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts"); - try Util.repeat a Pfedit.delete_current_proof () - with e -> prerr_endline "WARNING : found a closed environment"; raise e - -exception UndoStackExhausted - -(* appelle Pfedit.undo n fois - * utiliser vernac_undo ? *) -let apply_tactic_undo n = - if n<>0 then - (prerr_endline ("Applying "^string_of_int n^" undos"); - try Pfedit.undo n with _ -> raise UndoStackExhausted) - - -let apply_reset = function - | BacktrackToMark mark -> reset_to mark - | NoBacktrack -> () - | BacktrackToNextActiveMark -> assert false - - - module PrintOpt = struct @@ -506,7 +452,7 @@ let interp_with_options verbosely s = Vernac.eval_expr (loc,vernac); Flags.make_silent true; prerr_endline ("...Done with interp of : "^s); - reset_info + reset_info(* ,Stack.length comm_stack *) with Vernac.End_of_input -> assert false let interp verbosely phrase = @@ -556,28 +502,92 @@ let interp_last last = let s,_ = process_exn e in prerr_endline ("Replay during undo failed because: "^s); raise e -let rec apply_undos cmd_stk (n,a,b,p,l as undos) = - if p = 0 & b <> BacktrackToNextActiveMark then - begin - apply_aborts a; - try - apply_tactic_undo n; - apply_reset b - with UndoStackExhausted -> - apply_undos cmd_stk (n,0,BacktrackToNextActiveMark,p,l) - end - else - (* re-synchronize Coq to the current state of the stack *) - if Stack.is_empty cmd_stk then - reset_initial () - else +let push_phrase cmd_stk reset_info ide_payload = + Stack.push (ide_payload,reset_info) cmd_stk + +type backtrack = + | BacktrackToNextActiveMark + | BacktrackToMark of Libnames.object_name + | NoBacktrack + +let add_undo = function (n,a,b,p,l as x) -> if p = 0 then (n+1,a,b,p,l) else x +let add_abort = function + | (n,a,b,0,l) -> (0,a+1,b,0,l) + | (n,a,b,p,l) -> (n,a,b,p-1,l) +let add_qed q (n,a,b,p,l as x) = + if q = 0 then x else (n,a,BacktrackToNextActiveMark,p+q,l) +let add_backtrack (n,a,b,p,l) b' = (n,a,b',p,l) + +let update_proofs (n,a,b,p,cur_lems) prev_lems = + let ncommon = List.length (Util.list_intersect cur_lems prev_lems) in + let openproofs = List.length cur_lems - ncommon in + let closedproofs = List.length prev_lems - ncommon in + let undos = (n,a,b,p,prev_lems) in + add_qed closedproofs (Util.iterate add_abort openproofs undos) + +let pop_command cmd_stk undos = + let (_,t) = Stack.top cmd_stk in + let (state_info,undo_info) = t.status,t.proofs in + let undos = update_proofs undos undo_info in + ignore (Stack.pop cmd_stk); + match state_info with + | _ when is_vernac_tactic_command (snd t.loc_ast) -> + (* A tactic, active if not * below a Qed *) + add_undo undos + | ResetAtMark mark -> + add_backtrack undos (BacktrackToMark mark) + | _ when is_vernac_state_preserving_command (snd t.loc_ast) -> + undos + | _ -> + add_backtrack undos BacktrackToNextActiveMark + +(* appelle Pfedit.delete_current_proof a fois +* * utiliser Vernacentries.vernac_abort a la place ? *) +let apply_aborts a = + if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts"); + try Util.repeat a Pfedit.delete_current_proof () + with e -> prerr_endline "WARNING : found a closed environment"; raise e + +exception UndoStackExhausted + +(* appelle Pfedit.undo n fois + * utiliser vernac_undo ? *) +let apply_tactic_undo n = + if n<>0 then + (prerr_endline ("Applying "^string_of_int n^" undos"); + try Pfedit.undo n with _ -> raise UndoStackExhausted) + + +let apply_reset = function + | BacktrackToMark mark -> reset_to mark + | NoBacktrack -> () + | BacktrackToNextActiveMark -> assert false + +let old_rewind count cmd_stk = + let rec do_rewind count n_undo n_abort reset_op n_closed prev_proofs = + if (count <= 0) && (reset_op <> BacktrackToNextActiveMark) && (n_closed = 0) then begin - let (ide_ri,coq_ri) = Stack.top cmd_stk in - apply_undos cmd_stk (pop_command cmd_stk undos); - let reset_info = compute_reset_info coq_ri.loc_ast in - interp_last coq_ri.loc_ast; - push_phrase cmd_stk reset_info ide_ri + apply_aborts n_abort; + try + apply_tactic_undo n_undo; + apply_reset reset_op + with UndoStackExhausted -> + do_rewind 0 n_undo 0 BacktrackToNextActiveMark n_closed prev_proofs end + else + if Stack.is_empty cmd_stk then + reset_initial () + else + begin + let ide,coq = Stack.top cmd_stk in + let (n_undo,n_abort,reset_op,n_closed,prev_proofs) = + pop_command cmd_stk (n_undo,n_abort,reset_op,n_closed,prev_proofs) in + do_rewind (pred count) n_undo n_abort reset_op n_closed prev_proofs; + if count <= 0 then ignore (eval_expr cmd_stk coq.loc_ast ide); + end + in + do_rewind count 0 0 NoBacktrack 0 (undo_info ()); + type tried_tactic = | Interrupted diff --git a/ide/coq.mli b/ide/coq.mli index 27a0dfe45a..e863288cd1 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -54,10 +54,7 @@ val interp_and_replace : string -> val push_phrase : ('a * reset_info) Stack.t -> reset_info -> 'a -> unit -type undo_cmds -val init_undo_cmds : unit -> undo_cmds -val pop_command : ('a * reset_info) Stack.t -> undo_cmds -> undo_cmds -val apply_undos : ('a * reset_info) Stack.t -> undo_cmds -> unit +val old_rewind : int -> ('a * reset_info) Stack.t -> unit val is_vernac_tactic_command : Vernacexpr.vernac_expr -> bool val is_vernac_state_preserving_command : Vernacexpr.vernac_expr -> bool diff --git a/ide/coqide.ml b/ide/coqide.ml index 2055053a8d..fafc28b067 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -104,7 +104,6 @@ type viewable_script = proof_view : GText.view; message_view : GText.view; analyzed_view : analyzed_views; - command_stack : (ide_info * Coq.reset_info) Stack.t; } @@ -1174,50 +1173,41 @@ object(self) method backtrack_to_no_lock i = prerr_endline "Backtracking_to iter starts now."; (* pop Coq commands until we reach iterator [i] *) - let rec pop_commands done_smthg undos = - if Stack.is_empty cmd_stack then - done_smthg, undos - else - let (ide_ri,_) = Stack.top cmd_stack in - if i#compare (input_buffer#get_iter_at_mark ide_ri.stop) < 0 then - begin - prerr_endline "Popped top command"; - pop_commands true (pop_command cmd_stack undos) - end - else - done_smthg, undos + let itstk = Stack.copy cmd_stack in + let rec n_step n = + if Stack.is_empty itstk then n else + let ide_ri,_ = Stack.pop itstk in + if i#compare (input_buffer#get_iter_at_mark ide_ri.stop) < 0 then + n_step (succ n) + else + n in - let undos = init_undo_cmds () in - let done_smthg, undos = pop_commands false undos in - prerr_endline "Popped commands"; - if done_smthg then - begin - try - apply_undos cmd_stack undos; - sync (fun _ -> - let start = - if Stack.is_empty cmd_stack then input_buffer#start_iter - else input_buffer#get_iter_at_mark (fst (Stack.top cmd_stack)).stop in - prerr_endline "Removing (long) processed tag..."; - input_buffer#remove_tag - Tags.Script.processed - ~start - ~stop:self#get_start_of_input; - input_buffer#remove_tag - Tags.Script.unjustified - ~start - ~stop:self#get_start_of_input; - prerr_endline "Moving (long) start_of_input..."; - input_buffer#move_mark ~where:start (`NAME "start_of_input"); - self#show_goals; - clear_stdout (); - self#clear_message) - (); - with _ -> - push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state. - Please restart and report NOW."; - end - else prerr_endline "backtrack_to : discarded (...)" + begin + try + old_rewind (n_step 0) cmd_stack; + sync (fun _ -> + let start = + if Stack.is_empty cmd_stack then input_buffer#start_iter + else input_buffer#get_iter_at_mark (fst (Stack.top cmd_stack)).stop in + prerr_endline "Removing (long) processed tag..."; + input_buffer#remove_tag + Tags.Script.processed + ~start + ~stop:self#get_start_of_input; + input_buffer#remove_tag + Tags.Script.unjustified + ~start + ~stop:self#get_start_of_input; + prerr_endline "Moving (long) start_of_input..."; + input_buffer#move_mark ~where:start (`NAME "start_of_input"); + self#show_goals; + clear_stdout (); + self#clear_message) + (); + with _ -> + push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state. + Please restart and report NOW."; + end method backtrack_to i = if Mutex.try_lock coq_may_stop then @@ -1257,9 +1247,8 @@ object(self) self#show_goals; self#clear_message in - let undo = pop_command cmd_stack (init_undo_cmds ()) in - apply_undos cmd_stack undo; - sync update_input () + old_rewind 1 cmd_stack; + sync update_input () with | Stack.Empty -> (* flash_info "Nothing to Undo"*)() ); @@ -1591,7 +1580,6 @@ let create_session () = proof_view=proof; message_view=message; analyzed_view=legacy_av; - command_stack=stack; encoding="" } |