From 3b316ab662a9877001cc4a497d13969d43f7ba4a Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 24 Aug 2007 10:57:37 +0000
Subject: Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et
 -rectypes)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10091 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/toplevel.ml | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 7f21de041..fbdc96d6e 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -139,16 +139,16 @@ let print_highlight_location ib loc =
 
 (* Functions to report located errors in a file. *)
 
-let print_location_in_file s inlibrary fname (bp,ep) =
+let print_location_in_file s inlibrary fname loc =
   let errstrm = (str"Error while reading " ++ str s ++ str" :" ++ fnl ()) in
-  if (bp,ep) = dummy_loc then 
+  if loc = dummy_loc then 
     (errstrm ++ str", unknown location." ++ fnl ())
   else
     if inlibrary then
       (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++
-       str" characters " ++ Cerrors.print_loc (bp,ep) ++ fnl ())
+       str" characters " ++ Cerrors.print_loc loc ++ fnl ())
     else
-    let (bp,ep) = unloc (bp,ep) in
+    let (bp,ep) = unloc loc in
     let ic = open_in fname in
     let rec line_of_pos lin bol cnt =
       if cnt < bp then
@@ -172,15 +172,16 @@ let print_command_location ib dloc =
            str(String.sub ib.str (bp-ib.start) (ep-bp)) ++ fnl ())
     | None -> (mt ())
 
-let valid_loc dloc (b,e) =
-  (b,e) <> dummy_loc
+let valid_loc dloc loc =
+  loc <> dummy_loc
   & match dloc with
-    | Some (bd,ed) -> bd<=b & e<=ed
+    | Some dloc ->
+	let (bd,ed) = unloc dloc in let (b,e) = unloc loc in bd<=b & e<=ed
     | _ -> true
 	  
-let valid_buffer_loc ib dloc (b,e) =
-  valid_loc dloc (b,e) & 
-  let (b,e) = unloc (b,e) in b-ib.start >= 0 & e-ib.start < ib.len & b<=e 
+let valid_buffer_loc ib dloc loc =
+  valid_loc dloc loc & 
+  let (b,e) = unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e 
 
 (*s The Coq prompt is the name of the focused proof, if any, and "Coq"
     otherwise. We trap all exceptions to prevent the error message printing
-- 
cgit v1.2.3