1.1 --- a/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 17:53:32 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 18:07:40 2011 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  sig
     1.5    val serial: exn -> serial * exn
     1.6    val make: exn list -> exn
     1.7 -  val dest: exn -> (serial * exn) list option
     1.8 +  val dest: exn -> exn list option
     1.9    val release_all: 'a Exn.result list -> 'a list
    1.10    val release_first: 'a Exn.result list -> 'a list
    1.11  end;
    1.12 @@ -43,7 +43,7 @@
    1.13      [] => Exn.Interrupt
    1.14    | es => Par_Exn es);
    1.15  
    1.16 -fun dest (Par_Exn exns) = SOME (map (`the_serial) exns)
    1.17 +fun dest (Par_Exn exns) = SOME exns
    1.18    | dest exn = if Exn.is_interrupt exn then SOME [] else NONE;
    1.19  
    1.20  

     2.1 --- a/src/Pure/Isar/runtime.ML	Thu Aug 18 17:53:32 2011 +0200
     2.2 +++ b/src/Pure/Isar/runtime.ML	Thu Aug 18 18:07:40 2011 +0200
     2.3 @@ -61,7 +61,7 @@
     2.4        | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
     2.5        | flatten context exn =
     2.6            (case Par_Exn.dest exn of
     2.7 -            SOME exns => map (pair context) exns
     2.8 +            SOME exns => maps (flatten context) exns
     2.9            | NONE => [(context, Par_Exn.serial exn)]);
    2.10  
    2.11      fun exn_msgs (context, (i, exn)) =
    2.12 @@ -98,7 +98,7 @@
    2.13              | _ => raised exn (General.exnMessage exn) []);
    2.14          in [(i, msg)] end)
    2.15        and sorted_msgs context exn =
    2.16 -        sort (int_ord o pairself fst) (maps exn_msgs (flatten context exn));
    2.17 +        sort_distinct (int_ord o pairself fst) (maps exn_msgs (flatten context exn));
    2.18  
    2.19    in sorted_msgs NONE e end;
    2.20  

     3.1 --- a/src/Pure/PIDE/document.ML	Thu Aug 18 17:53:32 2011 +0200
     3.2 +++ b/src/Pure/PIDE/document.ML	Thu Aug 18 18:07:40 2011 +0200
     3.3 @@ -264,8 +264,8 @@
     3.4  fun run int tr st =
     3.5    (case Toplevel.transition int tr st of
     3.6      SOME (st', NONE) => ([], SOME st')
     3.7 -  | SOME (_, SOME exn_info) =>
     3.8 -      (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
     3.9 +  | SOME (_, SOME (exn, _)) =>
    3.10 +      (case ML_Compiler.exn_messages exn of
    3.11          [] => Exn.interrupt ()
    3.12        | errs => (errs, NONE))
    3.13    | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));