src/Pure/Isar/toplevel.ML
changeset 56303 4cc3f4db3447
parent 56265 785569927666
child 56334 6b3739fee456
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Mar 27 13:00:40 2014 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Mar 27 17:12:40 2014 +0100
     1.3 @@ -29,10 +29,6 @@
     1.4    val interact: bool Unsynchronized.ref
     1.5    val timing: bool Unsynchronized.ref
     1.6    val profiling: int Unsynchronized.ref
     1.7 -  val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
     1.8 -  val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
     1.9 -  val program: (unit -> 'a) -> 'a
    1.10 -  val thread: bool -> (unit -> unit) -> Thread.thread
    1.11    type transition
    1.12    val empty: transition
    1.13    val print_of: transition -> bool
    1.14 @@ -232,26 +228,6 @@
    1.15  val profiling = Unsynchronized.ref 0;
    1.16  
    1.17  
    1.18 -(* controlled execution *)
    1.19 -
    1.20 -fun debugging arg = Runtime.debugging ML_Compiler.exn_message arg;
    1.21 -fun controlled_execution arg = Runtime.controlled_execution ML_Compiler.exn_message arg;
    1.22 -
    1.23 -fun program body =
    1.24 - (body
    1.25 -  |> controlled_execution NONE
    1.26 -  |> Runtime.toplevel_error ML_Compiler.exn_error_message) ();
    1.27 -
    1.28 -fun thread interrupts body =
    1.29 -  Thread.fork
    1.30 -    (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
    1.31 -        |> debugging NONE
    1.32 -        |> Runtime.toplevel_error
    1.33 -          (fn exn =>
    1.34 -            Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
    1.35 -      Simple_Thread.attributes interrupts);
    1.36 -
    1.37 -
    1.38  (* node transactions -- maintaining stable checkpoints *)
    1.39  
    1.40  exception FAILURE of state * exn;
    1.41 @@ -275,7 +251,7 @@
    1.42  
    1.43      val (result, err) =
    1.44        cont_node
    1.45 -      |> controlled_execution (SOME context) f
    1.46 +      |> Runtime.controlled_execution (SOME context) f
    1.47        |> state_error NONE
    1.48        handle exn => state_error (SOME exn) cont_node;
    1.49    in
    1.50 @@ -304,11 +280,11 @@
    1.51  local
    1.52  
    1.53  fun apply_tr _ (Init f) (State (NONE, _)) =
    1.54 -      State (SOME (Theory (Context.Theory (controlled_execution NONE f ()), NONE)), NONE)
    1.55 +      State (SOME (Theory (Context.Theory (Runtime.controlled_execution NONE f ()), NONE)), NONE)
    1.56    | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
    1.57        exit_transaction state
    1.58    | apply_tr int (Keep f) state =
    1.59 -      controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
    1.60 +      Runtime.controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
    1.61    | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
    1.62        apply_transaction (fn x => f int x) g state
    1.63    | apply_tr _ _ _ = raise UNDEF;
    1.64 @@ -649,8 +625,8 @@
    1.65  fun command_errors int tr st =
    1.66    (case transition int tr st of
    1.67      SOME (st', NONE) => ([], SOME st')
    1.68 -  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE)
    1.69 -  | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE));
    1.70 +  | SOME (_, SOME (exn, _)) => (Runtime.exn_messages_ids exn, NONE)
    1.71 +  | NONE => (Runtime.exn_messages_ids Runtime.TERMINATE, NONE));
    1.72  
    1.73  fun command_exception int tr st =
    1.74    (case transition int tr st of