src/Pure/Isar/runtime.ML
changeset 44247 270366301bd7
parent 43761 e72ba84ae58f
child 44249 64620f1d6f87
equal deleted inserted replaced
44246:380a4677c55d 44247:270366301bd7
    58     val detailed = ! debug;
    58     val detailed = ! debug;
    59 
    59 
    60     fun exn_msgs context exn =
    60     fun exn_msgs context exn =
    61       if Exn.is_interrupt exn then []
    61       if Exn.is_interrupt exn then []
    62       else
    62       else
    63         (case exn of
    63         (case Par_Exn.dest exn of
    64           Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
    64           SOME exns => maps (exn_msgs context o #2) exns   (* FIXME include serial in message!? *)
    65         | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
    65         | NONE =>
    66         | EXCURSION_FAIL (exn, loc) =>
    66             (case exn of
    67             map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)) (exn_msgs context exn)
    67               Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
    68         | TERMINATE => ["Exit"]
    68             | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
    69         | TimeLimit.TimeOut => ["Timeout"]
    69             | EXCURSION_FAIL (exn, loc) =>
    70         | TOPLEVEL_ERROR => ["Error"]
    70                 map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc))
    71         | ERROR msg => [msg]
    71                   (exn_msgs context exn)
    72         | Fail msg => [raised exn "Fail" [msg]]
    72             | TERMINATE => ["Exit"]
    73         | THEORY (msg, thys) =>
    73             | TimeLimit.TimeOut => ["Timeout"]
    74             [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
    74             | TOPLEVEL_ERROR => ["Error"]
    75         | Ast.AST (msg, asts) =>
    75             | ERROR msg => [msg]
    76             [raised exn "AST" (msg ::
    76             | Fail msg => [raised exn "Fail" [msg]]
    77               (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
    77             | THEORY (msg, thys) =>
    78         | TYPE (msg, Ts, ts) =>
    78                 [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
    79             [raised exn "TYPE" (msg ::
    79             | Ast.AST (msg, asts) =>
    80               (if detailed then
    80                 [raised exn "AST" (msg ::
    81                 if_context context Syntax.string_of_typ Ts @
    81                   (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
    82                 if_context context Syntax.string_of_term ts
    82             | TYPE (msg, Ts, ts) =>
    83                else []))]
    83                 [raised exn "TYPE" (msg ::
    84         | TERM (msg, ts) =>
    84                   (if detailed then
    85             [raised exn "TERM" (msg ::
    85                     if_context context Syntax.string_of_typ Ts @
    86               (if detailed then if_context context Syntax.string_of_term ts else []))]
    86                     if_context context Syntax.string_of_term ts
    87         | THM (msg, i, thms) =>
    87                    else []))]
    88             [raised exn ("THM " ^ string_of_int i) (msg ::
    88             | TERM (msg, ts) =>
    89               (if detailed then if_context context Display.string_of_thm thms else []))]
    89                 [raised exn "TERM" (msg ::
    90         | _ => [raised exn (General.exnMessage exn) []]);
    90                   (if detailed then if_context context Syntax.string_of_term ts else []))]
       
    91             | THM (msg, i, thms) =>
       
    92                 [raised exn ("THM " ^ string_of_int i) (msg ::
       
    93                   (if detailed then if_context context Display.string_of_thm thms else []))]
       
    94             | _ => [raised exn (General.exnMessage exn) []]));
    91   in exn_msgs NONE e end;
    95   in exn_msgs NONE e end;
    92 
    96 
    93 fun exn_message exn_position exn =
    97 fun exn_message exn_position exn =
    94   (case exn_messages exn_position exn of
    98   (case exn_messages exn_position exn of
    95     [] => "Interrupt"
    99     [] => "Interrupt"