diff options
| -rw-r--r-- | ide/coq.ml | 35 | ||||
| -rw-r--r-- | ide/coq.mli | 11 | ||||
| -rw-r--r-- | ide/coqide.ml | 230 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 19 | ||||
| -rw-r--r-- | toplevel/toplevel.mli | 4 |
5 files changed, 103 insertions, 196 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index a567fb4f5..d75a996ef 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -407,6 +407,41 @@ let interp_and_replace s = let msg = read_stdout () in result,msg +type bktk_info = { start : GText.mark; + stop : GText.mark; + state_num : int; + pending_proofs : string list; + proof_stack_depth : int; +} + +let record_interp cmd_stk start_of_sentence end_of_sentence (sn,pp,psd) = + Stack.push { start = start_of_sentence; + stop = end_of_sentence; + state_num = sn; + pending_proofs = pp; + proof_stack_depth = psd; + } cmd_stk + +let backtrack cmd_stack stop_cond = + if Stack.is_empty cmd_stack then + reset_initial () (* reset coq *) + else try + let current = Stack.top cmd_stack in + while not (stop_cond (Stack.top cmd_stack).stop) do + ignore (Stack.pop cmd_stack) + done; + let target = Stack.top cmd_stack in + if current != target then + let rst = target.state_num in + let undo = target.proof_stack_depth in + let abrt = List.fold_left + (fun acc e -> if List.mem e target.pending_proofs then acc else succ acc) + 0 current.pending_proofs + in + raw_interp (Printf.sprintf "Backtrack %d %d %d.\n" rst undo abrt) + else () + with Stack.Empty -> reset_initial () (* might as well reset coq ... *) + type tried_tactic = | Interrupted | Success of int (* nb of goals after *) diff --git a/ide/coq.mli b/ide/coq.mli index c2f96a1fe..664005b61 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -29,6 +29,17 @@ type printing_state = { val printing_state : printing_state +type bktk_info = { start : GText.mark; + stop : GText.mark; + state_num : int; + pending_proofs : string list; + proof_stack_depth : int; +} + +val record_interp : bktk_info Stack.t -> GText.mark -> GText.mark -> (int * string list * int) -> unit + +val backtrack : bktk_info Stack.t -> (GText.mark -> bool) -> unit + type reset_mark type undo_info = identifier list * int diff --git a/ide/coqide.ml b/ide/coqide.ml index 4b08f4b9b..6f04d208e 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -18,13 +18,6 @@ open Ideutils open Coq_driver *) -type 'a info = {start:'a; - stop:'a; - ast:Util.loc * Vernacexpr.vernac_expr; - reset_info:Coq.reset_info -} - - class type analyzed_views= object('self) val mutable act_id : GtkSignal.id option @@ -37,7 +30,7 @@ object('self) val message_view : GText.view val proof_buffer : GText.buffer val proof_view : GText.view - val cmd_stack : GText.mark info Stack.t + val cmd_stack : bktk_info Stack.t val mutable is_active : bool val mutable read_only : bool val mutable filename : string option @@ -111,7 +104,7 @@ type viewable_script = proof_view : GText.view; message_view : GText.view; analyzed_view : analyzed_views; - command_stack : GText.mark info Stack.t; + command_stack : bktk_info Stack.t; } @@ -174,128 +167,6 @@ let on_active_view f = let cb = GData.clipboard Gdk.Atom.primary -(** Coq undoing mess ** - **********************) - -exception Size of int - -let update_on_end_of_segment cmd_stk id = - let lookup_section = function - | { reset_info = _,_,r } -> r := false - in - try Stack.iter lookup_section cmd_stk with Exit -> () - -let push_phrase cmd_stk 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 - } in - begin - match snd ast with - | VernacEndSegment (_,id) -> - prerr_endline "Updating on end of segment 1"; - update_on_end_of_segment cmd_stk id - | _ -> () - end; - Stack.push x cmd_stk - - -let repush_phrase cmd_stk reset_info x = - let x = { x with reset_info = reset_info } in - begin - match snd x.ast with - | VernacEndSegment (_,id) -> - prerr_endline "Updating on end of segment 2"; - update_on_end_of_segment cmd_stk id - | _ -> () - end; - Stack.push x cmd_stk - -type backtrack = -| BacktrackToNextActiveMark -| BacktrackToMark of reset_mark -| 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,ntacsteps)) (prev_lems,prev_ntacsteps) = - 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,prev_ntacsteps)) in - let undos = add_qed closedproofs (Util.iterate add_abort openproofs undos) in - Util.iterate add_undo (ntacsteps - prev_ntacsteps) undos - -let pop_command cmd_stk undos t = - let (state_info,undo_info,section_info) = t.reset_info in - let undos = - if !section_info then - let undos = update_proofs undos undo_info in - add_backtrack undos (BacktrackToMark state_info) - else - begin - prerr_endline "In section"; - (* An object inside a closed section *) - add_backtrack undos BacktrackToNextActiveMark - end in - ignore (Stack.pop cmd_stk); - undos - - -(* 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 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 - Coq.reset_initial () - else - begin - let t = Stack.top cmd_stk in - apply_undos cmd_stk (pop_command cmd_stk undos t); - let reset_info = Coq.compute_reset_info () in - interp_last t.ast; - repush_phrase cmd_stk reset_info t - end - - - let last_cb_content = ref "" @@ -1050,13 +921,13 @@ object(self) end; let start_of_phrase_mark = `MARK (b#create_mark start) in let end_of_phrase_mark = `MARK (b#create_mark stop) in - push_phrase - cmd_stack - reset_info - start_of_phrase_mark - end_of_phrase_mark ast; - if display_goals then self#show_goals; - remove_tag (start,stop) in + record_interp + cmd_stack + start_of_phrase_mark + end_of_phrase_mark + (Toplevel.current_status_triple ()); + if display_goals then self#show_goals; + remove_tag (start,stop) in begin match sync get_next_phrase () with None -> false @@ -1082,7 +953,11 @@ object(self) input_buffer#place_cursor stop; let start_of_phrase_mark = `MARK (input_buffer#create_mark start) in let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in - push_phrase cmd_stack reset_info start_of_phrase_mark end_of_phrase_mark ast; + record_interp + cmd_stack + start_of_phrase_mark + end_of_phrase_mark + (Toplevel.current_status_triple ()); self#show_goals; (*Auto insert save on success... try (match Coq.get_current_goals () with @@ -1173,51 +1048,32 @@ object(self) (* backtrack Coq to the phrase preceding iterator [i] *) 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 t = Stack.top cmd_stack in - if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then - begin - prerr_endline "Popped top command"; - pop_commands true (pop_command cmd_stack undos t) - end - else - done_smthg, undos - in - let undos = (0,0,NoBacktrack,0,undo_info()) 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 (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 + backtrack cmd_stack (fun b -> i#compare (input_buffer#get_iter_at_mark b) > 0); + sync (fun _ -> + let start = + if Stack.is_empty cmd_stack then input_buffer#start_iter + else input_buffer#get_iter_at_mark (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,11 +1113,11 @@ object(self) self#show_goals; self#clear_message in - let undo = pop_command cmd_stack (0,0,NoBacktrack,0,undo_info()) last_command in - apply_undos cmd_stack undo; + let curr_iter = input_buffer#get_iter_at_mark last_command.stop in + backtrack cmd_stack (fun b -> curr_iter#compare (input_buffer#get_iter_at_mark b) > 0); sync update_input () with - | Size 0 -> (* flash_info "Nothing to Undo"*)() + | Stack.Empty -> () ); pop_info (); Mutex.unlock coq_may_stop) diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index d14acaab9..c9f2a8772 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -224,6 +224,13 @@ let make_prompt () = "<"^l' *) +let current_status_triple () = + let statnum = Lib.current_command_label () in + let dpth = Pfedit.current_proof_depth () in + let pf_info = if 0 <= dpth then dpth else 0 in + let pending = List.map Names.string_of_id (Pfedit.get_all_proof_names ()) in + (statnum,pending,pf_info) + (* the coq prompt added to the default one when in emacs mode The prompt contains the current state label [n] (for global backtracking) and the current proof state [p] (for proof @@ -233,15 +240,9 @@ let make_prompt () = "n |lem1|lem2|lem3| p < " *) let make_emacs_prompt() = - let statnum = string_of_int (Lib.current_command_label ()) in - let dpth = Pfedit.current_proof_depth() in - let pending = Pfedit.get_all_proof_names() in - let pendingprompt = - List.fold_left - (fun acc x -> acc ^ (if acc <> "" then "|" else "") ^ Names.string_of_id x) - "" pending in - let proof_info = if dpth >= 0 then string_of_int dpth else "0" in - if !Flags.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " + let statnum,pending,proof_info = current_status_triple () in + let pendingprompt = String.concat "|" pending in + if !Flags.print_emacs then Printf.sprintf "%d |%s| %d < " statnum pendingprompt proof_info else "" (* A buffer to store the current command read on stdin. It is diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli index 3f2fa83ad..8204660f2 100644 --- a/toplevel/toplevel.mli +++ b/toplevel/toplevel.mli @@ -44,3 +44,7 @@ val do_vernac : unit -> unit (* Main entry point of Coq: read and execute vernac commands. *) val loop : unit -> unit + +(* hack to handle backtracking in CoqIde *) + +val current_status_triple : unit -> int * string list * int |