src/Pure/Isar/runtime.ML
author wenzelm
Mon May 03 14:25:56 2010 +0200 (2010-05-03)
changeset 36610 bafd82950e24
parent 33603 3713a5208671
child 37370 582780d89e64
permissions -rw-r--r--
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
     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 exn_context: Proof.context option -> exn -> exn
    14   val exn_message: (exn -> Position.T) -> exn -> string
    15   val debugging: ('a -> 'b) -> 'a -> 'b
    16   val controlled_execution: ('a -> 'b) -> 'a -> 'b
    17   val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
    18 end;
    19 
    20 structure Runtime: RUNTIME =
    21 struct
    22 
    23 (** exceptions **)
    24 
    25 exception UNDEF;
    26 exception TERMINATE;
    27 exception EXCURSION_FAIL of exn * string;
    28 exception TOPLEVEL_ERROR;
    29 
    30 
    31 (* exn_context *)
    32 
    33 exception CONTEXT of Proof.context * exn;
    34 
    35 fun exn_context NONE exn = exn
    36   | exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn);
    37 
    38 
    39 (* exn_message *)
    40 
    41 fun if_context NONE _ _ = []
    42   | if_context (SOME ctxt) f xs = map (f ctxt) xs;
    43 
    44 fun exn_message exn_position e =
    45   let
    46     fun raised exn name msgs =
    47       let val pos = Position.str_of (exn_position exn) in
    48         (case msgs of
    49           [] => "exception " ^ name ^ " raised" ^ pos
    50         | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
    51         | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
    52       end;
    53 
    54     val detailed = ! Output.debugging;
    55 
    56     fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
    57       | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns)
    58       | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
    59           exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
    60       | exn_msg _ TERMINATE = "Exit."
    61       | exn_msg _ Exn.Interrupt = "Interrupt."
    62       | exn_msg _ TimeLimit.TimeOut = "Timeout."
    63       | exn_msg _ TOPLEVEL_ERROR = "Error."
    64       | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
    65       | exn_msg _ (ERROR msg) = msg
    66       | exn_msg _ (exn as Fail msg) = raised exn "Fail" [msg]
    67       | exn_msg _ (exn as THEORY (msg, thys)) =
    68           raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
    69       | exn_msg _ (exn as Syntax.AST (msg, asts)) = raised exn "AST" (msg ::
    70             (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))
    71       | exn_msg ctxt (exn as TYPE (msg, Ts, ts)) = raised exn "TYPE" (msg ::
    72             (if detailed then
    73               if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
    74              else []))
    75       | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg ::
    76             (if detailed then if_context ctxt Syntax.string_of_term ts else []))
    77       | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg ::
    78             (if detailed then if_context ctxt Display.string_of_thm thms else []))
    79       | exn_msg _ exn = raised exn (General.exnMessage exn) [];
    80   in exn_msg NONE e end;
    81 
    82 
    83 
    84 (** controlled execution **)
    85 
    86 fun debugging f x =
    87   if ! Output.debugging then
    88     Exn.release (exception_trace (fn () =>
    89       Exn.Result (f x) handle
    90         exn as UNDEF => Exn.Exn exn
    91       | exn as EXCURSION_FAIL _ => Exn.Exn exn))
    92   else f x;
    93 
    94 fun controlled_execution f =
    95   f
    96   |> debugging
    97   |> Future.interruptible_task;
    98 
    99 fun toplevel_error output_exn f x =
   100   let val ctxt = Option.map Context.proof_of (Context.thread_data ())
   101   in f x handle exn => (output_exn (exn_context ctxt exn); raise TOPLEVEL_ERROR) end;
   102 
   103 end;
   104