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

4 files changed, 40 insertions, 6 deletions

diff --git a/lib/system.ml b/lib/system.ml
index 65826c81..3fa32ef8 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: system.ml 11801 2009-01-18 20:11:41Z herbelin $ *)
+(* $Id: system.ml 13175 2010-06-22 06:28:37Z herbelin $ *)
 
 open Pp
 open Util
@@ -153,8 +153,12 @@ let where_in_path ?(warn=true) path filename =
 
 let find_file_in_path ?(warn=true) paths filename =
   if not (Filename.is_implicit filename) then
-    let root = Filename.dirname filename in
-    root, filename
+    if Sys.file_exists filename then
+      let root = Filename.dirname filename in
+      root, filename
+    else
+      errorlabstrm "System.find_file_in_path"
+	(hov 0 (str "Can't find file" ++ spc () ++ str filename))
   else 
     try where_in_path ~warn paths filename
     with Not_found ->
@@ -224,6 +228,13 @@ let extern_intern ?(warn=true) magic suffix =
   in 
   (extern_state,intern_state)
 
+let with_magic_number_check f a =
+  try f a
+  with Bad_magic_number fname ->
+    errorlabstrm "with_magic_number_check"
+    (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++ 
+    strbrk "It is corrupted or was compiled with another version of Coq.")
+
 (* Communication through files with another executable *)
 
 let connect writefun readfun com =
diff --git a/lib/system.mli b/lib/system.mli
index ba5aa408..426a00df 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: system.mli 11801 2009-01-18 20:11:41Z herbelin $ i*)
+(*i $Id: system.mli 13175 2010-06-22 06:28:37Z herbelin $ i*)
 
 (*s Files and load paths. Load path entries remember the original root
     given by the user. For efficiency, we keep the full path (field
@@ -54,6 +54,8 @@ val raw_extern_intern : int -> string ->
 val extern_intern : ?warn:bool -> int -> string -> 
   (string -> 'a -> unit) * (load_path -> string -> 'a)
 
+val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
+
 (*s Sending/receiving once with external executable *)
 
 val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a 
diff --git a/lib/util.ml b/lib/util.ml
index dce36419..0d6e7ff2 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: util.ml 12181 2009-06-10 20:53:09Z glondu $ *)
+(* $Id: util.ml 13200 2010-06-25 22:36:25Z letouzey $ *)
 
 open Pp
 
@@ -486,6 +486,26 @@ let lowercase_first_char_utf8 s =
   let j, n = next_utf8 s 0 in
   utf8_of_unicode (lowercase_unicode (String.sub s 0 j) n)
 
+(* For extraction, we need to encode unicode character into ascii ones *)
+
+let ascii_of_ident s =
+  let check_ascii s =
+    let ok = ref true in
+    String.iter (fun c -> if Char.code c >= 128 then ok := false) s;
+    !ok
+  in
+  if check_ascii s then s else
+    let i = ref 0 and out = ref "" in
+    begin try while true do
+      let j, n = next_utf8 s !i in
+      out :=
+       if n >= 128
+       then Printf.sprintf "%s__U%04x_" !out n
+       else Printf.sprintf "%s%c" !out s.[!i];
+      i := !i + j
+    done with End_of_input -> () end;
+    !out
+
 (* Lists *)
 
 let list_intersect l1 l2 = 
diff --git a/lib/util.mli b/lib/util.mli
index 5432eb98..97bda074 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i $Id: util.mli 11897 2009-02-09 19:28:02Z barras $ i*)
+(*i $Id: util.mli 13200 2010-06-25 22:36:25Z letouzey $ i*)
 
 (*i*)
 open Pp
@@ -94,6 +94,7 @@ val classify_unicode : int -> utf8_status
 val check_ident : string -> unit
 val check_ident_soft : string -> unit
 val lowercase_first_char_utf8 : string -> string
+val ascii_of_ident : string -> string
 
 (*s Lists. *)