From 4c1ccb9e2a4b219ac5180115bc4267e1b059cdd1 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 18 Feb 2013 19:45:36 +0000 Subject: 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 --- lib/loc.mli | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'lib/loc.mli') diff --git a/lib/loc.mli b/lib/loc.mli index c712cddd9..a0b99c689 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 -- cgit v1.2.3