From 19b041bcc069e79608392d705fa9998440d50815 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 10 May 2008 15:27:38 +0000 Subject: Amélioration de la colorisation, du backtrack et des messages de CoqIDE MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Colorisation: - on ne colorie que les noms de commandes que si en début de phrase (par exemple: Definition F := fun Local => Local) ne colorie pas Local), - ajout de motifs plus sophistiqué, (par exemple, tous les Set/Unset sont uniformément mis en valeur). - Backtracking: résolution bug #1538 et réactivation de la possibilité de déclarer des défs, types, etc pendant une session de preuve. En revanche, il n'est pas clair que cela fonctionne bien avec le mode déclaratif. - Messages d'erreur : on ne capture la sortie de coq qu'après l'initialisation pour que les erreurs d'initialisation soit affichées (cf bug #1424 and item 5 of #1123). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10915 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coqide.ml | 58 +++++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 37 insertions(+), 21 deletions(-) (limited to 'ide/coqide.ml') diff --git a/ide/coqide.ml b/ide/coqide.ml index 29b55da6a..1e6892d0d 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -159,7 +159,7 @@ object('self) method activate : unit -> unit method active_keypress_handler : GdkEvent.Key.t -> bool method backtrack_to : GText.iter -> unit - method backtrack_to_no_lock : GText.iter -> unit + method backtrack_to_no_lock : GText.iter -> Names.identifier list -> unit method clear_message : unit method deactivate : unit -> unit method disconnected_keypress_handler : GdkEvent.Key.t -> bool @@ -1271,22 +1271,34 @@ object(self) self#clear_message)(); Coq.reset_initial () - (* backtrack Coq to the phrase preceding iterator [i] *) - method backtrack_to_no_lock i = + method backtrack_to_no_lock i oldest_id_to_reset = prerr_endline "Backtracking_to iter starts now."; + let was_refining = Pfedit.refining () in (* re-synchronize Coq to the current state of the stack *) - let rec synchro () = + let rec synchro oldest_decl_in_middle_of_proof = if is_empty () then Coq.reset_initial () else begin let t = pop () in begin match t.reset_info with - | ResetAtSegmentStart (id, ({contents=true} as v)) -> - v:=false; reset_to_mod id - | ResetAtDecl (id, ({contents=true} as v)) -> - v:=false; reset_to id - | _ -> synchro () + | ResetAtSegmentStart (id, {contents=true}) -> + reset_to_mod id + | ResetAtDecl (id, {contents=true}) -> + if was_refining then + (prerr_endline ("Skipping "^Names.string_of_id id); + synchro [id]) + else + reset_to (List.hd (oldest_decl_in_middle_of_proof@[id])) + | ResetAtDecl (id, {contents=false}) -> + if was_refining then + (*reset oldest decl found before theorem started, if any*) + List.iter reset_to oldest_decl_in_middle_of_proof + else + (prerr_endline ("Skipping "^Names.string_of_id id); + synchro [id]) + | _ -> + synchro oldest_decl_in_middle_of_proof end; interp_last t.ast; repush_phrase t @@ -1301,9 +1313,12 @@ object(self) else let t = top () in if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then begin + prerr_endline "Popped top command"; ignore (pop ()); - let undos = if is_tactic (snd t.ast) then add_undo undos else None in - pop_commands true undos + let undos = + if is_vernac_tactic_command (snd t.ast) then add_undo undos + else None in + pop_commands true undos end else done_smthg, undos in @@ -1313,8 +1328,8 @@ object(self) begin try (match undos with - | None -> synchro () - | Some n -> try Pfedit.undo n with _ -> synchro ()); + | None -> synchro oldest_id_to_reset + | Some n -> try Pfedit.undo n with _ -> synchro oldest_id_to_reset); sync (fun _ -> let start = if is_empty () then input_buffer#start_iter @@ -1342,7 +1357,8 @@ Please restart and report NOW."; method backtrack_to i = if Mutex.try_lock coq_may_stop then - (!push_info "Undoing...";self#backtrack_to_no_lock i ; Mutex.unlock coq_may_stop; + (!push_info "Undoing..."; + self#backtrack_to_no_lock i []; Mutex.unlock coq_may_stop; !pop_info ()) else prerr_endline "backtrack_to : discarded (lock is busy)" @@ -1381,7 +1397,7 @@ Please restart and report NOW."; | {ast=_, (VernacSolve _ | VernacTime (VernacSolve _))} -> begin try Pfedit.undo 1; ignore (pop ()); sync update_input () - with _ -> self#backtrack_to_no_lock start + with _ -> self#backtrack_to_no_lock start [] end | {reset_info=ResetAtSegmentStart (id, {contents=true})} -> @@ -1389,9 +1405,10 @@ Please restart and report NOW."; reset_to_mod id; sync update_input () | {reset_info=ResetAtDecl (id, {contents=true})} -> - ignore (pop ()); - reset_to id; - sync update_input () + if Pfedit.refining () then + self#backtrack_to_no_lock start [id] + else + (ignore (pop ()); sync update_input ()) | {reset_info=ResetAtDecl (id,{contents=false})} -> ignore (pop ()); (try @@ -1406,7 +1423,7 @@ Please restart and report NOW."; ignore (pop ()); sync update_input () | _ -> - self#backtrack_to_no_lock start + self#backtrack_to_no_lock start [] end; with | Size 0 -> (* !flash_info "Nothing to Undo"*)() @@ -3468,6 +3485,7 @@ let start () = else failwith ("Coqide internal error: " ^ msg))); Command_windows.main (); Blaster_window.main 9; + init_stdout (); main files; if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ()); while true do @@ -3480,5 +3498,3 @@ let start () = flush stderr; crash_save 127 done - - -- cgit v1.2.3