]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/extlib/hExtlib.ml
* New implementation of localized exceptions
[helm.git] / helm / ocaml / extlib / hExtlib.ml
index a76a5c76e8252dcb7eb734a7ca4a55122a2971d8..6afae34a79fd240f3be640bb209240330579a29c 100644 (file)
@@ -282,3 +282,20 @@ let finally at_end f arg =
   at_end ();
   res
 
+(** {2 Localized exceptions } *)
+
+exception Localized of Token.flocation * exn
+
+let loc_of_floc = function
+  | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
+      (loc_begin, loc_end)
+
+let raise_localized_exception ~offset floc exn =
+ let (x, y) = loc_of_floc floc in
+ let x = offset + x in
+ let y = offset + y in
+ let flocb,floce = floc in
+ let floc =
+   { flocb with Lexing.pos_cnum = x }, { floce with Lexing.pos_cnum = y }
+ in
+  raise (Localized (floc, exn))