[exn] remove `raise` taking optional exception information argument

This was redundant with `iraise`; exceptions in the logic monad now
are forced to attach `info` to `Proofview.NonLogical.raise`

8 files changed, 30 insertions, 26 deletions

diff --git a/clib/exninfo.ml b/clib/exninfo.ml
index ee998c2f17..34a4555a9a 100644
--- a/clib/exninfo.ml
+++ b/clib/exninfo.ml
@@ -81,16 +81,6 @@ let iraise (e,i) =
   | Some bt ->
     Printexc.raise_with_backtrace e bt
 
-let raise ?info e = match info with
-| None ->
-  let () = Mutex.lock lock in
-  let id = Thread.id (Thread.self ()) in
-  let () = current := remove_assoc id !current in
-  let () = Mutex.unlock lock in
-  raise e
-| Some i ->
-  iraise (e,i)
-
 let find_and_remove () =
   let () = Mutex.lock lock in
   let id = Thread.id (Thread.self ()) in
diff --git a/clib/exninfo.mli b/clib/exninfo.mli
index 36cc44cf82..725cd82809 100644
--- a/clib/exninfo.mli
+++ b/clib/exninfo.mli
@@ -79,6 +79,3 @@ val capture : exn -> iexn
 
 val iraise : iexn -> 'a
 (** Raise the given enriched exception. *)
-
-val raise : ?info:info -> exn -> 'a
-(** Raise the given exception with additional information. *)
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 3c383b2e00..6df3378524 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -83,7 +83,7 @@ struct
 
   (** [Pervasives.raise]. Except that exceptions are wrapped with
       {!Exception}. *)
-  let raise ?info = fun e -> (); fun () -> Exninfo.raise ?info (Exception e)
+  let raise (e, info) () = Exninfo.iraise (Exception e, info)
 
   (** [try ... with ...] but restricted to {!Exception}. *)
   let catch = fun s h -> ();
@@ -93,7 +93,8 @@ struct
         h (e, info) ()
 
   let read_line = fun () -> try read_line () with e ->
-    let (e, info) = CErrors.push e in raise ~info e ()
+    let (e, info) = CErrors.push e in
+    raise (e, info) ()
 
   let print_char = fun c -> (); fun () -> print_char c
 
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 75920455ce..5002d24af0 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -70,7 +70,7 @@ module NonLogical : sig
 
   (** [Pervasives.raise]. Except that exceptions are wrapped with
       {!Exception}. *)
-  val raise : ?info:Exninfo.info -> exn -> 'a t
+  val raise : Exninfo.iexn -> 'a t
 
   (** [try ... with ...] but restricted to {!Exception}. *)
   val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
diff --git a/engine/proofview.ml b/engine/proofview.ml
index b0ea75ac60..690b1620b9 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -937,7 +937,7 @@ let tclTIMEOUT n t =
           return (Util.Inr (Logic_monad.Tac_Timeout, info))
         | Logic_monad.TacticFailure e ->
           return (Util.Inr (e, info))
-        | e -> Logic_monad.NonLogical.raise ~info e
+        | e -> Logic_monad.NonLogical.raise (e, info)
       end
   end >>= function
     | Util.Inl (res,s,m,i) ->
diff --git a/ide/idetop.ml b/ide/idetop.ml
index ae2301a0a7..60036ef876 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -70,7 +70,7 @@ let ide_cmd_checks ~last_valid { CAst.loc; v } =
     with e ->
       let (e, info) = CErrors.push e in
       let info = Stateid.add info ~valid:last_valid Stateid.dummy in
-      Exninfo.raise ~info e
+      Exninfo.iraise (e, info)
   in
   if is_debug v.expr then
     user_error "Debug mode not available in the IDE"
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 0e9465839a..392f9b2ffd 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -107,13 +107,29 @@ let db_initialize =
 
 let int_of_string s =
   try Proofview.NonLogical.return (int_of_string s)
-  with e -> Proofview.NonLogical.raise e
+  with e ->
+    let e = Exninfo.capture e in
+    Proofview.NonLogical.raise e
 
 let string_get s i =
   try Proofview.NonLogical.return (String.get s i)
-  with e -> Proofview.NonLogical.raise e
+  with e ->
+    let e = Exninfo.capture e in
+    Proofview.NonLogical.raise e
+
+let check_positive n =
+  try
+    if n < 0 then
+      raise (Invalid_argument "number must be positive")
+    else
+      Proofview.NonLogical.return ()
+  with e ->
+    let e = Exninfo.capture e in
+    Proofview.NonLogical.raise e
 
-let run_invalid_arg () = Proofview.NonLogical.raise (Invalid_argument "run_com")
+let run_invalid_arg () =
+  let info = Exninfo.null in
+  Proofview.NonLogical.raise (Invalid_argument "run_com", info)
 
 (* Gives the number of steps or next breakpoint of a run command *)
 let run_com inst =
@@ -125,7 +141,7 @@ let run_com inst =
       let s = String.sub inst i (String.length inst - i) in
       if inst.[0] >= '0' && inst.[0] <= '9' then
         int_of_string s >>= fun num ->
-        (if num<0 then run_invalid_arg () else return ()) >>
+        check_positive num >>
         (skip:=num) >> (skipped:=0)
       else
         breakpoint:=Some (possibly_unquote s)
@@ -156,11 +172,11 @@ let rec prompt level =
     let open Proofview.NonLogical in
     Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
     if Util.(!batch) then return (DebugOn (level+1)) else
-    let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
+    let exit = (skip:=0) >> (skipped:=0) >> raise (Sys.Break, Exninfo.null) in
     Proofview.NonLogical.catch Proofview.NonLogical.read_line
       begin function (e, info) -> match e with
         | End_of_file -> exit
-        | e -> raise ~info e
+        | e -> raise (e, info)
       end
     >>= fun inst ->
     match inst with
@@ -176,7 +192,7 @@ let rec prompt level =
         Proofview.NonLogical.catch (run_com inst >> runtrue >> return (DebugOn (level+1)))
           begin function (e, info) -> match e with
             | Failure _ | Invalid_argument _ -> prompt level
-            | e -> raise ~info e
+            | e -> raise (e, info)
           end
   end
 
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 431589aa30..196b28b274 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -161,7 +161,7 @@ let set_bt info =
 let throw ?(info = Exninfo.null) e =
   set_bt info >>= fun info ->
   let info = Exninfo.add info fatal_flag () in
-  Proofview.tclLIFT (Proofview.NonLogical.raise ~info e)
+  Proofview.tclLIFT (Proofview.NonLogical.raise (e, info))
 
 let fail ?(info = Exninfo.null) e =
   set_bt info >>= fun info ->