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