Removing Exc_located and using the new exception enrichement

mechanism to retrieve the same information.

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

2 files changed, 23 insertions, 9 deletions

diff --git a/lib/loc.ml b/lib/loc.ml
index e87ad132e6..8f133ce0d4 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -19,8 +19,6 @@ type t = {
   ep : int; (** end position *)
 }
 
-exception Exc_located of t * exn
-
 let create fname line_nb bol_pos (bp, ep) = {
   fname = fname; line_nb = line_nb; bol_pos = bol_pos;
   line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; }
@@ -58,12 +56,22 @@ let unloc loc = (loc.bp, loc.ep)
 
 let represent loc = (loc.fname, loc.line_nb, loc.bol_pos, loc.bp, loc.ep)
 
-let raise loc e = raise (Exc_located (loc, e))
-
 let dummy_loc = ghost
 let join_loc = merge
 
+(** Located type *)
+
 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
+
+(** Exceptions *)
+
+let location : t Exninfo.t = Exninfo.make ()
+
+let add_loc e loc = Exninfo.add e location loc
+
+let get_loc e = Exninfo.get e location
+
+let raise loc e = raise (Exninfo.add e location loc)
diff --git a/lib/loc.mli b/lib/loc.mli
index c712cddd9e..a0b99c689a 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -10,8 +10,6 @@
 
 type t
 
-exception Exc_located of t * exn
-
 type 'a located = t * 'a
 (** Embed a location in a type *)
 
@@ -37,12 +35,20 @@ val is_ghost : t -> bool
 
 val merge : t -> t -> t
 
-val raise : t -> exn -> 'a
-(** Raise a located exception *)
-
 val represent : t -> (string * int * int * int * int)
 (** Return the arguments given in [create] *)
 
+(** {5 Located exceptions} *)
+
+val add_loc : exn -> t -> exn
+(** Adding location to an exception *)
+
+val get_loc : exn -> t option
+(** Retrieving the optional location of an exception *)
+
+val raise : t -> exn -> 'a
+(** [raise loc e] is the same as [Pervasives.raise (add_loc e loc)]. *)
+
 (** {5 Location utilities} *)
 
 val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a