more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Thu Sep 09 17:20:27 2010 +0200
@@ -73,12 +73,12 @@
fun log_exn log tag id e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
fun catch tag f id (st as {log, ...}: run_args) = (f id st; ())
- handle (exn as Exn.Interrupt) => reraise exn
- | exn => (log_exn log tag id exn; ())
+ handle exn =>
+ if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; ())
fun catch_result tag d f id (st as {log, ...}: run_args) = f id st
- handle (exn as Exn.Interrupt) => reraise exn
- | exn => (log_exn log tag id exn; d)
+ handle exn =>
+ if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; d)
fun register (init, run, done) thy =
let val id = length (Actions.get thy) + 1
--- a/src/Pure/Concurrent/future.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/Concurrent/future.ML Thu Sep 09 17:20:27 2010 +0200
@@ -110,7 +110,7 @@
val _ = Single_Assignment.assign result res
handle exn as Fail _ =>
(case Single_Assignment.peek result of
- SOME (Exn.Exn Exn.Interrupt) => raise Exn.Interrupt
+ SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn)
| _ => reraise exn);
val ok =
(case the (Single_Assignment.peek result) of
@@ -184,7 +184,7 @@
Exn.capture (fn () =>
Multithreading.with_attributes Multithreading.private_interrupts
(fn _ => Position.setmp_thread_data pos e ())) ()
- else Exn.Exn Exn.Interrupt;
+ else Exn.interrupt_exn;
in assign_result group result res end;
in (result, job) end;
@@ -359,10 +359,12 @@
val _ = broadcast scheduler_event;
in continue end
- handle Exn.Interrupt =>
- (Multithreading.tracing 1 (fn () => "Interrupt");
- List.app cancel_later (Task_Queue.cancel_all (! queue));
- broadcast_work (); true);
+ handle exn =>
+ if Exn.is_interrupt exn then
+ (Multithreading.tracing 1 (fn () => "Interrupt");
+ List.app cancel_later (Task_Queue.cancel_all (! queue));
+ broadcast_work (); true)
+ else reraise exn;
fun scheduler_loop () =
while
@@ -415,11 +417,12 @@
fun get_result x =
(case peek x of
NONE => Exn.Exn (Fail "Unfinished future")
- | SOME (exn as Exn.Exn Exn.Interrupt) =>
- (case Exn.flatten_list (Task_Queue.group_status (group_of x)) of
- [] => exn
- | exns => Exn.Exn (Exn.EXCEPTIONS exns))
- | SOME res => res);
+ | SOME res =>
+ if Exn.is_interrupt_exn res then
+ (case Exn.flatten_list (Task_Queue.group_status (group_of x)) of
+ [] => res
+ | exns => Exn.Exn (Exn.EXCEPTIONS exns))
+ else res);
fun join_next deps = (*requires SYNCHRONIZED*)
if null deps then NONE
@@ -486,7 +489,7 @@
fun promise_group group : 'a future =
let
val result = Single_Assignment.var "promise" : 'a result;
- fun abort () = assign_result group result (Exn.Exn Exn.Interrupt) handle Fail _ => true;
+ fun abort () = assign_result group result Exn.interrupt_exn handle Fail _ => true;
val task = SYNCHRONIZED "enqueue_passive" (fn () =>
Unsynchronized.change_result queue (Task_Queue.enqueue_passive group abort));
in Future {promised = true, task = task, group = group, result = result} end;
@@ -496,7 +499,7 @@
fun fulfill_result (Future {promised, task, group, result}) res =
let
val _ = promised orelse raise Fail "Not a promised future";
- fun job ok = assign_result group result (if ok then res else Exn.Exn Exn.Interrupt);
+ fun job ok = assign_result group result (if ok then res else Exn.interrupt_exn);
val _ = execute (task, group, [job]);
in () end;
--- a/src/Pure/Concurrent/lazy.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/Concurrent/lazy.ML Thu Sep 09 17:20:27 2010 +0200
@@ -60,9 +60,9 @@
(*semantic race: some other threads might see the same
Interrupt, until there is a fresh start*)
val _ =
- (case res of
- Exn.Exn Exn.Interrupt => Synchronized.change var (fn _ => Expr e)
- | _ => ());
+ if Exn.is_interrupt_exn res then
+ Synchronized.change var (fn _ => Expr e)
+ else ();
in res end
| NONE => restore_interrupts (fn () => Future.join_result x) ())
end) ());
--- a/src/Pure/Concurrent/lazy_sequential.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/Concurrent/lazy_sequential.ML Thu Sep 09 17:20:27 2010 +0200
@@ -34,10 +34,7 @@
(case ! r of
Expr e => Exn.capture e ()
| Result res => res);
- val _ =
- (case result of
- Exn.Exn Exn.Interrupt => ()
- | _ => r := Result result);
+ val _ = if Exn.is_interrupt_exn result then () else r := Result result;
in result end;
fun force r = Exn.release (force_result r);
--- a/src/Pure/Concurrent/simple_thread.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML Thu Sep 09 17:20:27 2010 +0200
@@ -19,7 +19,9 @@
if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts;
fun fork interrupts body =
- Thread.fork (fn () => exception_trace (fn () => body () handle Exn.Interrupt => ()),
+ Thread.fork (fn () =>
+ exception_trace (fn () =>
+ body () handle exn => if Exn.is_interrupt exn then () else reraise exn),
attributes interrupts);
fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
--- a/src/Pure/Concurrent/task_queue.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Thu Sep 09 17:20:27 2010 +0200
@@ -80,9 +80,8 @@
fun cancel_group (Group {status, ...}) exn =
Synchronized.change status
(fn exns =>
- (case exn of
- Exn.Interrupt => if null exns then [exn] else exns
- | _ => exn :: exns));
+ if not (Exn.is_interrupt exn) orelse null exns then exn :: exns
+ else exns);
fun is_canceled (Group {parent, status, ...}) =
not (null (Synchronized.value status)) orelse
--- a/src/Pure/General/basics.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/General/basics.ML Thu Sep 09 17:20:27 2010 +0200
@@ -94,7 +94,7 @@
(* partiality *)
fun try f x = SOME (f x)
- handle (exn as Exn.Interrupt) => reraise exn | _ => NONE;
+ handle exn => if Exn.is_interrupt exn then reraise exn else NONE;
fun can f x = is_some (try f x);
--- a/src/Pure/General/exn.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/General/exn.ML Thu Sep 09 17:20:27 2010 +0200
@@ -12,6 +12,10 @@
val capture: ('a -> 'b) -> 'a -> 'b result
val release: 'a result -> 'a
exception Interrupt
+ val interrupt: unit -> 'a
+ val is_interrupt: exn -> bool
+ val interrupt_exn: 'a result
+ val is_interrupt_exn: 'a result -> bool
exception EXCEPTIONS of exn list
val flatten: exn -> exn list
val flatten_list: exn list -> exn list
@@ -40,14 +44,27 @@
| release (Exn e) = reraise e;
-(* interrupt and nested exceptions *)
+(* interrupts *)
exception Interrupt = Interrupt;
+
+fun interrupt () = raise Interrupt;
+
+fun is_interrupt Interrupt = true
+ | is_interrupt _ = false;
+
+val interrupt_exn = Exn Interrupt;
+
+fun is_interrupt_exn (Exn exn) = is_interrupt exn
+ | is_interrupt_exn _ = false;
+
+
+(* nested exceptions *)
+
exception EXCEPTIONS of exn list;
-fun flatten Interrupt = []
- | flatten (EXCEPTIONS exns) = flatten_list exns
- | flatten exn = [exn]
+fun flatten (EXCEPTIONS exns) = flatten_list exns
+ | flatten exn = if is_interrupt exn then [] else [exn]
and flatten_list exns = List.concat (map flatten exns);
fun release_all results =
--- a/src/Pure/Isar/proof.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/Isar/proof.ML Thu Sep 09 17:20:27 2010 +0200
@@ -990,8 +990,9 @@
(case test_proof goal_state of
Exn.Result (SOME _) => goal_state
| Exn.Result NONE => error (fail_msg (context_of goal_state))
- | Exn.Exn Exn.Interrupt => raise Exn.Interrupt
- | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
+ | Exn.Exn exn =>
+ if Exn.is_interrupt exn then reraise exn
+ else raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
end;
in
--- a/src/Pure/Isar/runtime.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/Isar/runtime.ML Thu Sep 09 17:20:27 2010 +0200
@@ -54,30 +54,38 @@
val detailed = ! Output.debugging;
- fun exn_msgs _ (CONTEXT (ctxt, exn)) = exn_msgs (SOME ctxt) exn
- | exn_msgs ctxt (Exn.EXCEPTIONS exns) = maps (exn_msgs ctxt) exns
- | exn_msgs ctxt (EXCURSION_FAIL (exn, loc)) =
- map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs ctxt exn)
- | exn_msgs _ TERMINATE = ["Exit"]
- | exn_msgs _ Exn.Interrupt = []
- | exn_msgs _ TimeLimit.TimeOut = ["Timeout"]
- | exn_msgs _ TOPLEVEL_ERROR = ["Error"]
- | exn_msgs _ (SYS_ERROR msg) = ["## SYSTEM ERROR ##\n" ^ msg]
- | exn_msgs _ (ERROR msg) = [msg]
- | exn_msgs _ (exn as Fail msg) = [raised exn "Fail" [msg]]
- | exn_msgs _ (exn as THEORY (msg, thys)) =
- [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
- | exn_msgs _ (exn as Syntax.AST (msg, asts)) = [raised exn "AST" (msg ::
- (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
- | exn_msgs ctxt (exn as TYPE (msg, Ts, ts)) = [raised exn "TYPE" (msg ::
- (if detailed then
- if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
- else []))]
- | exn_msgs ctxt (exn as TERM (msg, ts)) = [raised exn "TERM" (msg ::
- (if detailed then if_context ctxt Syntax.string_of_term ts else []))]
- | exn_msgs ctxt (exn as THM (msg, i, thms)) = [raised exn ("THM " ^ string_of_int i) (msg ::
- (if detailed then if_context ctxt Display.string_of_thm thms else []))]
- | exn_msgs _ exn = [raised exn (General.exnMessage exn) []];
+ fun exn_msgs context exn =
+ if Exn.is_interrupt exn then []
+ else
+ (case exn of
+ Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
+ | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
+ | EXCURSION_FAIL (exn, loc) =>
+ map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs context exn)
+ | TERMINATE => ["Exit"]
+ | TimeLimit.TimeOut => ["Timeout"]
+ | TOPLEVEL_ERROR => ["Error"]
+ | SYS_ERROR msg => ["## SYSTEM ERROR ##\n" ^ msg]
+ | ERROR msg => [msg]
+ | Fail msg => [raised exn "Fail" [msg]]
+ | THEORY (msg, thys) =>
+ [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
+ | Syntax.AST (msg, asts) =>
+ [raised exn "AST" (msg ::
+ (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
+ | TYPE (msg, Ts, ts) =>
+ [raised exn "TYPE" (msg ::
+ (if detailed then
+ if_context context Syntax.string_of_typ Ts @
+ if_context context Syntax.string_of_term ts
+ else []))]
+ | TERM (msg, ts) =>
+ [raised exn "TERM" (msg ::
+ (if detailed then if_context context Syntax.string_of_term ts else []))]
+ | THM (msg, i, thms) =>
+ [raised exn ("THM " ^ string_of_int i) (msg ::
+ (if detailed then if_context context Display.string_of_thm thms else []))]
+ | _ => [raised exn (General.exnMessage exn) []]);
in exn_msgs NONE e end;
fun exn_message exn_position exn =
--- a/src/Pure/Isar/toplevel.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Sep 09 17:20:27 2010 +0200
@@ -231,7 +231,7 @@
fun thread interrupts body =
Thread.fork
- (((fn () => body () handle Exn.Interrupt => ())
+ (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
|> Runtime.debugging
|> Runtime.toplevel_error
(fn exn => priority ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Thu Sep 09 17:20:27 2010 +0200
@@ -148,7 +148,7 @@
(OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
val result = Exn.capture (restore_attributes f) x;
- val was_timeout = (case result of Exn.Exn Exn.Interrupt => ! timeout | _ => false);
+ val was_timeout = Exn.is_interrupt_exn result andalso ! timeout;
val _ = Thread.interrupt watchdog handle Thread _ => ();
in if was_timeout then raise TimeOut else Exn.release result end) ();
@@ -209,7 +209,7 @@
let val res =
sync_wait (SOME orig_atts)
(SOME (Time.+ (Time.now (), Time.fromMilliseconds 100))) cond lock
- in case res of Exn.Exn Exn.Interrupt => kill 10 | _ => () end;
+ in if Exn.is_interrupt_exn res then kill 10 else () end;
(*cleanup*)
val output = read_file output_name handle IO.Io _ => "";
@@ -217,7 +217,7 @@
val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => ();
val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
val _ = Thread.interrupt system_thread handle Thread _ => ();
- val rc = (case ! result of Signal => raise Exn.Interrupt | Result rc => rc);
+ val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc);
in (output, rc) end);
--- a/src/Pure/ML-Systems/smlnj.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Thu Sep 09 17:20:27 2010 +0200
@@ -142,7 +142,7 @@
fun interruptible (f: 'a -> 'b) x =
let
- val result = ref (Exn.Exn Interrupt: 'b Exn.result);
+ val result = ref (Exn.interrupt_exn: 'b Exn.result);
val old_handler = Signals.inqHandler Signals.sigINT;
in
SMLofNJ.Cont.callcc (fn cont =>
@@ -165,7 +165,7 @@
struct
open TextIO;
fun inputLine is = TextIO.inputLine is
- handle IO.Io _ => raise Interrupt;
+ handle IO.Io _ => Exn.interrupt ();
end;
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Thu Sep 09 17:20:27 2010 +0200
@@ -186,17 +186,18 @@
val _ =
(while not (List.null (! input_buffer)) do
PolyML.compiler (get, parameters) ())
- handle exn as Exn.Interrupt => reraise exn
- | exn =>
- let
- val exn_msg =
- (case exn of
- STATIC_ERRORS () => ""
- | Runtime.TOPLEVEL_ERROR => ""
- | _ => "Exception- " ^ General.exnMessage exn ^ " raised");
- val _ = output_warnings ();
- val _ = output_writeln ();
- in raise_error exn_msg end;
+ handle exn =>
+ if Exn.is_interrupt exn then reraise exn
+ else
+ let
+ val exn_msg =
+ (case exn of
+ STATIC_ERRORS () => ""
+ | Runtime.TOPLEVEL_ERROR => ""
+ | _ => "Exception- " ^ General.exnMessage exn ^ " raised");
+ val _ = output_warnings ();
+ val _ = output_writeln ();
+ in raise_error exn_msg end;
in
if verbose then (output_warnings (); flush_error (); output_writeln ())
else ()
--- a/src/Pure/PIDE/document.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/PIDE/document.ML Thu Sep 09 17:20:27 2010 +0200
@@ -225,7 +225,7 @@
SOME (st', NONE) => ([], SOME st')
| SOME (_, SOME exn_info) =>
(case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
- [] => raise Exn.Interrupt
+ [] => Exn.interrupt ()
| errs => (errs, NONE))
| NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
val _ = List.app (Toplevel.error_msg tr) errs;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Sep 09 11:05:52 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Sep 09 17:20:27 2010 +0200
@@ -983,17 +983,18 @@
end handle e => handler (e,SOME src) (* error in XML parse or Ready issue *)
and handler (e,srco) =
- case (e,srco) of
- (XML_PARSE,SOME src) =>
- panic "Invalid XML input, aborting" (* TODO: attempt recovery *)
- | (Exn.Interrupt,SOME src) =>
- (Output.error_msg "Interrupt during PGIP processing"; loop true src)
- | (Toplevel.UNDEF,SOME src) =>
- (Output.error_msg "No working context defined"; loop true src)
- | (e,SOME src) =>
- (Output.error_msg (ML_Compiler.exn_message e); loop true src)
- | (PGIP_QUIT,_) => ()
- | (_,NONE) => ()
+ if Exn.is_interrupt e andalso is_some srco then
+ (Output.error_msg "Interrupt during PGIP processing"; loop true (the srco))
+ else
+ case (e,srco) of
+ (XML_PARSE,SOME src) =>
+ panic "Invalid XML input, aborting" (* TODO: attempt recovery *)
+ | (Toplevel.UNDEF,SOME src) =>
+ (Output.error_msg "No working context defined"; loop true src)
+ | (e,SOME src) =>
+ (Output.error_msg (ML_Compiler.exn_message e); loop true src)
+ | (PGIP_QUIT,_) => ()
+ | (_,NONE) => ()
in
(* TODO: add socket interface *)