src/Pure/Isar/runtime.ML
changeset 50911 ee7fe4230642
parent 50505 33c92722cc3d
child 50914 fe4714886d92
     1.1 --- a/src/Pure/Isar/runtime.ML	Wed Jan 16 11:31:08 2013 +0100
     1.2 +++ b/src/Pure/Isar/runtime.ML	Wed Jan 16 16:26:36 2013 +0100
     1.3 @@ -47,6 +47,17 @@
     1.4  
     1.5  fun exn_messages exn_position e =
     1.6    let
     1.7 +    fun identify exn =
     1.8 +      let val exn' = Par_Exn.identify [] exn
     1.9 +      in (Par_Exn.the_serial exn', exn') end;
    1.10 +
    1.11 +    fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
    1.12 +      | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
    1.13 +      | flatten context exn =
    1.14 +          (case Par_Exn.dest exn of
    1.15 +            SOME exns => maps (flatten context) exns
    1.16 +          | NONE => [(context, identify exn)]);
    1.17 +
    1.18      fun raised exn name msgs =
    1.19        let val pos = Position.here (exn_position exn) in
    1.20          (case msgs of
    1.21 @@ -55,13 +66,6 @@
    1.22          | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
    1.23        end;
    1.24  
    1.25 -    fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
    1.26 -      | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
    1.27 -      | flatten context exn =
    1.28 -          (case Par_Exn.dest exn of
    1.29 -            SOME exns => maps (flatten context) exns
    1.30 -          | NONE => [(context, Par_Exn.serial exn)]);
    1.31 -
    1.32      fun exn_msgs (context, (i, exn)) =
    1.33        (case exn of
    1.34          EXCURSION_FAIL (exn, loc) =>