diff options
| -rw-r--r-- | clib/exninfo.ml | 10 | ||||
| -rw-r--r-- | clib/exninfo.mli | 3 | ||||
| -rw-r--r-- | engine/logic_monad.ml | 5 | ||||
| -rw-r--r-- | engine/logic_monad.mli | 2 | ||||
| -rw-r--r-- | engine/proofview.ml | 2 | ||||
| -rw-r--r-- | ide/idetop.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 30 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2core.ml | 2 |
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 -> |