diff options
-rw-r--r-- | ide/coq.ml | 135 | ||||
-rw-r--r-- | ide/coq.mli | 37 | ||||
-rw-r--r-- | ide/coqide.ml | 114 | ||||
-rw-r--r-- | ide/gtk_parsing.ml | 67 |
4 files changed, 242 insertions, 111 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 6018cc07e..ea3400f2e 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -323,6 +323,9 @@ let rec attribute_of_vernac_command = function | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand] | VernacExtend _ -> [] +let is_vernac_goal_starting_command com = + List.mem GoalStartingCommand (attribute_of_vernac_command com) + let is_vernac_navigation_command com = List.mem NavigationCommand (attribute_of_vernac_command com) @@ -340,49 +343,74 @@ let is_vernac_goal_printing_command com = List.mem GoalStartingCommand attribute or List.mem SolveCommand attribute -type reset_mark = Libnames.object_name +let is_vernac_state_preserving_command com = + let attribute = attribute_of_vernac_command com in + List.mem OtherStatePreservingCommand attribute or + List.mem QueryCommand attribute -type reset_info = { - state : reset_mark; - pending : identifier list; - pf_depth : int; - mutable segment : bool; -} +let is_vernac_tactic_command com = + List.mem SolveCommand (attribute_of_vernac_command com) -let compute_reset_info () = - match Lib.has_top_frozen_state () with - | Some st -> - { state = st; - pending = Pfedit.get_all_proof_names (); - pf_depth = Pfedit.current_proof_depth (); - segment = true; } - | None -> - failwith "FATAL ERROR: NO RESET" - -type backtrack = - | BacktrackToNextActiveMark - | BacktrackToMark of reset_mark - | NoBacktrack - -type undo_cmds = { - n : int; - a : int; - b : backtrack; - p : int; - l : (identifier list * int); -} +let is_vernac_proof_ending_command com = + List.mem ProofEndingCommand (attribute_of_vernac_command com) + +type undo_info = identifier list + +let undo_info () = Pfedit.get_all_proof_names () + +type reset_mark = + | ResetToId of Names.identifier (* Relying on identifiers only *) + | ResetToState of Libnames.object_name (* Relying on states if any *) + +type reset_status = + | NoReset + | ResetAtSegmentStart of Names.identifier + | ResetAtRegisteredObject of reset_mark + +type reset_info = reset_status * undo_info * bool ref -let init_undo u = - { n = 0; a = 0; b = NoBacktrack; p = 0; - l = (Pfedit.get_all_proof_names u,Pfedit.current_proof_depth u) } + +let reset_mark id = match Lib.has_top_frozen_state () with + | Some sp -> + prerr_endline ("On top of state "^Libnames.string_of_path (fst sp)); + ResetToState sp + | None -> ResetToId id + +let compute_reset_info = function + | VernacBeginSection id + | VernacDefineModule (_,id, _, _, _) + | VernacDeclareModule (_,id, _, _) + | VernacDeclareModuleType (id, _, _, _) -> + ResetAtSegmentStart (snd id), undo_info(), ref true + + | VernacDefinition (_, (_,id), DefineBody _, _) + | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_) + | VernacInductive (_,_, (((_,(_,id)),_,_,_,_),_) :: _) -> + ResetAtRegisteredObject (reset_mark id), undo_info(), ref true + + | com when is_vernac_proof_ending_command com -> NoReset, undo_info(), ref true + | VernacEndSegment _ -> NoReset, undo_info(), ref true + + | com when is_vernac_tactic_command com -> NoReset, undo_info(), ref true + | _ -> + (match Lib.has_top_frozen_state () with + | Some sp -> + prerr_endline ("On top of state "^Libnames.string_of_path (fst sp)); + ResetAtRegisteredObject (ResetToState sp) + | None -> NoReset), undo_info(), ref true let reset_initial () = prerr_endline "Reset initial called"; flush stderr; Vernacentries.abort_refine Lib.reset_initial () -let reset_to st = - prerr_endline ("Reset called with state "^(Libnames.string_of_path (fst st))); - Lib.reset_to_state st +let reset_to = function + | ResetToId id -> + prerr_endline ("Reset called with "^(string_of_id id)); + Lib.reset_name (Util.dummy_loc,id) + | ResetToState sp -> + prerr_endline + ("Reset called with state "^(Libnames.string_of_path (fst sp))); + Lib.reset_to_state sp let reset_to_mod id = prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id)); @@ -414,7 +442,7 @@ let interp_with_options verbosely options s = if not (is_vernac_goal_printing_command vernac) then (* Verbose if in small step forward and not a tactic *) Flags.make_silent (not verbosely); - let reset_info = compute_reset_info () in + let reset_info = compute_reset_info vernac in List.iter (fun (set_option,_) -> raw_interp set_option) options; raw_interp s; Flags.make_silent true; @@ -430,6 +458,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 a03528f81..3ded7b6bd 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -29,32 +29,22 @@ type printing_state = { val printing_state : printing_state -type reset_mark +type reset_mark = + | ResetToId of Names.identifier + | ResetToState of Libnames.object_name -type reset_info = { - state : reset_mark; - pending : identifier list; - pf_depth : int; - mutable segment : bool; -} - -val compute_reset_info : unit -> reset_info +type reset_status = + | NoReset + | ResetAtSegmentStart of Names.identifier + | ResetAtRegisteredObject of reset_mark -type backtrack = - | BacktrackToNextActiveMark - | BacktrackToMark of reset_mark - | NoBacktrack +type undo_info = identifier list -type undo_cmds = { - n : int; - a : int; - b : backtrack; - p : int; - l : (identifier list * int); -} +val undo_info : unit -> undo_info -val init_undo : unit -> undo_cmds +type reset_info = reset_status * undo_info * bool ref +val compute_reset_info : Vernacexpr.vernac_expr -> reset_info val reset_initial : unit -> unit val reset_to : reset_mark -> unit val reset_to_mod : identifier -> unit @@ -65,6 +55,11 @@ val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit val interp_and_replace : string -> (reset_info * (Util.loc * Vernacexpr.vernac_expr)) * string +val is_vernac_tactic_command : Vernacexpr.vernac_expr -> bool +val is_vernac_state_preserving_command : Vernacexpr.vernac_expr -> bool +val is_vernac_goal_starting_command : Vernacexpr.vernac_expr -> bool +val is_vernac_proof_ending_command : Vernacexpr.vernac_expr -> bool + (* type hyp = (identifier * constr option * constr) * string *) type hyp = env * evar_map * diff --git a/ide/coqide.ml b/ide/coqide.ml index dc1e89cf1..734bdccdc 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -172,12 +172,12 @@ let cb = GData.clipboard Gdk.Atom.primary exception Size of int -(* when pushing a segment end, all the previous sentences have their segment - * boolean turned to false, causing backtrack to such sentences to be a - * BackTrackToNextActiveMark *) -let update_on_end_of_segment cmd_stk = let lookup_section item = - item.reset_info.segment <- false in try Stack.iter lookup_section cmd_stk with - Exit -> () +let update_on_end_of_segment cmd_stk id = + let lookup_section = function + | { reset_info = ResetAtSegmentStart id',_,_ } when id = id' -> raise Exit + | { 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; @@ -187,9 +187,9 @@ let push_phrase cmd_stk reset_info start_of_phrase_mark end_of_phrase_mark ast = } in begin match snd ast with - | VernacEndSegment _ -> + | VernacEndSegment (_,id) -> prerr_endline "Updating on end of segment 1"; - update_on_end_of_segment cmd_stk + update_on_end_of_segment cmd_stk id | _ -> () end; Stack.push x cmd_stk @@ -199,59 +199,63 @@ let repush_phrase cmd_stk reset_info x = let x = { x with reset_info = reset_info } in begin match snd x.ast with - | VernacEndSegment _ -> + | VernacEndSegment (_,id) -> prerr_endline "Updating on end of segment 2"; - update_on_end_of_segment cmd_stk + update_on_end_of_segment cmd_stk id | _ -> () end; Stack.push x cmd_stk -(* called ($ntacsteps - $prev_ntacsteps) times *) -let add_undo x = - if x.p = 0 then { x with n = x.n + 1 } else x - -(* called $openproofs times *) -let add_abort x = - if x.p = 0 then (* *) - { x with n = 0; a = x.a + 1 } - else (* there was a closed proof between S+ and S0, and now there is an open proof between S0 and S- *) - { x with p = x.p - 1 } - -(* called at each update_proof call *) -let add_qed q x = - if q = 0 then (* no closed proofs *) - x - else (* closed proofs *) - { x with b = BacktrackToNextActiveMark; p = x.p + q } - -let add_backtrack x b' = - { x with b = b' } - -let update_proofs x (prev_lems,prev_ntacsteps) = - let (cur_lems,ntacsteps) = x.l in +type backtrack = +| BacktrackToNextActiveMark +| BacktrackToMark of reset_mark +| BacktrackToModSec of Names.identifier +| 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 = { x with l = (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 undos = (n,a,b,p,prev_lems) in + add_qed closedproofs (Util.iterate add_abort openproofs undos) let pop_command cmd_stk undos t = - let t = t.reset_info in - let (state_info,undo_info,section_info) = (t.state,(t.pending,t.pf_depth),t.segment) in + let (state_info,undo_info,section_info) = t.reset_info in let undos = - if section_info then (* segment ouvert, on saute directement au bon état *) + if !section_info then let undos = update_proofs undos undo_info in - add_backtrack undos (BacktrackToMark state_info) - else (* segment fermé, il faut sauter au debut du segment *) + match state_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 begin prerr_endline "In section"; - (* XXX - all the way to the bottom of the stack *) - add_backtrack undos BacktrackToNextActiveMark + (* 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 () @@ -259,6 +263,8 @@ let apply_aborts a = 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"); @@ -267,20 +273,19 @@ let apply_tactic_undo n = let apply_reset = function | BacktrackToMark mark -> reset_to mark + | BacktrackToModSec id -> reset_to_mod id | NoBacktrack -> () | BacktrackToNextActiveMark -> assert false -(* XXX - in its current form, it goes all the way to the bottom of the stack. *) -let rec apply_undos cmd_stk undos = - if undos.p = 0 & undos.b <> BacktrackToNextActiveMark then - (* pas de preuve fermée et dans un segment ouvert *) +let rec apply_undos cmd_stk (n,a,b,p,l as undos) = + if p = 0 & b <> BacktrackToNextActiveMark then begin - apply_aborts undos.a; + apply_aborts a; try - apply_tactic_undo undos.n; - apply_reset undos.b + apply_tactic_undo n; + apply_reset b with UndoStackExhausted -> - apply_undos cmd_stk { undos with a = 0; b = BacktrackToNextActiveMark } + apply_undos cmd_stk (n,0,BacktrackToNextActiveMark,p,l) end else (* re-synchronize Coq to the current state of the stack *) @@ -290,7 +295,7 @@ let rec apply_undos cmd_stk undos = 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 + let reset_info = Coq.compute_reset_info (snd t.ast) in interp_last t.ast; repush_phrase cmd_stk reset_info t end @@ -1305,7 +1310,7 @@ object(self) else done_smthg, undos in - let undos = Coq.init_undo () 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 @@ -1375,7 +1380,7 @@ object(self) self#show_goals; self#clear_message in - let undo = pop_command cmd_stack (Coq.init_undo ()) last_command in + let undo = pop_command cmd_stack (0,0,NoBacktrack,0,undo_info()) last_command in apply_undos cmd_stack undo; sync update_input () with @@ -1939,6 +1944,7 @@ let main files = input_buffer#place_cursor input_buffer#start_iter; prerr_endline ("Loading: switch to view "^ string_of_int index); session_notebook#goto_page index; + prerr_endline "Loading: highlight"; input_buffer#set_modified false; prerr_endline "Loading: clear undo"; session.script#clear_undo; diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index ffb8c8d59..e92a345e3 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -107,3 +107,70 @@ let rec complete_forward w (it:GText.iter) = else Some (stop,stop,ne) else complete_forward w stop + +let find_comment_end (start:GText.iter) = + let rec find_nested_comment (search_start:GText.iter) (search_end:GText.iter) (comment_end:GText.iter) = + match (search_start#forward_search ~limit:search_end "(*"),(comment_end#forward_search "*)") with + | None,_ -> comment_end + | Some _, None -> raise Not_found + | Some (_,next_search_start),Some (next_search_end,next_comment_end) -> + find_nested_comment next_search_start next_search_end next_comment_end + in + match start#forward_search "*)" with + | None -> raise Not_found + | Some (search_end,comment_end) -> find_nested_comment start search_end comment_end + + +let rec find_string_end (start:GText.iter) = + let dblquote = int_of_char '"' in + let rec escaped_dblquote c = + (c#char = dblquote) && not (escaped_dblquote c#backward_char) + in + match start#forward_search "\"" with + | None -> raise Not_found + | Some (stop,next_start) -> + if escaped_dblquote stop#backward_char + then find_string_end next_start + else next_start + + +let rec find_next_sentence (from:GText.iter) = + match (from#forward_search ".") with + | None -> raise Not_found + | Some (non_vernac_search_end,next_sentence) -> + match from#forward_search ~limit:non_vernac_search_end "(*",from#forward_search ~limit:non_vernac_search_end "\"" with + | None,None -> + if Glib.Unichar.isspace next_sentence#char || next_sentence#compare next_sentence#forward_char == 0 + then next_sentence else find_next_sentence next_sentence + | None,Some (_,string_search_start) -> find_next_sentence (find_string_end string_search_start) + | Some (_,comment_search_start),None -> find_next_sentence (find_comment_end comment_search_start) + | Some (_,comment_search_start),Some (_,string_search_start) -> + find_next_sentence ( + if comment_search_start#compare string_search_start < 0 + then find_comment_end comment_search_start + else find_string_end string_search_start) + + +let find_nearest_forward (cursor:GText.iter) targets = + let fold_targets acc target = + match cursor#forward_search target,acc with + | Some (t_start,_),Some nearest when (t_start#compare nearest < 0) -> Some t_start + | Some (t_start,_),None -> Some t_start + | _ -> acc + in + match List.fold_left fold_targets None targets with + | None -> raise Not_found + | Some nearest -> nearest + + +let find_nearest_backward (cursor:GText.iter) targets = + let fold_targets acc target = + match cursor#backward_search target,acc with + | Some (t_start,_),Some nearest when (t_start#compare nearest > 0) -> Some t_start + | Some (t_start,_),None -> Some t_start + | _ -> acc + in + match List.fold_left fold_targets None targets with + | None -> raise Not_found + | Some nearest -> nearest + |