src/Pure/Isar/runtime.ML
author wenzelm
Wed, 16 Jan 2013 20:41:29 +0100
changeset 50914 fe4714886d92
parent 50911 ee7fe4230642
child 51242 a8e664e4fb5f
permissions -rw-r--r--
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/runtime.ML
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
     3
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
     4
Isar toplevel runtime support.
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
     5
*)
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
     6
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
     7
signature RUNTIME =
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
     8
sig
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
     9
  exception UNDEF
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    10
  exception TERMINATE
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    11
  exception EXCURSION_FAIL of exn * string
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    12
  exception TOPLEVEL_ERROR
39513
fce2202892c4 discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
wenzelm
parents: 39439
diff changeset
    13
  val debug: bool Unsynchronized.ref
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    14
  val exn_context: Proof.context option -> exn -> exn
50914
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    15
  val exn_messages_ids: (exn -> Position.T) -> exn -> ((serial * string) * string option) list
44270
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
    16
  val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    17
  val exn_message: (exn -> Position.T) -> exn -> string
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    18
  val debugging: ('a -> 'b) -> 'a -> 'b
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    19
  val controlled_execution: ('a -> 'b) -> 'a -> 'b
33603
3713a5208671 generalized Runtime.toplevel_error wrt. output function;
wenzelm
parents: 32091
diff changeset
    20
  val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    21
end;
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    22
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    23
structure Runtime: RUNTIME =
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    24
struct
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    25
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    26
(** exceptions **)
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    27
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    28
exception UNDEF;
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    29
exception TERMINATE;
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    30
exception EXCURSION_FAIL of exn * string;
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    31
exception TOPLEVEL_ERROR;
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    32
39513
fce2202892c4 discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
wenzelm
parents: 39439
diff changeset
    33
val debug = Unsynchronized.ref false;
fce2202892c4 discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
wenzelm
parents: 39439
diff changeset
    34
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    35
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    36
(* exn_context *)
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    37
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    38
exception CONTEXT of Proof.context * exn;
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    39
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    40
fun exn_context NONE exn = exn
39285
85728a4b5620 avoid extra wrapping for interrupts;
wenzelm
parents: 39238
diff changeset
    41
  | exn_context (SOME ctxt) exn = if Exn.is_interrupt exn then exn else CONTEXT (ctxt, exn);
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    42
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    43
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    44
(* exn_message *)
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    45
50914
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    46
local
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    47
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    48
fun if_context NONE _ _ = []
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    49
  | if_context (SOME ctxt) f xs = map (f ctxt) xs;
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    50
50914
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    51
fun identify exn =
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    52
  let
50914
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    53
    val exn' = Par_Exn.identify [] exn;
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    54
    val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN;
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    55
  in ((Par_Exn.the_serial exn', exn'), exec_id) end;
50911
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents: 50505
diff changeset
    56
50914
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    57
fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    58
  | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    59
  | flatten context exn =
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    60
      (case Par_Exn.dest exn of
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    61
        SOME exns => maps (flatten context) exns
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    62
      | NONE => [(context, identify exn)]);
50911
ee7fe4230642 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
wenzelm
parents: 50505
diff changeset
    63
50914
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    64
in
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    65
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    66
fun exn_messages_ids exn_position e =
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    67
  let
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    68
    fun raised exn name msgs =
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 45666
diff changeset
    69
      let val pos = Position.here (exn_position exn) in
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    70
        (case msgs of
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    71
          [] => "exception " ^ name ^ " raised" ^ pos
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    72
        | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    73
        | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    74
      end;
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
    75
50914
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    76
    fun exn_msgs (context, ((i, exn), id)) =
44270
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
    77
      (case exn of
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
    78
        EXCURSION_FAIL (exn, loc) =>
50914
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
    79
          map (fn ((i, msg), id) => ((i, msg ^ Markup.markup Markup.no_report ("\n" ^ loc)), id))
44270
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
    80
            (sorted_msgs context exn)
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
    81
      | _ =>
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
    82
        let
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
    83
          val msg =
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents: 43761
diff changeset
    84
            (case exn of
44270
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
    85
              TERMINATE => "Exit"
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
    86
            | TimeLimit.TimeOut => "Timeout"
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
    87
            | TOPLEVEL_ERROR => "Error"
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
    88
            | ERROR msg => msg
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
    89
            | Fail msg => raised exn "Fail" [msg]
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents: 43761
diff changeset
    90
            | THEORY (msg, thys) =>
45487
ae60518ac054 simplified Runtime.exn_messages: always print detailed version of low-level exeptions, which should not occur in regular user errors anyway;
wenzelm
parents: 45486
diff changeset
    91
                raised exn "THEORY" (msg :: map Context.str_of_thy thys)
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents: 43761
diff changeset
    92
            | Ast.AST (msg, asts) =>
45487
ae60518ac054 simplified Runtime.exn_messages: always print detailed version of low-level exeptions, which should not occur in regular user errors anyway;
wenzelm
parents: 45486
diff changeset
    93
                raised exn "AST" (msg :: map (Pretty.string_of o Ast.pretty_ast) asts)
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents: 43761
diff changeset
    94
            | TYPE (msg, Ts, ts) =>
44270
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
    95
                raised exn "TYPE" (msg ::
45487
ae60518ac054 simplified Runtime.exn_messages: always print detailed version of low-level exeptions, which should not occur in regular user errors anyway;
wenzelm
parents: 45486
diff changeset
    96
                  (if_context context Syntax.string_of_typ Ts @
ae60518ac054 simplified Runtime.exn_messages: always print detailed version of low-level exeptions, which should not occur in regular user errors anyway;
wenzelm
parents: 45486
diff changeset
    97
                    if_context context Syntax.string_of_term ts))
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents: 43761
diff changeset
    98
            | TERM (msg, ts) =>
45487
ae60518ac054 simplified Runtime.exn_messages: always print detailed version of low-level exeptions, which should not occur in regular user errors anyway;
wenzelm
parents: 45486
diff changeset
    99
                raised exn "TERM" (msg :: if_context context Syntax.string_of_term ts)
44247
270366301bd7 more systematic handling of parallel exceptions;
wenzelm
parents: 43761
diff changeset
   100
            | THM (msg, i, thms) =>
45487
ae60518ac054 simplified Runtime.exn_messages: always print detailed version of low-level exeptions, which should not occur in regular user errors anyway;
wenzelm
parents: 45486
diff changeset
   101
                raised exn ("THM " ^ string_of_int i)
ae60518ac054 simplified Runtime.exn_messages: always print detailed version of low-level exeptions, which should not occur in regular user errors anyway;
wenzelm
parents: 45486
diff changeset
   102
                  (msg :: if_context context Display.string_of_thm thms)
44270
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
   103
            | _ => raised exn (General.exnMessage exn) []);
50914
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
   104
        in [((i, msg), id)] end)
44270
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
   105
      and sorted_msgs context exn =
50914
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
   106
        sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
44270
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
   107
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
   108
  in sorted_msgs NONE e end;
38874
4a4d34d2f97b more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents: 37370
diff changeset
   109
50914
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
   110
end;
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
   111
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
   112
fun exn_messages exn_position exn =
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
   113
  map #1 (exn_messages_ids exn_position exn);
fe4714886d92 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents: 50911
diff changeset
   114
38874
4a4d34d2f97b more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents: 37370
diff changeset
   115
fun exn_message exn_position exn =
4a4d34d2f97b more careful treatment of nested multi-exceptions, collapsing cumulatively empty list to Interrupt;
wenzelm
parents: 37370
diff changeset
   116
  (case exn_messages exn_position exn of
38875
c7a66b584147 tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
wenzelm
parents: 38874
diff changeset
   117
    [] => "Interrupt"
44270
3eaad39e520c more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents: 44264
diff changeset
   118
  | msgs => cat_lines (map snd msgs));
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
   119
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
   120
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
   121
(** controlled execution **)
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
   122
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
   123
fun debugging f x =
45486
600682331b79 more detailed exception_trace: in Poly/ML 5.4.x intermediate handlers reset the trace (cf. Poly/ML SVN 1110);
wenzelm
parents: 45197
diff changeset
   124
  if ! debug
600682331b79 more detailed exception_trace: in Poly/ML 5.4.x intermediate handlers reset the trace (cf. Poly/ML SVN 1110);
wenzelm
parents: 45197
diff changeset
   125
  then exception_trace (fn () => f x)
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
   126
  else f x;
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
   127
41715
22f8c2483bd2 explicit Multithreading.interrupted to ensure that interrupts stay within the boundaries of managed evaluation blocks;
wenzelm
parents: 40318
diff changeset
   128
fun controlled_execution f x =
44295
e43f0ea90c9a more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;
wenzelm
parents: 44271
diff changeset
   129
  (f |> debugging |> Future.interruptible_task) x;
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
   130
39238
7189a138dd6c refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
wenzelm
parents: 39232
diff changeset
   131
fun toplevel_error output_exn f x = f x
7189a138dd6c refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
wenzelm
parents: 39232
diff changeset
   132
  handle exn =>
7189a138dd6c refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
wenzelm
parents: 39232
diff changeset
   133
    if Exn.is_interrupt exn then reraise exn
7189a138dd6c refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
wenzelm
parents: 39232
diff changeset
   134
    else
7189a138dd6c refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
wenzelm
parents: 39232
diff changeset
   135
      let
45197
b6c527c64789 more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
wenzelm
parents: 44295
diff changeset
   136
        val opt_ctxt =
b6c527c64789 more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
wenzelm
parents: 44295
diff changeset
   137
          (case Context.thread_data () of
b6c527c64789 more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
wenzelm
parents: 44295
diff changeset
   138
            NONE => NONE
b6c527c64789 more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
wenzelm
parents: 44295
diff changeset
   139
          | SOME context => try Context.proof_of context);
b6c527c64789 more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);
wenzelm
parents: 44295
diff changeset
   140
        val _ = output_exn (exn_context opt_ctxt exn);
39238
7189a138dd6c refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
wenzelm
parents: 39232
diff changeset
   141
      in raise TOPLEVEL_ERROR end;
31476
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
   142
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
   143
end;
c5d2899b6de9 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
diff changeset
   144