equal
deleted
inserted
replaced
50 |
50 |
51 fun identify exn = |
51 fun identify exn = |
52 let |
52 let |
53 val exn' = Par_Exn.identify [] exn; |
53 val exn' = Par_Exn.identify [] exn; |
54 val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN; |
54 val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN; |
55 in ((Par_Exn.the_serial exn', exn'), exec_id) end; |
55 val i = Par_Exn.the_serial exn' handle Option.Option => serial (); |
|
56 in ((i, exn'), exec_id) end; |
56 |
57 |
57 fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn |
58 fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn |
58 | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns |
59 | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns |
59 | flatten context exn = |
60 | flatten context exn = |
60 (case Par_Exn.dest exn of |
61 (case Par_Exn.dest exn of |