src/Pure/Isar/toplevel.ML
changeset 33604 d4220df6fde2
parent 33553 35f2b30593a8
child 33671 4b0f2599ed48
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Nov 10 23:15:20 2009 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Nov 10 23:18:03 2009 +0100
     1.3 @@ -33,6 +33,7 @@
     1.4    exception TERMINATE
     1.5    exception TOPLEVEL_ERROR
     1.6    val program: (unit -> 'a) -> 'a
     1.7 +  val thread: bool -> (unit -> unit) -> Thread.thread
     1.8    type transition
     1.9    val empty: transition
    1.10    val init_of: transition -> string option
    1.11 @@ -226,10 +227,18 @@
    1.12  exception EXCURSION_FAIL = Runtime.EXCURSION_FAIL;
    1.13  exception TOPLEVEL_ERROR = Runtime.TOPLEVEL_ERROR;
    1.14  
    1.15 -fun program f =
    1.16 - (f
    1.17 +fun program body =
    1.18 + (body
    1.19    |> Runtime.controlled_execution
    1.20 -  |> Runtime.toplevel_error ML_Compiler.exn_message) ();
    1.21 +  |> Runtime.toplevel_error (Output.error_msg o ML_Compiler.exn_message)) ();
    1.22 +
    1.23 +fun thread interrupts body =
    1.24 +  Thread.fork
    1.25 +    (((fn () => body () handle Exn.Interrupt => ())
    1.26 +        |> Runtime.debugging
    1.27 +        |> Runtime.toplevel_error
    1.28 +          (fn exn => priority ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
    1.29 +      SimpleThread.attributes interrupts);
    1.30  
    1.31  
    1.32  (* node transactions -- maintaining stable checkpoints *)