[gramlib] Remove legacy located exception wrapper in favor of standard infrastructure.

The old wrapper was basically unused, this PR also fixes backtraces in
some class of bugs such as https://github.com/coq/coq/issues/12695

3 files changed, 15 insertions, 28 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. *)