From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 8 Aug 2008 13:18:42 +0200 Subject: Imported Upstream version 8.2~beta4+dfsg --- ide/coqide.ml | 114 ++++++++++++++++++++++++++++++++++------------------------ 1 file changed, 67 insertions(+), 47 deletions(-) (limited to 'ide/coqide.ml') diff --git a/ide/coqide.ml b/ide/coqide.ml index 12716197..07ee698f 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqide.ml 11126 2008-06-13 18:45:04Z herbelin $ *) +(* $Id: coqide.ml 11221 2008-07-11 23:28:25Z herbelin $ *) open Preferences open Vernacexpr @@ -543,8 +543,11 @@ type backtrack = | 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) = (n,a,b,p+q,l) +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 = @@ -580,38 +583,46 @@ let pop_command undos t = ignore (pop ()); undos -let rec apply_backtrack l = function - | 0, BacktrackToMark mark -> reset_to mark - | 0, NoBacktrack -> () - | 0, BacktrackToModSec id -> reset_to_mod id - | p, _ -> - (* re-synchronize Coq to the current state of the stack *) - if is_empty () then - Coq.reset_initial () - else - begin - let t = top () in - let undos = (0,0,BacktrackToNextActiveMark,p,l) in - let (_,_,b,p,l) = pop_command undos t in - apply_backtrack l (p,b); - let reset_info = Coq.compute_reset_info (snd t.ast) in - interp_last t.ast; - repush_phrase reset_info t - end - -let rec apply_undos (n,a,b,p,l) = - (* Aborts *) +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); - (* Undos *) - if n<>0 then + try Util.repeat a Pfedit.delete_current_proof () + with e -> prerr_endline "WARNING : found a closed environment"; raise e + +exception UndoStackExhausted + +let apply_tactic_undo n = + if n<>0 then (prerr_endline ("Applying "^string_of_int n^" undos"); - try Pfedit.undo n - with _ -> (* Undo stack exhausted *) - apply_backtrack l (p,BacktrackToNextActiveMark)); - (* Reset *) - apply_backtrack l (p,b) + try Pfedit.undo n with _ -> raise UndoStackExhausted) + +let apply_reset = function + | BacktrackToMark mark -> reset_to mark + | BacktrackToModSec id -> reset_to_mod id + | NoBacktrack -> () + | BacktrackToNextActiveMark -> assert false + +let rec apply_undos (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 (n,0,BacktrackToNextActiveMark,p,l) + end + else + (* re-synchronize Coq to the current state of the stack *) + if is_empty () then + Coq.reset_initial () + else + begin + let t = top () in + apply_undos (pop_command undos t); + let reset_info = Coq.compute_reset_info (snd t.ast) in + interp_last t.ast; + repush_phrase reset_info t + end (* For electric handlers *) exception Found @@ -3521,24 +3532,33 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); \n" in let initial_about (b:GText.buffer) = - (try - let image = lib_ide_file "coq.png" in - let startup_image = GdkPixbuf.from_file image in - b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image; - b#insert ~iter:b#start_iter "\t\t " - with _ -> ()); + let initial_string = "Welcome to CoqIDE, an Integrated Development Environment for Coq\n" in let coq_version = Coq.short_version () in - b#insert ~iter:b#start_iter "\n\n"; - if Glib.Utf8.validate coq_version then b#insert ~iter:b#start_iter coq_version; - b#insert ~iter:b#start_iter "\n " + b#insert ~iter:b#start_iter "\n\n"; + if Glib.Utf8.validate ("You are running " ^ coq_version) then b#insert ~iter:b#start_iter ("You are running " ^ coq_version); + if Glib.Utf8.validate initial_string then b#insert ~iter:b#start_iter initial_string; + (try + let image = lib_ide_file "coq.png" in + let startup_image = GdkPixbuf.from_file image in + b#insert ~iter:b#start_iter "\n\n"; + b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image; + b#insert ~iter:b#start_iter "\n\n\t\t " + with _ -> ()) in let about (b:GText.buffer) = - if Glib.Utf8.validate about_full_string - then b#insert about_full_string; - let coq_version = Coq.version () in - if Glib.Utf8.validate coq_version - then b#insert coq_version + (try + let image = lib_ide_file "coq.png" in + let startup_image = GdkPixbuf.from_file image in + b#insert ~iter:b#start_iter "\n\n"; + b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image; + b#insert ~iter:b#start_iter "\n\n\t\t " + with _ -> ()); + if Glib.Utf8.validate about_full_string + then b#insert about_full_string; + let coq_version = Coq.version () in + if Glib.Utf8.validate coq_version + then b#insert coq_version in initial_about tv2#buffer; -- cgit v1.2.3