Imported Upstream version 8.2pl2+dfsgupstream/8.2.pl2+dfsg

4 files changed, 25 insertions, 26 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6a75b99c..821a73f7 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: metasyntax.ml 11786 2009-01-14 13:07:34Z herbelin $ *)
+(* $Id: metasyntax.ml 12882 2010-03-23 22:34:38Z herbelin $ *)
 
 open Pp
 open Util
@@ -266,16 +266,18 @@ let split_notation_string str =
 
 (* Interpret notations with a recursive component *)
 
-let rec find_pattern xl = function
-  | Break n as x :: l, Break n' :: l' when n=n' -> 
-      find_pattern (x::xl) (l,l')
+let out_nt = function NonTerminal x -> x | _ -> assert false
+
+let rec find_pattern nt xl = function
+  | Break n as x :: l, Break n' :: l' when n=n' ->
+      find_pattern nt (x::xl) (l,l')
   | Terminal s as x :: l, Terminal s' :: l' when s = s' -> 
-      find_pattern (x::xl) (l,l')
-  | [NonTerminal x], NonTerminal x' :: l' ->
-      (x,x',xl),l'
-  | [NonTerminal _], Terminal s :: _ | Terminal s :: _, _ ->
+      find_pattern nt (x::xl) (l,l')
+  | [], NonTerminal x' :: l' ->
+      (out_nt nt,x',List.rev xl),l'
+  | [], Terminal s :: _ | Terminal s :: _, _ ->
       error ("The token "^s^" occurs on one side of \"..\" but not on the other side.")
-  | [NonTerminal _], Break s :: _ | Break s :: _, _ ->
+  | [], Break s :: _ | Break s :: _, _ ->
       error ("A break occurs on one side of \"..\" but not on the other side.")
   | ((SProdList _ | NonTerminal _) :: _ | []), _ -> 
       error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".")
@@ -283,7 +285,8 @@ let rec find_pattern xl = function
 let rec interp_list_parser hd = function
   | [] -> [], [], List.rev hd
   | NonTerminal id :: tl when id = ldots_var ->
-      let ((x,y,sl),tl') = find_pattern [] (hd,tl) in
+      let hd = List.rev hd in
+      let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
       let yl,xl,tl'' = interp_list_parser [] tl' in
       (* We remember each pair of variable denoting a recursive part to *)
       (* remove the second copy of it afterwards *)
@@ -299,6 +302,7 @@ let rec interp_list_parser hd = function
       yl, xl, List.rev_append hd tl'
   | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
 
+
 (* Find non-terminal tokens of notation *)
 
 let unquote_notation_token s =
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 176f336b..b54700d3 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -11,7 +11,7 @@
  * camlp4deps will not work for this file unless Makefile system enhanced.
  *)
 
-(* $Id: mltop.ml4 11801 2009-01-18 20:11:41Z herbelin $ *)
+(* $Id: mltop.ml4 12341 2009-09-17 16:03:19Z glondu $ *)
 
 open Util
 open Pp
@@ -109,7 +109,7 @@ let dir_ml_load s =
 	 * in this file, the Makefile dependency logic needs to be updated.
 	 *)
         let warn = Flags.is_verbose() in
-        let _,gname = where_in_path ~warn !coq_mlpath_copy s in
+        let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in
         try
           Dynlink.loadfile gname;
 	with | Dynlink.Error a ->
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index a1acd1d6..9d64f983 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: toplevel.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: toplevel.ml 12891 2010-03-30 11:40:02Z herbelin $ *)
 
 open Pp
 open Util
@@ -163,11 +163,10 @@ let print_location_in_file s inlibrary fname loc =
     try
       let (line, bol) = line_of_pos 1 0 0 in
       close_in ic;
-      hov 0
-        (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ str"," ++ spc() ++
-         hov 0 (str"line " ++ int line ++ str"," ++ spc() ++
-                str"characters " ++
-                Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":") ++
+      hov 0 (* No line break so as to follow emacs error message format *)
+        (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++
+         str", line " ++ int line ++ str", characters " ++
+         Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":" ++
       fnl ()
     with e ->
       (close_in ic;
@@ -316,7 +315,7 @@ let parse_to_dot =
 let rec discard_to_dot () =
   try 
     Gram.Entry.parse parse_to_dot top_buffer.tokens
-  with Stdpp.Exc_located(_,Token.Error _) -> 
+  with Stdpp.Exc_located(_,(Token.Error _|Lexer.Error _)) -> 
     discard_to_dot()
 
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6a0acb52..385afbec 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacentries.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id: vernacentries.ml 12343 2009-09-17 17:02:03Z glondu $ i*)
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
@@ -234,12 +234,8 @@ let dump_universes s =
 (* "Locate" commands *)
 
 let locate_file f =
-  try
-    let _,file = System.where_in_path ~warn:false (Library.get_load_paths ()) f in
-    msgnl (str file)
-  with Not_found -> 
-    msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++
-		  str"on loadpath"))
+  let _,file = System.find_file_in_path ~warn:false (Library.get_load_paths ()) f in
+  msgnl (str file)
 
 let msg_found_library = function
   | Library.LibLoaded, fulldir, file ->