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

6 files changed, 71 insertions, 34 deletions

diff --git a/ide/coq.ico b/ide/coq.ico
deleted file mode 100644
index b99f6399..00000000
--- a/ide/coq.ico
+++ /dev/null
diff --git a/ide/coq.ml b/ide/coq.ml
index c560f0db..e2649c82 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq.ml 11238 2008-07-19 09:34:03Z herbelin $ *)
+(* $Id: coq.ml 11826 2009-01-22 06:43:35Z notin $ *)
 
 open Vernac
 open Vernacexpr
@@ -58,7 +58,7 @@ let get_version_date () =
     then Coq_config.date
     else "<date not printable>" in
   try
-    let ch = open_in (Coq_config.coqtop^"/revision") in
+    let ch = open_in (Coq_config.coqsrc^"/revision") in
     let ver = input_line ch in
     let rev = input_line ch in
     (ver,rev)
@@ -79,7 +79,7 @@ let version () =
       ver date
       Coq_config.arch Sys.os_type
       (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
-    (if Mltop.get () = Mltop.Native then "native" else "bytecode") 
+    (if Mltop.is_native then "native" else "bytecode") 
     (if Coq_config.best="opt" then "native" else "bytecode") 
 
 let is_in_coq_lib dir = 
@@ -88,7 +88,7 @@ let is_in_coq_lib dir =
   List.exists 
     (fun s -> 
       let fdir =
-        Filename.concat Coq_config.coqlib (Filename.concat "theories" s) in
+        Filename.concat (Envars.coqlib ()) (Filename.concat "theories" s) in
       prerr_endline (" Comparing to: "^fdir);
       if is_same_file fdir then (prerr_endline " YES";true)
       else (prerr_endline"NO";false))
@@ -230,7 +230,6 @@ let rec attribute_of_vernac_command = function
   (* Gallina extensions *)
   | VernacBeginSection _ -> []
   | VernacEndSegment _ -> []
-  | VernacRecord _ -> []
   | VernacRequire _ -> []
   | VernacImport _ -> []
   | VernacCanonical _ -> []
@@ -238,7 +237,6 @@ let rec attribute_of_vernac_command = function
   | VernacIdentityCoercion _ -> []
 
   (* Type classes *)
-  | VernacClass _ -> []
   | VernacInstance _ -> []
   | VernacContext _ -> []
   | VernacDeclareInstance _ -> []
@@ -273,6 +271,7 @@ let rec attribute_of_vernac_command = function
 
   (* Commands *)
   | VernacDeclareTacticDefinition _ -> []
+  | VernacCreateHintDb _ -> []
   | VernacHints _ -> []
   | VernacSyntacticDefinition _ -> []
   | VernacDeclareImplicits _ -> []
@@ -386,7 +385,7 @@ let compute_reset_info = function
 
   | VernacDefinition (_, (_,id), DefineBody _, _)
   | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_)
-  | VernacInductive (_, (((_,id),_,_,_),_) :: _) ->
+  | VernacInductive (_, (((_,(_,id)),_,_,_,_),_) :: _) ->
       ResetAtRegisteredObject (reset_mark id), undo_info(), ref true
 
   | com when is_vernac_proof_ending_command com -> NoReset, undo_info(), ref true
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 07ee698f..ea2dfe4d 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqide.ml 11221 2008-07-11 23:28:25Z herbelin $ *)
+(* $Id: coqide.ml 11853 2009-01-23 18:40:58Z notin $ *)
 
 open Preferences
 open Vernacexpr
@@ -482,10 +482,11 @@ let input_channel b ic =
       Buffer.add_substring b buf 0 !len
     done
 
-let with_file name ~f =
-  let ic = open_in_gen [Open_rdonly;Open_creat] 0o644 name in
-    try f ic; close_in ic with exn -> 
-      close_in ic; !flash_info ("Error: "^Printexc.to_string exn)
+let with_file handler name ~f =
+  try
+    let ic = open_in_gen [Open_rdonly;Open_creat] 0o644 name in
+    try f ic; close_in ic with e -> close_in ic; raise e
+  with Sys_error s -> handler s
 
 type info =  {start:GText.mark;
 	      stop:GText.mark;
@@ -713,7 +714,7 @@ object(self)
 		try
 		  if is_active then self#reset_initial;
 		  let b = Buffer.create 1024 in
-		    with_file f ~f:(input_channel b);
+		    with_file !flash_info f ~f:(input_channel b);
 		    let s = try_convert (Buffer.contents b) in
 		      input_buffer#set_text s;
 		      self#update_stats;
@@ -1839,7 +1840,7 @@ let main files =
     ~title:"CoqIde" ()
   in
     (try
-	 let icon_image = lib_ide_file "coq.ico" in
+	 let icon_image = lib_ide_file "coq.png" in
 	 let icon = GdkPixbuf.from_file icon_image in
 	   w#set_icon (Some icon)
      with _ -> ());
@@ -1871,7 +1872,7 @@ let main files =
       let file_factory = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/File/" file_menu ~accel_group in
 
       (* File/Load Menu *)
-      let load f =
+      let load_file handler f =
 	let f = absolute_filename f in		
 	  try
 	    prerr_endline "Loading file starts";
@@ -1886,7 +1887,7 @@ let main files =
 	    prerr_endline "Loading: must open";
 	    let b = Buffer.create 1024 in
 	      prerr_endline "Loading: get raw content";
-	      with_file f ~f:(input_channel b);
+	      with_file handler f ~f:(input_channel b);
 	      prerr_endline "Loading: convert content";
 	      let s = do_convert (Buffer.contents b) in
 		prerr_endline "Loading: create view";
@@ -1922,8 +1923,9 @@ let main files =
 		      prerr_endline "Loading: success"
 	  with       
 	    | Vector.Found i -> set_current_view i
-	    | e -> !flash_info ("Load failed: "^(Printexc.to_string e))
+	    | e -> handler ("Load failed: "^(Printexc.to_string e))
       in
+      let load f = load_file !flash_info f in
       let load_m = file_factory#add_item "_New" 
 	~key:GdkKeysyms._N in
       let load_f () = 	  
@@ -2478,7 +2480,7 @@ let main files =
 				(fun () -> 	 
 				   let av = Option.get ((get_current_view()).analyzed_view) in 
 				     match av#filename with
-				       | None -> ()
+				       | None -> warning "Call to external editor available only on named files"
 				       | Some f ->
 					   save_f ();
 					   let com = Flags.subst_command_placeholder !current.cmd_editor (Filename.quote f) in
@@ -3632,9 +3634,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 								begin
 								  List.iter (fun f -> 
 									       if Sys.file_exists f then load f else 
-										 if Filename.check_suffix f ".v" 
-										 then load f 
-										 else load (f^".v")) files;
+                                                                                 let f = if Filename.check_suffix f ".v" then f else f^".v" in
+										 load_file (fun s -> print_endline s; exit 1) f)
+                                                                    files;
 								  activate_input 0
 								end
 							      else
diff --git a/ide/highlight.mll b/ide/highlight.mll
index 8cd55c97..f2ecaa9c 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: highlight.mll 11004 2008-05-28 09:09:12Z herbelin $ *)
+(* $Id: highlight.mll 11481 2008-10-20 19:23:51Z herbelin $ *)
 
 {
 
@@ -110,13 +110,16 @@ rule next_starting_order = parse
   | multiword_command
       { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, "kwd" }
   | ident as id 
-      { starting:=false; 
-        if is_one_word_command id then 
-	  lexeme_start lexbuf, lexeme_end lexbuf, "kwd" 
-	else if is_one_word_declaration id then
-	  lexeme_start lexbuf, lexeme_end lexbuf, "decl"
-	else
-	  next_interior_order lexbuf
+      { if id = "Time" then next_starting_order lexbuf else
+	begin
+	  starting:=false; 
+          if is_one_word_command id then 
+	    lexeme_start lexbuf, lexeme_end lexbuf, "kwd" 
+	  else if is_one_word_declaration id then
+	    lexeme_start lexbuf, lexeme_end lexbuf, "decl"
+	  else
+	    next_interior_order lexbuf
+	end
       }
   | _    { starting := false; next_interior_order lexbuf}
   | eof  { raise End_of_file }
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index d851dc2f..d9b5e572 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ideutils.ml 11093 2008-06-10 18:41:33Z barras $ *)
+(* $Id: ideutils.ml 11749 2009-01-05 14:01:04Z notin $ *)
 
 
 open Preferences
@@ -33,10 +33,7 @@ let prerr_string s =
   if !debug then (prerr_string s;flush stderr)
 
 let lib_ide_file f =
-  let coqlib =
-    System.getenv_else "COQLIB"
-      (if Coq_config.local || !Flags.boot then Coq_config.coqtop
-       else Coq_config.coqlib) in
+  let coqlib = Envars.coqlib () in
   Filename.concat (Filename.concat coqlib "ide") f
   
 let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT
diff --git a/ide/undo_lablgtk_ge212.mli b/ide/undo_lablgtk_ge212.mli
new file mode 100644
index 00000000..916a06e9
--- /dev/null
+++ b/ide/undo_lablgtk_ge212.mli
@@ -0,0 +1,36 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: undo_lablgtk_ge26.mli 7580 2005-11-18 17:09:10Z herbelin $ i*)
+
+(* An undoable view class *)
+
+class undoable_view : [> Gtk.text_view] Gtk.obj ->
+object
+  inherit GText.view
+  method undo : bool
+  method redo : bool
+  method clear_undo : unit
+end
+
+val undoable_view : 
+    ?buffer:GText.buffer ->
+    ?editable:bool ->
+    ?cursor_visible:bool ->
+    ?justification:GtkEnums.justification ->
+    ?wrap_mode:GtkEnums.wrap_mode ->
+    ?accepts_tab:bool ->
+    ?border_width:int ->
+    ?width:int ->
+    ?height:int ->
+    ?packing:(GObj.widget -> unit) ->
+    ?show:bool ->
+    unit ->
+  undoable_view
+
+