Imported Upstream version 8.0pl2upstream/8.0pl2

10 files changed, 22 insertions, 15 deletions

diff --git a/ide/command_windows.mli b/ide/command_windows.mli
index 014be777..6028c818 100644
--- a/ide/command_windows.mli
+++ b/ide/command_windows.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: command_windows.mli,v 1.1.2.1 2004/07/16 19:30:19 herbelin Exp $ *)
+(*i $Id: command_windows.mli,v 1.1.2.2 2005/01/21 17:21:33 herbelin Exp $ i*)
 
 class command_window :
   unit ->
diff --git a/ide/coq.mli b/ide/coq.mli
index bcebd4e6..c1dfd847 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq.mli,v 1.14.2.2 2004/07/18 11:20:15 herbelin Exp $ *)
+(*i $Id: coq.mli,v 1.14.2.3 2005/01/21 17:21:33 herbelin Exp $ i*)
 
 open Names
 open Term
diff --git a/ide/coq_tactics.mli b/ide/coq_tactics.mli
index 8d603346..962b4d27 100644
--- a/ide/coq_tactics.mli
+++ b/ide/coq_tactics.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq_tactics.mli,v 1.1.2.1 2004/07/16 19:30:20 herbelin Exp $ *)
+(*i $Id: coq_tactics.mli,v 1.1.2.2 2005/01/21 17:21:33 herbelin Exp $ i*)
 
 val tactics : string list
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 2169862e..08994010 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqide.ml,v 1.99.2.2 2004/07/18 11:20:15 herbelin Exp $ *)
+(* $Id: coqide.ml,v 1.99.2.3 2004/10/15 14:50:12 coq Exp $ *)
 
 open Preferences
 open Vernacexpr
@@ -1030,6 +1030,7 @@ object(self)
       end_iter#nocopy#set_offset (start#offset + !Find_phrase.length);
       Some (start,end_iter)
     with
+(*
     | Find_phrase.EOF s -> 
 	(* Phrase is at the end of the buffer*)
 	let si = start#offset in
@@ -1038,6 +1039,7 @@ object(self)
 	input_buffer#insert ~iter:end_iter "\n";
 	Some (input_buffer#get_iter (`OFFSET si),
 	      input_buffer#get_iter (`OFFSET ei))
+*)
     | _ -> None
 
   method complete_at_offset (offset:int) = 
diff --git a/ide/coqide.mli b/ide/coqide.mli
index 15e28fea..553426f1 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqide.mli,v 1.1.2.1 2004/07/16 19:30:20 herbelin Exp $ *)
+(*i $Id: coqide.mli,v 1.1.2.2 2005/01/21 17:21:33 herbelin Exp $ i*)
 
 (* The CoqIde main module. The following function [start] will parse the
    command line, initialize the load path, load the input 
diff --git a/ide/find_phrase.mll b/ide/find_phrase.mll
index 8081474f..7b65bd94 100644
--- a/ide/find_phrase.mll
+++ b/ide/find_phrase.mll
@@ -6,13 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: find_phrase.mll,v 1.8.2.1 2004/07/16 19:30:20 herbelin Exp $ *)
+(* $Id: find_phrase.mll,v 1.8.2.2 2004/10/15 14:50:13 coq Exp $ *)
 
 {
   exception Lex_error of string
   let length = ref 0
   let buff = Buffer.create 513
-  exception EOF of string
 
 }
 
@@ -34,10 +33,13 @@ rule next_phrase = parse
       Buffer.contents buff}
 
   | phrase_sep eof{
+      length := !length + 1; 
+      Buffer.add_string buff (Lexing.lexeme lexbuf);
+      Buffer.contents buff}
+  | phrase_sep phrase_sep {
       length := !length + 2; 
       Buffer.add_string buff (Lexing.lexeme lexbuf);
-      Buffer.add_char buff '\n';
-      raise (EOF(Buffer.contents buff))}
+      next_phrase lexbuf}
   | _ 
       { 
 	let c = Lexing.lexeme_char lexbuf 0 in 
diff --git a/ide/highlight.mll b/ide/highlight.mll
index 21063459..e2a1d0cd 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: highlight.mll,v 1.14.2.1 2004/07/16 19:30:20 herbelin Exp $ *)
+(* $Id: highlight.mll,v 1.14.2.2 2004/11/27 14:41:43 herbelin Exp $ *)
 
 {
 
@@ -29,18 +29,21 @@ let identchar =
 let ident = firstchar identchar*
 
 let keyword = 
-  "Add" | "CoInductive" | "Defined" | 
+  "Add" | "Defined" | 
   "End" | "Export" | "Extraction" | "Hint" |
   "Implicits" | "Import" | 
   "Infix" | "Load" | "match" | "Module" | "Module Type" |
   "Proof" | "Qed" |
-  "Record" | "Require" | "Save" | "Scheme" |
+  "Require" | "Save" | "Scheme" |
   "Section" | "Unset" |
   "Set"  
 
 let declaration = 
   "Lemma" | "Axiom" | "CoFixpoint" | "Definition"  |
   "Fixpoint" | "Hypothesis" | 
+  "Hypotheses" | "Axioms" | "Parameters" | "Subclass" |
+  "Remark" | "Fact" | "Conjecture" | "Let" |
+  "CoInductive" | "Record" | "Structure" |
   "Inductive" | "Parameter" | "Theorem" | 
   "Variable" | "Variables" 
 
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 7c225e0e..d91faff4 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ideutils.mli,v 1.6.2.1 2004/07/16 19:30:20 herbelin Exp $ *)
+(*i $Id: ideutils.mli,v 1.6.2.2 2005/01/21 17:21:33 herbelin Exp $ i*)
 
 val async : ('a -> unit) -> 'a -> unit
 val browse : (string -> unit) -> string -> unit
diff --git a/ide/preferences.mli b/ide/preferences.mli
index b4be283d..048707a3 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: preferences.mli,v 1.8.2.1 2004/07/16 19:30:21 herbelin Exp $ *)
+(*i $Id: preferences.mli,v 1.8.2.2 2005/01/21 17:21:33 herbelin Exp $ i*)
 
 type pref =
     {
diff --git a/ide/undo.mli b/ide/undo.mli
index 6c7492ab..11613fdb 100644
--- a/ide/undo.mli
+++ b/ide/undo.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: undo.mli,v 1.4.2.1 2004/07/16 19:30:21 herbelin Exp $ *)
+(*i $Id: undo.mli,v 1.4.2.2 2005/01/21 17:21:33 herbelin Exp $ i*)
 
 (* An undoable view class *)