# HG changeset patch # User wenzelm # Date 1284045627 -7200 # Node ID 69c6d3e87660610bc51186abf73479620e7bc68e # Parent 25c345302a1700ec0a6a912fb08d4359ade7e7de more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally; diff -r 25c345302a17 -r 69c6d3e87660 src/HOL/Mirabelle/Tools/mirabelle.ML --- 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 diff -r 25c345302a17 -r 69c6d3e87660 src/Pure/Concurrent/future.ML --- 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; diff -r 25c345302a17 -r 69c6d3e87660 src/Pure/Concurrent/lazy.ML --- 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) ()); diff -r 25c345302a17 -r 69c6d3e87660 src/Pure/Concurrent/lazy_sequential.ML --- 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); diff -r 25c345302a17 -r 69c6d3e87660 src/Pure/Concurrent/simple_thread.ML --- 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 _ => (); diff -r 25c345302a17 -r 69c6d3e87660 src/Pure/Concurrent/task_queue.ML --- 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 diff -r 25c345302a17 -r 69c6d3e87660 src/Pure/General/basics.ML --- 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); diff -r 25c345302a17 -r 69c6d3e87660 src/Pure/General/exn.ML --- 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 = diff -r 25c345302a17 -r 69c6d3e87660 src/Pure/Isar/proof.ML --- 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 diff -r 25c345302a17 -r 69c6d3e87660 src/Pure/Isar/runtime.ML --- 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 = diff -r 25c345302a17 -r 69c6d3e87660 src/Pure/Isar/toplevel.ML --- 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))), diff -r 25c345302a17 -r 69c6d3e87660 src/Pure/ML-Systems/multithreading_polyml.ML --- 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); diff -r 25c345302a17 -r 69c6d3e87660 src/Pure/ML-Systems/smlnj.ML --- 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; diff -r 25c345302a17 -r 69c6d3e87660 src/Pure/ML/ml_compiler_polyml-5.3.ML --- 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 () diff -r 25c345302a17 -r 69c6d3e87660 src/Pure/PIDE/document.ML --- 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; diff -r 25c345302a17 -r 69c6d3e87660 src/Pure/ProofGeneral/proof_general_pgip.ML --- 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 *)