src/Pure/Isar/runtime.ML
changeset 39232 69c6d3e87660
parent 38875 c7a66b584147
child 39238 7189a138dd6c
     1.1 --- a/src/Pure/Isar/runtime.ML	Thu Sep 09 11:05:52 2010 +0200
     1.2 +++ b/src/Pure/Isar/runtime.ML	Thu Sep 09 17:20:27 2010 +0200
     1.3 @@ -54,30 +54,38 @@
     1.4  
     1.5      val detailed = ! Output.debugging;
     1.6  
     1.7 -    fun exn_msgs _ (CONTEXT (ctxt, exn)) = exn_msgs (SOME ctxt) exn
     1.8 -      | exn_msgs ctxt (Exn.EXCEPTIONS exns) = maps (exn_msgs ctxt) exns
     1.9 -      | exn_msgs ctxt (EXCURSION_FAIL (exn, loc)) =
    1.10 -          map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs ctxt exn)
    1.11 -      | exn_msgs _ TERMINATE = ["Exit"]
    1.12 -      | exn_msgs _ Exn.Interrupt = []
    1.13 -      | exn_msgs _ TimeLimit.TimeOut = ["Timeout"]
    1.14 -      | exn_msgs _ TOPLEVEL_ERROR = ["Error"]
    1.15 -      | exn_msgs _ (SYS_ERROR msg) = ["## SYSTEM ERROR ##\n" ^ msg]
    1.16 -      | exn_msgs _ (ERROR msg) = [msg]
    1.17 -      | exn_msgs _ (exn as Fail msg) = [raised exn "Fail" [msg]]
    1.18 -      | exn_msgs _ (exn as THEORY (msg, thys)) =
    1.19 -          [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
    1.20 -      | exn_msgs _ (exn as Syntax.AST (msg, asts)) = [raised exn "AST" (msg ::
    1.21 -            (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
    1.22 -      | exn_msgs ctxt (exn as TYPE (msg, Ts, ts)) = [raised exn "TYPE" (msg ::
    1.23 -            (if detailed then
    1.24 -              if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
    1.25 -             else []))]
    1.26 -      | exn_msgs ctxt (exn as TERM (msg, ts)) = [raised exn "TERM" (msg ::
    1.27 -            (if detailed then if_context ctxt Syntax.string_of_term ts else []))]
    1.28 -      | exn_msgs ctxt (exn as THM (msg, i, thms)) = [raised exn ("THM " ^ string_of_int i) (msg ::
    1.29 -            (if detailed then if_context ctxt Display.string_of_thm thms else []))]
    1.30 -      | exn_msgs _ exn = [raised exn (General.exnMessage exn) []];
    1.31 +    fun exn_msgs context exn =
    1.32 +      if Exn.is_interrupt exn then []
    1.33 +      else
    1.34 +        (case exn of
    1.35 +          Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
    1.36 +        | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
    1.37 +        | EXCURSION_FAIL (exn, loc) =>
    1.38 +            map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs context exn)
    1.39 +        | TERMINATE => ["Exit"]
    1.40 +        | TimeLimit.TimeOut => ["Timeout"]
    1.41 +        | TOPLEVEL_ERROR => ["Error"]
    1.42 +        | SYS_ERROR msg => ["## SYSTEM ERROR ##\n" ^ msg]
    1.43 +        | ERROR msg => [msg]
    1.44 +        | Fail msg => [raised exn "Fail" [msg]]
    1.45 +        | THEORY (msg, thys) =>
    1.46 +            [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
    1.47 +        | Syntax.AST (msg, asts) =>
    1.48 +            [raised exn "AST" (msg ::
    1.49 +              (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
    1.50 +        | TYPE (msg, Ts, ts) =>
    1.51 +            [raised exn "TYPE" (msg ::
    1.52 +              (if detailed then
    1.53 +                if_context context Syntax.string_of_typ Ts @
    1.54 +                if_context context Syntax.string_of_term ts
    1.55 +               else []))]
    1.56 +        | TERM (msg, ts) =>
    1.57 +            [raised exn "TERM" (msg ::
    1.58 +              (if detailed then if_context context Syntax.string_of_term ts else []))]
    1.59 +        | THM (msg, i, thms) =>
    1.60 +            [raised exn ("THM " ^ string_of_int i) (msg ::
    1.61 +              (if detailed then if_context context Display.string_of_thm thms else []))]
    1.62 +        | _ => [raised exn (General.exnMessage exn) []]);
    1.63    in exn_msgs NONE e end;
    1.64  
    1.65  fun exn_message exn_position exn =