--- a/src/Pure/Isar/runtime.ML Wed Jan 16 11:31:08 2013 +0100
+++ b/src/Pure/Isar/runtime.ML Wed Jan 16 16:26:36 2013 +0100
@@ -47,6 +47,17 @@
fun exn_messages exn_position e =
let
+ fun identify exn =
+ let val exn' = Par_Exn.identify [] exn
+ in (Par_Exn.the_serial exn', exn') end;
+
+ fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
+ | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
+ | flatten context exn =
+ (case Par_Exn.dest exn of
+ SOME exns => maps (flatten context) exns
+ | NONE => [(context, identify exn)]);
+
fun raised exn name msgs =
let val pos = Position.here (exn_position exn) in
(case msgs of
@@ -55,13 +66,6 @@
| _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
end;
- fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
- | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
- | flatten context exn =
- (case Par_Exn.dest exn of
- SOME exns => maps (flatten context) exns
- | NONE => [(context, Par_Exn.serial exn)]);
-
fun exn_msgs (context, (i, exn)) =
(case exn of
EXCURSION_FAIL (exn, loc) =>