src/Pure/Isar/runtime.ML
changeset 44270 3eaad39e520c
parent 44264 c21ecbb028b6
child 44271 89f40a5939b2
     1.1 --- a/src/Pure/Isar/runtime.ML	Thu Aug 18 17:30:47 2011 +0200
     1.2 +++ b/src/Pure/Isar/runtime.ML	Thu Aug 18 17:53:32 2011 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    exception TOPLEVEL_ERROR
     1.5    val debug: bool Unsynchronized.ref
     1.6    val exn_context: Proof.context option -> exn -> exn
     1.7 -  val exn_messages: (exn -> Position.T) -> exn -> string list
     1.8 +  val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list
     1.9    val exn_message: (exn -> Position.T) -> exn -> string
    1.10    val debugging: ('a -> 'b) -> 'a -> 'b
    1.11    val controlled_execution: ('a -> 'b) -> 'a -> 'b
    1.12 @@ -57,47 +57,55 @@
    1.13  
    1.14      val detailed = ! debug;
    1.15  
    1.16 -    fun exn_msgs context exn =
    1.17 -      if Exn.is_interrupt exn then []
    1.18 -      else
    1.19 -        (case Par_Exn.dest exn of
    1.20 -          SOME exns => maps (exn_msgs context) (rev exns)
    1.21 -        | NONE =>
    1.22 +    fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
    1.23 +      | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
    1.24 +      | flatten context exn =
    1.25 +          (case Par_Exn.dest exn of
    1.26 +            SOME exns => map (pair context) exns
    1.27 +          | NONE => [(context, Par_Exn.serial exn)]);
    1.28 +
    1.29 +    fun exn_msgs (context, (i, exn)) =
    1.30 +      (case exn of
    1.31 +        EXCURSION_FAIL (exn, loc) =>
    1.32 +          map (apsnd (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)))
    1.33 +            (sorted_msgs context exn)
    1.34 +      | _ =>
    1.35 +        let
    1.36 +          val msg =
    1.37              (case exn of
    1.38 -              Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
    1.39 -            | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
    1.40 -            | EXCURSION_FAIL (exn, loc) =>
    1.41 -                map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc))
    1.42 -                  (exn_msgs context exn)
    1.43 -            | TERMINATE => ["Exit"]
    1.44 -            | TimeLimit.TimeOut => ["Timeout"]
    1.45 -            | TOPLEVEL_ERROR => ["Error"]
    1.46 -            | ERROR msg => [msg]
    1.47 -            | Fail msg => [raised exn "Fail" [msg]]
    1.48 +              TERMINATE => "Exit"
    1.49 +            | TimeLimit.TimeOut => "Timeout"
    1.50 +            | TOPLEVEL_ERROR => "Error"
    1.51 +            | ERROR msg => msg
    1.52 +            | Fail msg => raised exn "Fail" [msg]
    1.53              | THEORY (msg, thys) =>
    1.54 -                [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
    1.55 +                raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
    1.56              | Ast.AST (msg, asts) =>
    1.57 -                [raised exn "AST" (msg ::
    1.58 -                  (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
    1.59 +                raised exn "AST" (msg ::
    1.60 +                  (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))
    1.61              | TYPE (msg, Ts, ts) =>
    1.62 -                [raised exn "TYPE" (msg ::
    1.63 +                raised exn "TYPE" (msg ::
    1.64                    (if detailed then
    1.65                      if_context context Syntax.string_of_typ Ts @
    1.66                      if_context context Syntax.string_of_term ts
    1.67 -                   else []))]
    1.68 +                   else []))
    1.69              | TERM (msg, ts) =>
    1.70 -                [raised exn "TERM" (msg ::
    1.71 -                  (if detailed then if_context context Syntax.string_of_term ts else []))]
    1.72 +                raised exn "TERM" (msg ::
    1.73 +                  (if detailed then if_context context Syntax.string_of_term ts else []))
    1.74              | THM (msg, i, thms) =>
    1.75 -                [raised exn ("THM " ^ string_of_int i) (msg ::
    1.76 -                  (if detailed then if_context context Display.string_of_thm thms else []))]
    1.77 -            | _ => [raised exn (General.exnMessage exn) []]));
    1.78 -  in exn_msgs NONE e end;
    1.79 +                raised exn ("THM " ^ string_of_int i) (msg ::
    1.80 +                  (if detailed then if_context context Display.string_of_thm thms else []))
    1.81 +            | _ => raised exn (General.exnMessage exn) []);
    1.82 +        in [(i, msg)] end)
    1.83 +      and sorted_msgs context exn =
    1.84 +        sort (int_ord o pairself fst) (maps exn_msgs (flatten context exn));
    1.85 +
    1.86 +  in sorted_msgs NONE e end;
    1.87  
    1.88  fun exn_message exn_position exn =
    1.89    (case exn_messages exn_position exn of
    1.90      [] => "Interrupt"
    1.91 -  | msgs => cat_lines msgs);
    1.92 +  | msgs => cat_lines (map snd msgs));
    1.93  
    1.94  
    1.95  (** controlled execution **)