Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

4 files changed, 76 insertions, 56 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 5166fb21..c560f0db 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq.ml 11126 2008-06-13 18:45:04Z herbelin $ *)
+(* $Id: coq.ml 11238 2008-07-19 09:34:03Z herbelin $ *)
 
 open Vernac
 open Vernacexpr
@@ -44,6 +44,8 @@ let init () =
      messages *)
 (**)
   Flags.make_silent true;
+  (* don't set a too large undo stack because Edit.create allocates an array *)
+  Pfedit.set_undo (Some 5000);
 (**)
   Coqtop.init_ide ()
 
@@ -98,7 +100,7 @@ let is_in_loadpath dir =
 let is_in_coq_path f = 
   try 
   let base = Filename.chop_extension (Filename.basename f) in
-  let _ = Library.locate_qualified_library 
+  let _ = Library.locate_qualified_library false
 	    (Libnames.make_qualid Names.empty_dirpath 
 	       (Names.id_of_string base)) in
   prerr_endline (f ^ " is in coq path");
@@ -246,9 +248,9 @@ let rec attribute_of_vernac_command = function
   | VernacSolveExistential _ -> [SolveCommand]
 
   (* MMode *)
-  | VernacDeclProof -> []
-  | VernacReturn -> []
-  | VernacProofInstr _ -> []
+  | VernacDeclProof -> [SolveCommand]
+  | VernacReturn -> [SolveCommand]
+  | VernacProofInstr _ -> [SolveCommand]
 
   (* Auxiliary file and library management *)
   | VernacRequireFrom _ -> []
diff --git a/ide/coq.png b/ide/coq.png
index 6ad66dbd..06aac459 100644
--- a/ide/coq.png
+++ b/ide/coq.png
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;
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 444b2c2b..dba56a77 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: preferences.ml 11058 2008-06-06 08:21:03Z herbelin $ *)
+(* $Id: preferences.ml 11276 2008-07-28 00:28:34Z glondu $ *)
 
 open Configwin
 open Printf
@@ -507,12 +507,11 @@ let configure ?(apply=(fun () -> ())) () =
   in    
   let cmd_browse =
     let predefined = [
+      Coq_config.browser;
       "netscape -remote \"openURL(%s)\"";
       "mozilla -remote \"openURL(%s)\"";
-      "firefox -remote \"openURL(%s,new-tab)\" || firefox %s &";
       "firefox -remote \"openURL(%s,new-windows)\" || firefox %s &";
       "seamonkey -remote \"openURL(%s)\" || seamonkey %s &";
-      "C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s";
       "open -a Safari %s &"
     ] in
     combo 
@@ -585,4 +584,3 @@ let configure ?(apply=(fun () -> ())) () =
   match x with 
     | Return_apply | Return_ok -> save_pref ()
     | Return_cancel -> ()
-