Merge PR #12696: [gramlib] Remove legacy located exception wrapper in favor of standard infrastructure.

Reviewed-by: ppedrot

5 files changed, 16 insertions, 31 deletions

diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index d6951fff6d..83c158e057 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -1548,12 +1548,21 @@ module Parsable = struct
       Stream.Failure ->
       let loc = get_loc () in
       restore ();
-      Ploc.raise loc (Stream.Error ("illegal begin of " ^ entry.ename))
+      Loc.raise ~loc (Stream.Error ("illegal begin of " ^ entry.ename))
     | Stream.Error _ as exc ->
-      let loc = get_loc () in restore (); Ploc.raise loc exc
+      let loc = get_loc () in restore ();
+      Loc.raise ~loc exc
     | exc ->
+      let exc,info = Exninfo.capture exc in
       let loc = Stream.count cs, Stream.count cs + 1 in
-      restore (); Ploc.raise (Ploc.make_unlined loc) exc
+      restore ();
+      (* If the original exn had a loc, keep it *)
+      let info =
+        match Loc.get_loc info with
+        | Some _ -> info
+        | None -> Loc.add_loc info (Ploc.make_unlined loc)
+      in
+      Exninfo.iraise (exc,info)
 
   let parse_parsable e p =
     L.State.set !(p.lexer_state);
@@ -1561,11 +1570,10 @@ module Parsable = struct
       let c = parse_parsable e p in
       p.lexer_state := L.State.get ();
       c
-    with Ploc.Exc (loc,e) ->
+    with exn ->
+      let exn,info = Exninfo.capture exn in
       L.State.drop ();
-      let loc' = Loc.get_loc (Exninfo.info e) in
-      let loc = match loc' with None -> loc | Some loc -> loc in
-      Loc.raise ~loc e
+      Exninfo.iraise (exn,info)
 
   let make ?loc cs =
     let lexer_state = ref (L.State.init ()) in
diff --git a/gramlib/ploc.ml b/gramlib/ploc.ml
index 056a2b7ad3..e121342c94 100644
--- a/gramlib/ploc.ml
+++ b/gramlib/ploc.ml
@@ -16,10 +16,3 @@ let dummy =
 
 let sub loc sh len = {loc with bp = loc.bp + sh; ep = loc.bp + sh + len}
 let after loc sh len = {loc with bp = loc.ep + sh; ep = loc.ep + sh + len}
-
-exception Exc of Loc.t * exn
-
-let raise loc exc =
-  match exc with
-    Exc (_, _) -> raise exc
-  | _ -> raise (Exc (loc, exc))
diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli
index 15a5a74455..4b865110c3 100644
--- a/gramlib/ploc.mli
+++ b/gramlib/ploc.mli
@@ -2,20 +2,6 @@
 (* ploc.mli,v *)
 (* Copyright (c) INRIA 2007-2017 *)
 
-(* located exceptions *)
-
-exception Exc of Loc.t * exn
-   (** [Ploc.Exc loc e] is an encapsulation of the exception [e] with
-       the input location [loc]. To be used to specify a location
-       for an error. This exception must not be raised by [raise] but
-       rather by [Ploc.raise] (see below), to prevent the risk of several
-       encapsulations of [Ploc.Exc]. *)
-
-val raise : Loc.t -> exn -> 'a
-   (** [Ploc.raise loc e], if [e] is already the exception [Ploc.Exc],
-       re-raise it (ignoring the new location [loc]), else raise the
-       exception [Ploc.Exc loc e]. *)
-
 val make_unlined : int * int -> Loc.t
    (** [Ploc.make_unlined] is like [Ploc.make] except that the line number
        is not provided (to be used e.g. when the line number is unknown. *)
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index ba978c0705..1b7768852e 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1129,8 +1129,7 @@ let tclDO n tac =
       let _, info = Exninfo.capture e in
       let e' = CErrors.UserError (l, prefix i ++ s) in
       Exninfo.iraise (e', info)
-    | Gramlib.Ploc.Exc(loc, CErrors.UserError (l, s))  ->
-      raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
+  in
   let rec loop i gl =
     if i = n then tac_err_at i gl else
     (tclTHEN (tac_err_at i) (loop (i + 1))) gl in
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index a12b4aad11..1c81fbc10b 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -490,7 +490,6 @@ let equality_inj l b id c =
   let msg = ref "" in
   try Proofview.V82.of_tactic (Equality.inj None l b None c) gl
   with
-    | Gramlib.Ploc.Exc(_,CErrors.UserError (_,s))
     | CErrors.UserError (_,s)
   when msg := Pp.string_of_ppcmds s;
        !msg = "Not a projectable equality but a discriminable one." ||