src/Pure/Isar/runtime.ML
changeset 59055 5a7157b8e870
parent 58894 447972249785
child 59056 cbe9563c03d1
     1.1 --- a/src/Pure/Isar/runtime.ML	Wed Nov 26 11:43:51 2014 +0100
     1.2 +++ b/src/Pure/Isar/runtime.ML	Wed Nov 26 14:35:55 2014 +0100
     1.3 @@ -7,7 +7,6 @@
     1.4  signature RUNTIME =
     1.5  sig
     1.6    exception UNDEF
     1.7 -  exception TERMINATE
     1.8    exception EXCURSION_FAIL of exn * string
     1.9    exception TOPLEVEL_ERROR
    1.10    val exn_context: Proof.context option -> exn -> exn
    1.11 @@ -30,7 +29,6 @@
    1.12  (** exceptions **)
    1.13  
    1.14  exception UNDEF;
    1.15 -exception TERMINATE;
    1.16  exception EXCURSION_FAIL of exn * string;
    1.17  exception TOPLEVEL_ERROR;
    1.18  
    1.19 @@ -96,8 +94,7 @@
    1.20          let
    1.21            val msg =
    1.22              (case exn of
    1.23 -              TERMINATE => "Exit"
    1.24 -            | TimeLimit.TimeOut => "Timeout"
    1.25 +              TimeLimit.TimeOut => "Timeout"
    1.26              | TOPLEVEL_ERROR => "Error"
    1.27              | ERROR "" => "Error"
    1.28              | ERROR msg => msg
    1.29 @@ -136,7 +133,7 @@
    1.30  
    1.31  val exn_error_message = Output.error_message o exn_message;
    1.32  val exn_system_message = Output.system_message o exn_message;
    1.33 -fun exn_trace e = print_exception_trace exn_message e;
    1.34 +fun exn_trace e = print_exception_trace exn_message tracing e;
    1.35  
    1.36  
    1.37  
    1.38 @@ -144,8 +141,7 @@
    1.39  
    1.40  fun debugging opt_context f x =
    1.41    if ML_Options.exception_trace_enabled opt_context
    1.42 -  then print_exception_trace exn_message (fn () => f x)
    1.43 -  else f x;
    1.44 +  then exn_trace (fn () => f x) else f x;
    1.45  
    1.46  fun controlled_execution opt_context f x =
    1.47    (f |> debugging opt_context |> Future.interruptible_task) x;