src/Pure/Isar/runtime.ML
author wenzelm
Sun May 30 21:34:19 2010 +0200 (2010-05-30)
changeset 37198 3af985b10550
parent 33603 3713a5208671
child 37370 582780d89e64
permissions -rw-r--r--
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information;
fall back on ML_Context.eval_text if there is no position or no surrounding text;
proper Args.name_source_position for method "tactic" and "raw_tactic";
tuned;
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@31476
    13
  val exn_context: Proof.context option -> exn -> exn
wenzelm@31476
    14
  val exn_message: (exn -> Position.T) -> exn -> string
wenzelm@31476
    15
  val debugging: ('a -> 'b) -> 'a -> 'b
wenzelm@31476
    16
  val controlled_execution: ('a -> 'b) -> 'a -> 'b
wenzelm@33603
    17
  val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
wenzelm@31476
    18
end;
wenzelm@31476
    19
wenzelm@31476
    20
structure Runtime: RUNTIME =
wenzelm@31476
    21
struct
wenzelm@31476
    22
wenzelm@31476
    23
(** exceptions **)
wenzelm@31476
    24
wenzelm@31476
    25
exception UNDEF;
wenzelm@31476
    26
exception TERMINATE;
wenzelm@31476
    27
exception EXCURSION_FAIL of exn * string;
wenzelm@31476
    28
exception TOPLEVEL_ERROR;
wenzelm@31476
    29
wenzelm@31476
    30
wenzelm@31476
    31
(* exn_context *)
wenzelm@31476
    32
wenzelm@31476
    33
exception CONTEXT of Proof.context * exn;
wenzelm@31476
    34
wenzelm@31476
    35
fun exn_context NONE exn = exn
wenzelm@31476
    36
  | exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn);
wenzelm@31476
    37
wenzelm@31476
    38
wenzelm@31476
    39
(* exn_message *)
wenzelm@31476
    40
wenzelm@31476
    41
fun if_context NONE _ _ = []
wenzelm@31476
    42
  | if_context (SOME ctxt) f xs = map (f ctxt) xs;
wenzelm@31476
    43
wenzelm@31476
    44
fun exn_message exn_position e =
wenzelm@31476
    45
  let
wenzelm@31476
    46
    fun raised exn name msgs =
wenzelm@31476
    47
      let val pos = Position.str_of (exn_position exn) in
wenzelm@31476
    48
        (case msgs of
wenzelm@31476
    49
          [] => "exception " ^ name ^ " raised" ^ pos
wenzelm@31476
    50
        | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
wenzelm@31476
    51
        | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
wenzelm@31476
    52
      end;
wenzelm@31476
    53
wenzelm@31476
    54
    val detailed = ! Output.debugging;
wenzelm@31476
    55
wenzelm@31476
    56
    fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
wenzelm@31476
    57
      | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns)
wenzelm@31476
    58
      | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
wenzelm@31476
    59
          exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
wenzelm@31476
    60
      | exn_msg _ TERMINATE = "Exit."
wenzelm@31476
    61
      | exn_msg _ Exn.Interrupt = "Interrupt."
wenzelm@31476
    62
      | exn_msg _ TimeLimit.TimeOut = "Timeout."
wenzelm@31476
    63
      | exn_msg _ TOPLEVEL_ERROR = "Error."
wenzelm@31476
    64
      | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
wenzelm@31476
    65
      | exn_msg _ (ERROR msg) = msg
wenzelm@31476
    66
      | exn_msg _ (exn as Fail msg) = raised exn "Fail" [msg]
wenzelm@31476
    67
      | exn_msg _ (exn as THEORY (msg, thys)) =
wenzelm@31476
    68
          raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
wenzelm@31476
    69
      | exn_msg _ (exn as Syntax.AST (msg, asts)) = raised exn "AST" (msg ::
wenzelm@31476
    70
            (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))
wenzelm@31476
    71
      | exn_msg ctxt (exn as TYPE (msg, Ts, ts)) = raised exn "TYPE" (msg ::
wenzelm@31476
    72
            (if detailed then
wenzelm@31476
    73
              if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
wenzelm@31476
    74
             else []))
wenzelm@31476
    75
      | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg ::
wenzelm@31476
    76
            (if detailed then if_context ctxt Syntax.string_of_term ts else []))
wenzelm@31476
    77
      | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg ::
wenzelm@32091
    78
            (if detailed then if_context ctxt Display.string_of_thm thms else []))
wenzelm@31476
    79
      | exn_msg _ exn = raised exn (General.exnMessage exn) [];
wenzelm@31476
    80
  in exn_msg NONE e end;
wenzelm@31476
    81
wenzelm@31476
    82
wenzelm@31476
    83
wenzelm@31476
    84
(** controlled execution **)
wenzelm@31476
    85
wenzelm@31476
    86
fun debugging f x =
wenzelm@31476
    87
  if ! Output.debugging then
wenzelm@31476
    88
    Exn.release (exception_trace (fn () =>
wenzelm@31476
    89
      Exn.Result (f x) handle
wenzelm@31476
    90
        exn as UNDEF => Exn.Exn exn
wenzelm@31476
    91
      | exn as EXCURSION_FAIL _ => Exn.Exn exn))
wenzelm@31476
    92
  else f x;
wenzelm@31476
    93
wenzelm@31476
    94
fun controlled_execution f =
wenzelm@31476
    95
  f
wenzelm@31476
    96
  |> debugging
wenzelm@31476
    97
  |> Future.interruptible_task;
wenzelm@31476
    98
wenzelm@33603
    99
fun toplevel_error output_exn f x =
wenzelm@33603
   100
  let val ctxt = Option.map Context.proof_of (Context.thread_data ())
wenzelm@33603
   101
  in f x handle exn => (output_exn (exn_context ctxt exn); raise TOPLEVEL_ERROR) end;
wenzelm@31476
   102
wenzelm@31476
   103
end;
wenzelm@31476
   104