src/Pure/Isar/runtime.ML
author wenzelm
Fri Apr 08 16:34:14 2011 +0200 (2011-04-08)
changeset 42290 b1f544c84040
parent 42224 578a51fae383
child 43761 e72ba84ae58f
permissions -rw-r--r--
discontinued special treatment of structure Lexicon;
wenzelm@31476
     1
(*  Title:      Pure/Isar/runtime.ML
wenzelm@31476
     2
    Author:     Makarius
wenzelm@31476
     3
wenzelm@31476
     4
Isar toplevel runtime support.
wenzelm@31476
     5
*)
wenzelm@31476
     6
wenzelm@31476
     7
signature RUNTIME =
wenzelm@31476
     8
sig
wenzelm@31476
     9
  exception UNDEF
wenzelm@31476
    10
  exception TERMINATE
wenzelm@31476
    11
  exception EXCURSION_FAIL of exn * string
wenzelm@31476
    12
  exception TOPLEVEL_ERROR
wenzelm@39513
    13
  val debug: bool Unsynchronized.ref
wenzelm@31476
    14
  val exn_context: Proof.context option -> exn -> exn
wenzelm@38874
    15
  val exn_messages: (exn -> Position.T) -> exn -> string list
wenzelm@31476
    16
  val exn_message: (exn -> Position.T) -> exn -> string
wenzelm@31476
    17
  val debugging: ('a -> 'b) -> 'a -> 'b
wenzelm@31476
    18
  val controlled_execution: ('a -> 'b) -> 'a -> 'b
wenzelm@33603
    19
  val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
wenzelm@31476
    20
end;
wenzelm@31476
    21
wenzelm@31476
    22
structure Runtime: RUNTIME =
wenzelm@31476
    23
struct
wenzelm@31476
    24
wenzelm@31476
    25
(** exceptions **)
wenzelm@31476
    26
wenzelm@31476
    27
exception UNDEF;
wenzelm@31476
    28
exception TERMINATE;
wenzelm@31476
    29
exception EXCURSION_FAIL of exn * string;
wenzelm@31476
    30
exception TOPLEVEL_ERROR;
wenzelm@31476
    31
wenzelm@39513
    32
val debug = Unsynchronized.ref false;
wenzelm@39513
    33
wenzelm@31476
    34
wenzelm@31476
    35
(* exn_context *)
wenzelm@31476
    36
wenzelm@31476
    37
exception CONTEXT of Proof.context * exn;
wenzelm@31476
    38
wenzelm@31476
    39
fun exn_context NONE exn = exn
wenzelm@39285
    40
  | exn_context (SOME ctxt) exn = if Exn.is_interrupt exn then exn else CONTEXT (ctxt, exn);
wenzelm@31476
    41
wenzelm@31476
    42
wenzelm@31476
    43
(* exn_message *)
wenzelm@31476
    44
wenzelm@31476
    45
fun if_context NONE _ _ = []
wenzelm@31476
    46
  | if_context (SOME ctxt) f xs = map (f ctxt) xs;
wenzelm@31476
    47
wenzelm@38874
    48
fun exn_messages exn_position e =
wenzelm@31476
    49
  let
wenzelm@31476
    50
    fun raised exn name msgs =
wenzelm@31476
    51
      let val pos = Position.str_of (exn_position exn) in
wenzelm@31476
    52
        (case msgs of
wenzelm@31476
    53
          [] => "exception " ^ name ^ " raised" ^ pos
wenzelm@31476
    54
        | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
wenzelm@31476
    55
        | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
wenzelm@31476
    56
      end;
wenzelm@31476
    57
wenzelm@39513
    58
    val detailed = ! debug;
wenzelm@31476
    59
wenzelm@39232
    60
    fun exn_msgs context exn =
wenzelm@39232
    61
      if Exn.is_interrupt exn then []
wenzelm@39232
    62
      else
wenzelm@39232
    63
        (case exn of
wenzelm@39232
    64
          Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
wenzelm@39232
    65
        | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
wenzelm@39232
    66
        | EXCURSION_FAIL (exn, loc) =>
wenzelm@39439
    67
            map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)) (exn_msgs context exn)
wenzelm@39232
    68
        | TERMINATE => ["Exit"]
wenzelm@39232
    69
        | TimeLimit.TimeOut => ["Timeout"]
wenzelm@39232
    70
        | TOPLEVEL_ERROR => ["Error"]
wenzelm@39232
    71
        | ERROR msg => [msg]
wenzelm@39232
    72
        | Fail msg => [raised exn "Fail" [msg]]
wenzelm@39232
    73
        | THEORY (msg, thys) =>
wenzelm@39232
    74
            [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
wenzelm@42224
    75
        | Ast.AST (msg, asts) =>
wenzelm@39232
    76
            [raised exn "AST" (msg ::
wenzelm@42224
    77
              (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
wenzelm@39232
    78
        | TYPE (msg, Ts, ts) =>
wenzelm@39232
    79
            [raised exn "TYPE" (msg ::
wenzelm@39232
    80
              (if detailed then
wenzelm@39232
    81
                if_context context Syntax.string_of_typ Ts @
wenzelm@39232
    82
                if_context context Syntax.string_of_term ts
wenzelm@39232
    83
               else []))]
wenzelm@39232
    84
        | TERM (msg, ts) =>
wenzelm@39232
    85
            [raised exn "TERM" (msg ::
wenzelm@39232
    86
              (if detailed then if_context context Syntax.string_of_term ts else []))]
wenzelm@39232
    87
        | THM (msg, i, thms) =>
wenzelm@39232
    88
            [raised exn ("THM " ^ string_of_int i) (msg ::
wenzelm@39232
    89
              (if detailed then if_context context Display.string_of_thm thms else []))]
wenzelm@39232
    90
        | _ => [raised exn (General.exnMessage exn) []]);
wenzelm@38874
    91
  in exn_msgs NONE e end;
wenzelm@38874
    92
wenzelm@38874
    93
fun exn_message exn_position exn =
wenzelm@38874
    94
  (case exn_messages exn_position exn of
wenzelm@38875
    95
    [] => "Interrupt"
wenzelm@38874
    96
  | msgs => cat_lines msgs);
wenzelm@31476
    97
wenzelm@31476
    98
wenzelm@31476
    99
(** controlled execution **)
wenzelm@31476
   100
wenzelm@31476
   101
fun debugging f x =
wenzelm@39513
   102
  if ! debug then
wenzelm@31476
   103
    Exn.release (exception_trace (fn () =>
wenzelm@31476
   104
      Exn.Result (f x) handle
wenzelm@31476
   105
        exn as UNDEF => Exn.Exn exn
wenzelm@31476
   106
      | exn as EXCURSION_FAIL _ => Exn.Exn exn))
wenzelm@31476
   107
  else f x;
wenzelm@31476
   108
wenzelm@41715
   109
fun controlled_execution f x =
wenzelm@41715
   110
  ((f |> debugging |> Future.interruptible_task) x before Multithreading.interrupted ());
wenzelm@31476
   111
wenzelm@39238
   112
fun toplevel_error output_exn f x = f x
wenzelm@39238
   113
  handle exn =>
wenzelm@39238
   114
    if Exn.is_interrupt exn then reraise exn
wenzelm@39238
   115
    else
wenzelm@39238
   116
      let
wenzelm@39238
   117
        val ctxt = Option.map Context.proof_of (Context.thread_data ());
wenzelm@39238
   118
        val _ = output_exn (exn_context ctxt exn);
wenzelm@39238
   119
      in raise TOPLEVEL_ERROR end;
wenzelm@31476
   120
wenzelm@31476
   121
end;
wenzelm@31476
   122