Added an indirection with respect to Loc in Compat. As many [open Compat]

were closed (i.e. the only remaining ones are those of printing/parsing).
Meanwhile, a simplified interface is provided in loc.mli.

This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 79 insertions, 41 deletions

diff --git a/lib/errors.ml b/lib/errors.ml
index 026198a98..77f03f045 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-open Compat
 open Pp
 
 (* Errors *)
@@ -32,7 +31,7 @@ let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s)
 (* Like Exc_located, but specifies the outermost file read, the filename
    associated to the location of the error, and the error itself. *)
 
-exception Error_in_file of string * (bool * string * loc) * exn
+exception Error_in_file of string * (bool * string * Loc.t) * exn
 
 exception Timeout
 exception Drop
diff --git a/lib/errors.mli b/lib/errors.mli
index d04ebb3fe..3dd470a06 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -19,17 +19,17 @@ open Pp
 exception Anomaly of string * std_ppcmds
 val anomaly : string -> 'a
 val anomalylabstrm : string -> std_ppcmds -> 'a
-val anomaly_loc : loc * string * std_ppcmds -> 'a
+val anomaly_loc : Loc.t * string * std_ppcmds -> 'a
 
 exception UserError of string * std_ppcmds
 val error : string -> 'a
 val errorlabstrm : string -> std_ppcmds -> 'a
-val user_err_loc : loc * string * std_ppcmds -> 'a
+val user_err_loc : Loc.t * string * std_ppcmds -> 'a
 
 exception AlreadyDeclared of std_ppcmds
 val alreadydeclared : std_ppcmds -> 'a
 
-val invalid_arg_loc : loc * string -> 'a
+val invalid_arg_loc : Loc.t * string -> 'a
 
 (** [todo] is for running of an incomplete code its implementation is
    "do nothing" (or print a message), but this function should not be
@@ -45,7 +45,7 @@ exception Quit
    input buffer associated to the location of the error (or the module name
    if boolean is true), and the error itself. *)
 
-exception Error_in_file of string * (bool * string * loc) * exn
+exception Error_in_file of string * (bool * string * Loc.t) * exn
 
 (** [register_handler h] registers [h] as a handler.
     When an expression is printed with [print e], it
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 1cbf0c780..93fb748ac 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -3,6 +3,7 @@ Xml_parser
 Pp_control
 Compat
 Pp
+Loc
 Errors
 Bigint
 Hashcons
diff --git a/lib/loc.ml b/lib/loc.ml
new file mode 100644
index 000000000..b2d83a78b
--- /dev/null
+++ b/lib/loc.ml
@@ -0,0 +1,29 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+
+include Compat.Loc
+
+(* Locations management *)
+
+let dummy_loc = Compat.Loc.ghost
+let join_loc = Compat.Loc.merge
+let make_loc = Compat.make_loc
+let unloc = Compat.unloc
+
+type 'a located = t * 'a
+let located_fold_left f x (_,a) = f x a
+let located_iter2 f (_,a) (_,b) = f a b
+let down_located f (_,a) = f a
+
+let pr_located pr (loc, x) =
+  if Flags.do_beautify () && loc <> dummy_loc then
+    let (b, e) = unloc loc in
+    Pp.comment b ++ pr x ++ Pp.comment e
+  else pr x
diff --git a/lib/loc.mli b/lib/loc.mli
new file mode 100644
index 000000000..c8e0901e9
--- /dev/null
+++ b/lib/loc.mli
@@ -0,0 +1,44 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** {5 Basic types} *)
+
+type t = Compat.Loc.t
+
+exception Exc_located of t * exn
+
+type 'a located = t * 'a
+
+(** {5 Location manipulation} *)
+
+(** This is inherited from CAMPL4/5. *)
+
+val unloc : t -> int * int
+val make_loc : int * int -> t
+val ghost : t
+val merge : t -> t -> t
+val raise : t -> exn -> 'a
+
+(** {5 Location utilities} *)
+
+val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
+val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
+
+val down_located : ('a -> 'b) -> 'a located -> 'b
+(** Projects out a located object *)
+
+val pr_located : ('a -> Pp.std_ppcmds) -> 'a located -> Pp.std_ppcmds
+(** Prints an object surrounded by its commented location *)
+
+(** {5 Backward compatibility} *)
+
+val dummy_loc : t
+(** Same as [ghost] *)
+
+val join_loc : t -> t -> t
+(** Same as [merge] *)
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 789de8160..fb85af0eb 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Pp_control
-open Compat
 
 (* This should not be used outside of this file. Use
    Flags.print_emacs instead. This one is updated when reading
@@ -374,19 +373,6 @@ let string_of_ppcmds c =
   msg_with Format.str_formatter c;
   Format.flush_str_formatter ()
 
-(* Locations management *)
-type loc = Loc.t
-let dummy_loc = Loc.ghost
-let join_loc = Loc.merge
-let make_loc = make_loc
-let unloc = unloc
-
-type 'a located = loc * 'a
-let located_fold_left f x (_,a) = f x a
-let located_iter2 f (_,a) (_,b) = f a b
-let down_located f (_,a) = f a
-
-
 (* Copy paste from Util *)
 
 let pr_comma () = str "," ++ spc ()
@@ -467,10 +453,4 @@ let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v
 
 let prvect elem v = prvect_with_sep mt elem v
 
-let pr_located pr (loc,x) =
-  if Flags.do_beautify() && loc<>dummy_loc then
-    let (b,e) = unloc loc in
-    comment b ++ pr x ++ comment e
-  else pr x
-
 let surround p = hov 1 (str"(" ++ p ++ str")")
diff --git a/lib/pp.mli b/lib/pp.mli
index 09efc57a1..a1be529a9 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Pp_control
-open Compat
 
 (** Modify pretty printing functions behavior for emacs ouput (special
    chars inserted at some places). This function should called once in
@@ -125,19 +124,6 @@ val msgerr : std_ppcmds -> unit
 val msgerrnl : std_ppcmds -> unit
 val message : string -> unit       (** = pPNL *)
 
-(** {6 Location management. } *)
-
-type loc = Loc.t
-val unloc : loc -> int * int
-val make_loc : int * int -> loc
-val dummy_loc : loc
-val join_loc : loc -> loc -> loc
-
-type 'a located = loc * 'a
-val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
-val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
-val down_located : ('a -> 'b) -> 'a located -> 'b
-
 (** {6 Util copy/paste. } *)
 
 val pr_comma : unit -> std_ppcmds
@@ -163,7 +149,6 @@ val prvecti_with_sep :
    (unit -> std_ppcmds) -> (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
 val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
-val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds
 val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val surround : std_ppcmds -> std_ppcmds