# HG changeset patch # User wenzelm # Date 1257891483 -3600 # Node ID d4220df6fde2adcc5630d22c4cb5c4d1a92b6392 # Parent 3713a5208671be91c28c9808edbd544972a8248d Toplevel.thread provides Isar-style exception output; diff -r 3713a5208671 -r d4220df6fde2 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Nov 10 23:15:20 2009 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Nov 10 23:18:03 2009 +0100 @@ -119,7 +119,7 @@ fun check_thread_manager () = Synchronized.change global_state (fn state as {manager, timeout_heap, active, cancelling, messages, store} => if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state - else let val manager = SOME (SimpleThread.fork false (fn () => + else let val manager = SOME (Toplevel.thread false (fn () => let fun time_limit timeout_heap = (case try Thread_Heap.min timeout_heap of @@ -258,7 +258,7 @@ "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)); - val _ = SimpleThread.fork true (fn () => + val _ = Toplevel.thread true (fn () => let val _ = register birth_time death_time (Thread.self (), desc); val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal)); diff -r 3713a5208671 -r d4220df6fde2 src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Nov 10 23:15:20 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Nov 10 23:18:03 2009 +0100 @@ -427,7 +427,7 @@ |>> equal "genuine") in if auto orelse blocking then go () - else (SimpleThread.fork true (fn () => (go (); ())); (false, state)) + else (Toplevel.thread true (fn () => (go (); ())); (false, state)) end (* (TableFun().key * string list) list option * int option diff -r 3713a5208671 -r d4220df6fde2 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Tue Nov 10 23:15:20 2009 +0100 +++ b/src/Pure/Isar/toplevel.ML Tue Nov 10 23:18:03 2009 +0100 @@ -33,6 +33,7 @@ exception TERMINATE exception TOPLEVEL_ERROR val program: (unit -> 'a) -> 'a + val thread: bool -> (unit -> unit) -> Thread.thread type transition val empty: transition val init_of: transition -> string option @@ -226,10 +227,18 @@ exception EXCURSION_FAIL = Runtime.EXCURSION_FAIL; exception TOPLEVEL_ERROR = Runtime.TOPLEVEL_ERROR; -fun program f = - (f +fun program body = + (body |> Runtime.controlled_execution - |> Runtime.toplevel_error ML_Compiler.exn_message) (); + |> Runtime.toplevel_error (Output.error_msg o ML_Compiler.exn_message)) (); + +fun thread interrupts body = + Thread.fork + (((fn () => body () handle Exn.Interrupt => ()) + |> Runtime.debugging + |> Runtime.toplevel_error + (fn exn => priority ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))), + SimpleThread.attributes interrupts); (* node transactions -- maintaining stable checkpoints *)