Toplevel.thread provides Isar-style exception output;
authorwenzelm
Tue Nov 10 23:18:03 2009 +0100 (2009-11-10 ago)
changeset 33604d4220df6fde2
parent 33603 3713a5208671
child 33605 f91ec14e20b6
Toplevel.thread provides Isar-style exception output;
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Nov 10 23:15:20 2009 +0100
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Nov 10 23:18:03 2009 +0100
     1.3 @@ -119,7 +119,7 @@
     1.4  fun check_thread_manager () = Synchronized.change global_state
     1.5    (fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
     1.6      if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
     1.7 -    else let val manager = SOME (SimpleThread.fork false (fn () =>
     1.8 +    else let val manager = SOME (Toplevel.thread false (fn () =>
     1.9        let
    1.10          fun time_limit timeout_heap =
    1.11            (case try Thread_Heap.min timeout_heap of
    1.12 @@ -258,7 +258,7 @@
    1.13            "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
    1.14              Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
    1.15  
    1.16 -        val _ = SimpleThread.fork true (fn () =>
    1.17 +        val _ = Toplevel.thread true (fn () =>
    1.18            let
    1.19              val _ = register birth_time death_time (Thread.self (), desc);
    1.20              val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal));
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Nov 10 23:15:20 2009 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Nov 10 23:18:03 2009 +0100
     2.3 @@ -427,7 +427,7 @@
     2.4                             |>> equal "genuine")
     2.5    in
     2.6      if auto orelse blocking then go ()
     2.7 -    else (SimpleThread.fork true (fn () => (go (); ())); (false, state))
     2.8 +    else (Toplevel.thread true (fn () => (go (); ())); (false, state))
     2.9    end
    2.10  
    2.11  (* (TableFun().key * string list) list option * int option
     3.1 --- a/src/Pure/Isar/toplevel.ML	Tue Nov 10 23:15:20 2009 +0100
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Nov 10 23:18:03 2009 +0100
     3.3 @@ -33,6 +33,7 @@
     3.4    exception TERMINATE
     3.5    exception TOPLEVEL_ERROR
     3.6    val program: (unit -> 'a) -> 'a
     3.7 +  val thread: bool -> (unit -> unit) -> Thread.thread
     3.8    type transition
     3.9    val empty: transition
    3.10    val init_of: transition -> string option
    3.11 @@ -226,10 +227,18 @@
    3.12  exception EXCURSION_FAIL = Runtime.EXCURSION_FAIL;
    3.13  exception TOPLEVEL_ERROR = Runtime.TOPLEVEL_ERROR;
    3.14  
    3.15 -fun program f =
    3.16 - (f
    3.17 +fun program body =
    3.18 + (body
    3.19    |> Runtime.controlled_execution
    3.20 -  |> Runtime.toplevel_error ML_Compiler.exn_message) ();
    3.21 +  |> Runtime.toplevel_error (Output.error_msg o ML_Compiler.exn_message)) ();
    3.22 +
    3.23 +fun thread interrupts body =
    3.24 +  Thread.fork
    3.25 +    (((fn () => body () handle Exn.Interrupt => ())
    3.26 +        |> Runtime.debugging
    3.27 +        |> Runtime.toplevel_error
    3.28 +          (fn exn => priority ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
    3.29 +      SimpleThread.attributes interrupts);
    3.30  
    3.31  
    3.32  (* node transactions -- maintaining stable checkpoints *)