1.1 --- a/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 17:30:47 2011 +0200
     1.2 +++ b/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 17:53:32 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 -> exn list option
     1.8 +  val dest: exn -> (serial * 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 @@ -24,7 +24,9 @@
    1.13      SOME i => (i, exn)
    1.14    | NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end);
    1.15  
    1.16 -val exn_ord = rev_order o int_ord o pairself (the o get_exn_serial);
    1.17 +val the_serial = the o get_exn_serial;
    1.18 +
    1.19 +val exn_ord = rev_order o int_ord o pairself the_serial;
    1.20  
    1.21  
    1.22  (* parallel exceptions *)
    1.23 @@ -41,8 +43,8 @@
    1.24      [] => Exn.Interrupt
    1.25    | es => Par_Exn es);
    1.26  
    1.27 -fun dest (Par_Exn exns) = SOME exns
    1.28 -  | dest _ = NONE;
    1.29 +fun dest (Par_Exn exns) = SOME (map (`the_serial) exns)
    1.30 +  | dest exn = if Exn.is_interrupt exn then SOME [] else NONE;
    1.31  
    1.32  
    1.33  (* parallel results *)

     2.1 --- a/src/Pure/General/output.ML	Thu Aug 18 17:30:47 2011 +0200
     2.2 +++ b/src/Pure/General/output.ML	Thu Aug 18 17:53:32 2011 +0200
     2.3 @@ -31,13 +31,14 @@
     2.4      val urgent_message_fn: (output -> unit) Unsynchronized.ref
     2.5      val tracing_fn: (output -> unit) Unsynchronized.ref
     2.6      val warning_fn: (output -> unit) Unsynchronized.ref
     2.7 -    val error_fn: (output -> unit) Unsynchronized.ref
     2.8 +    val error_fn: (serial * output -> unit) Unsynchronized.ref
     2.9      val prompt_fn: (output -> unit) Unsynchronized.ref
    2.10      val status_fn: (output -> unit) Unsynchronized.ref
    2.11      val report_fn: (output -> unit) Unsynchronized.ref
    2.12      val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
    2.13    end
    2.14    val urgent_message: string -> unit
    2.15 +  val error_msg': serial * string -> unit
    2.16    val error_msg: string -> unit
    2.17    val prompt: string -> unit
    2.18    val status: string -> unit
    2.19 @@ -92,7 +93,8 @@
    2.20    val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    2.21    val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    2.22    val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
    2.23 -  val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
    2.24 +  val error_fn =
    2.25 +    Unsynchronized.ref (fn (_: serial, s) => raw_stdout (suffix "\n" (prefix_lines "*** " s)));
    2.26    val prompt_fn = Unsynchronized.ref raw_stdout;
    2.27    val status_fn = Unsynchronized.ref (fn _: output => ());
    2.28    val report_fn = Unsynchronized.ref (fn _: output => ());
    2.29 @@ -104,7 +106,8 @@
    2.30  fun urgent_message s = ! Private_Hooks.urgent_message_fn (output s);
    2.31  fun tracing s = ! Private_Hooks.tracing_fn (output s);
    2.32  fun warning s = ! Private_Hooks.warning_fn (output s);
    2.33 -fun error_msg s = ! Private_Hooks.error_fn (output s);
    2.34 +fun error_msg' (i, s) = ! Private_Hooks.error_fn (i, output s);
    2.35 +fun error_msg s = error_msg' (serial (), s);
    2.36  fun prompt s = ! Private_Hooks.prompt_fn (output s);
    2.37  fun status s = ! Private_Hooks.status_fn (output s);
    2.38  fun report s = ! Private_Hooks.report_fn (output s);

     3.1 --- a/src/Pure/Isar/runtime.ML	Thu Aug 18 17:30:47 2011 +0200
     3.2 +++ b/src/Pure/Isar/runtime.ML	Thu Aug 18 17:53:32 2011 +0200
     3.3 @@ -12,7 +12,7 @@
     3.4    exception TOPLEVEL_ERROR
     3.5    val debug: bool Unsynchronized.ref
     3.6    val exn_context: Proof.context option -> exn -> exn
     3.7 -  val exn_messages: (exn -> Position.T) -> exn -> string list
     3.8 +  val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list
     3.9    val exn_message: (exn -> Position.T) -> exn -> string
    3.10    val debugging: ('a -> 'b) -> 'a -> 'b
    3.11    val controlled_execution: ('a -> 'b) -> 'a -> 'b
    3.12 @@ -57,47 +57,55 @@
    3.13  
    3.14      val detailed = ! debug;
    3.15  
    3.16 -    fun exn_msgs context exn =
    3.17 -      if Exn.is_interrupt exn then []
    3.18 -      else
    3.19 -        (case Par_Exn.dest exn of
    3.20 -          SOME exns => maps (exn_msgs context) (rev exns)
    3.21 -        | NONE =>
    3.22 +    fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
    3.23 +      | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
    3.24 +      | flatten context exn =
    3.25 +          (case Par_Exn.dest exn of
    3.26 +            SOME exns => map (pair context) exns
    3.27 +          | NONE => [(context, Par_Exn.serial exn)]);
    3.28 +
    3.29 +    fun exn_msgs (context, (i, exn)) =
    3.30 +      (case exn of
    3.31 +        EXCURSION_FAIL (exn, loc) =>
    3.32 +          map (apsnd (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)))
    3.33 +            (sorted_msgs context exn)
    3.34 +      | _ =>
    3.35 +        let
    3.36 +          val msg =
    3.37              (case exn of
    3.38 -              Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
    3.39 -            | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
    3.40 -            | EXCURSION_FAIL (exn, loc) =>
    3.41 -                map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc))
    3.42 -                  (exn_msgs context exn)
    3.43 -            | TERMINATE => ["Exit"]
    3.44 -            | TimeLimit.TimeOut => ["Timeout"]
    3.45 -            | TOPLEVEL_ERROR => ["Error"]
    3.46 -            | ERROR msg => [msg]
    3.47 -            | Fail msg => [raised exn "Fail" [msg]]
    3.48 +              TERMINATE => "Exit"
    3.49 +            | TimeLimit.TimeOut => "Timeout"
    3.50 +            | TOPLEVEL_ERROR => "Error"
    3.51 +            | ERROR msg => msg
    3.52 +            | Fail msg => raised exn "Fail" [msg]
    3.53              | THEORY (msg, thys) =>
    3.54 -                [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
    3.55 +                raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
    3.56              | Ast.AST (msg, asts) =>
    3.57 -                [raised exn "AST" (msg ::
    3.58 -                  (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
    3.59 +                raised exn "AST" (msg ::
    3.60 +                  (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))
    3.61              | TYPE (msg, Ts, ts) =>
    3.62 -                [raised exn "TYPE" (msg ::
    3.63 +                raised exn "TYPE" (msg ::
    3.64                    (if detailed then
    3.65                      if_context context Syntax.string_of_typ Ts @
    3.66                      if_context context Syntax.string_of_term ts
    3.67 -                   else []))]
    3.68 +                   else []))
    3.69              | TERM (msg, ts) =>
    3.70 -                [raised exn "TERM" (msg ::
    3.71 -                  (if detailed then if_context context Syntax.string_of_term ts else []))]
    3.72 +                raised exn "TERM" (msg ::
    3.73 +                  (if detailed then if_context context Syntax.string_of_term ts else []))
    3.74              | THM (msg, i, thms) =>
    3.75 -                [raised exn ("THM " ^ string_of_int i) (msg ::
    3.76 -                  (if detailed then if_context context Display.string_of_thm thms else []))]
    3.77 -            | _ => [raised exn (General.exnMessage exn) []]));
    3.78 -  in exn_msgs NONE e end;
    3.79 +                raised exn ("THM " ^ string_of_int i) (msg ::
    3.80 +                  (if detailed then if_context context Display.string_of_thm thms else []))
    3.81 +            | _ => raised exn (General.exnMessage exn) []);
    3.82 +        in [(i, msg)] end)
    3.83 +      and sorted_msgs context exn =
    3.84 +        sort (int_ord o pairself fst) (maps exn_msgs (flatten context exn));
    3.85 +
    3.86 +  in sorted_msgs NONE e end;
    3.87  
    3.88  fun exn_message exn_position exn =
    3.89    (case exn_messages exn_position exn of
    3.90      [] => "Interrupt"
    3.91 -  | msgs => cat_lines msgs);
    3.92 +  | msgs => cat_lines (map snd msgs));
    3.93  
    3.94  
    3.95  (** controlled execution **)

     4.1 --- a/src/Pure/Isar/toplevel.ML	Thu Aug 18 17:30:47 2011 +0200
     4.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Aug 18 17:53:32 2011 +0200
     4.3 @@ -84,7 +84,7 @@
     4.4    val unknown_context: transition -> transition
     4.5    val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
     4.6    val status: transition -> Markup.T -> unit
     4.7 -  val error_msg: transition -> string -> unit
     4.8 +  val error_msg: transition -> serial * string -> unit
     4.9    val add_hook: (transition -> state -> state -> unit) -> unit
    4.10    val transition: bool -> transition -> state -> (state * (exn * string) option) option
    4.11    val command: transition -> state -> state
    4.12 @@ -567,7 +567,7 @@
    4.13    setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
    4.14  
    4.15  fun error_msg tr msg =
    4.16 -  setmp_thread_position tr (fn () => Output.error_msg msg) ();
    4.17 +  setmp_thread_position tr (fn () => Output.error_msg' msg) ();
    4.18  
    4.19  
    4.20  (* post-transition hooks *)

     5.1 --- a/src/Pure/ML/ml_compiler.ML	Thu Aug 18 17:30:47 2011 +0200
     5.2 +++ b/src/Pure/ML/ml_compiler.ML	Thu Aug 18 17:53:32 2011 +0200
     5.3 @@ -7,7 +7,7 @@
     5.4  signature ML_COMPILER =
     5.5  sig
     5.6    val exn_position: exn -> Position.T
     5.7 -  val exn_messages: exn -> string list
     5.8 +  val exn_messages: exn -> (serial * string) list
     5.9    val exn_message: exn -> string
    5.10    val eval: bool -> Position.T -> ML_Lex.token list -> unit
    5.11  end

     6.1 --- a/src/Pure/PIDE/document.ML	Thu Aug 18 17:30:47 2011 +0200
     6.2 +++ b/src/Pure/PIDE/document.ML	Thu Aug 18 17:53:32 2011 +0200
     6.3 @@ -268,7 +268,7 @@
     6.4        (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
     6.5          [] => Exn.interrupt ()
     6.6        | errs => (errs, NONE))
     6.7 -  | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
     6.8 +  | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
     6.9  
    6.10  in
    6.11  

     7.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Aug 18 17:30:47 2011 +0200
     7.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Aug 18 17:53:32 2011 +0200
     7.3 @@ -84,7 +84,7 @@
     7.4    Output.Private_Hooks.urgent_message_fn := message (special "I") (special "J") "";
     7.5    Output.Private_Hooks.tracing_fn := message (special "I" ^ special "V") (special "J") "";
     7.6    Output.Private_Hooks.warning_fn := message (special "K") (special "L") "### ";
     7.7 -  Output.Private_Hooks.error_fn := message (special "M") (special "N") "*** ";
     7.8 +  Output.Private_Hooks.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
     7.9    Output.Private_Hooks.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
    7.10  
    7.11  fun panic s =

     8.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Aug 18 17:30:47 2011 +0200
     8.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Aug 18 17:53:32 2011 +0200
     8.3 @@ -166,7 +166,7 @@
     8.4    Output.Private_Hooks.urgent_message_fn := (fn s => normalmsg Status s);
     8.5    Output.Private_Hooks.tracing_fn := (fn s => normalmsg Tracing s);
     8.6    Output.Private_Hooks.warning_fn := (fn s => errormsg Message Warning s);
     8.7 -  Output.Private_Hooks.error_fn := (fn s => errormsg Message Fatal s));
     8.8 +  Output.Private_Hooks.error_fn := (fn (_, s) => errormsg Message Fatal s));
     8.9  
    8.10  
    8.11  (* immediate messages *)

     9.1 --- a/src/Pure/System/isabelle_process.ML	Thu Aug 18 17:30:47 2011 +0200
     9.2 +++ b/src/Pure/System/isabelle_process.ML	Thu Aug 18 17:53:32 2011 +0200
     9.3 @@ -72,11 +72,11 @@
     9.4      val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
     9.5    in Mailbox.send mbox (chunk header @ chunk body) end;
     9.6  
     9.7 -fun standard_message mbox with_serial ch body =
     9.8 +fun standard_message mbox opt_serial ch body =
     9.9    if body = "" then ()
    9.10    else
    9.11      message mbox ch
    9.12 -      ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
    9.13 +      ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
    9.14          (Position.properties_of (Position.thread_data ()))) body;
    9.15  
    9.16  fun message_output mbox out_stream =
    9.17 @@ -103,12 +103,12 @@
    9.18      val mbox = Mailbox.create () : string list Mailbox.T;
    9.19      val _ = Simple_Thread.fork false (message_output mbox out_stream);
    9.20    in
    9.21 -    Output.Private_Hooks.status_fn := standard_message mbox false "B";
    9.22 -    Output.Private_Hooks.report_fn := standard_message mbox false "C";
    9.23 -    Output.Private_Hooks.writeln_fn := standard_message mbox true "D";
    9.24 -    Output.Private_Hooks.tracing_fn := standard_message mbox true "E";
    9.25 -    Output.Private_Hooks.warning_fn := standard_message mbox true "F";
    9.26 -    Output.Private_Hooks.error_fn := standard_message mbox true "G";
    9.27 +    Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
    9.28 +    Output.Private_Hooks.report_fn := standard_message mbox NONE "C";
    9.29 +    Output.Private_Hooks.writeln_fn := (fn s => standard_message mbox (SOME (serial ())) "D" s);
    9.30 +    Output.Private_Hooks.tracing_fn := (fn s => standard_message mbox (SOME (serial ())) "E" s);
    9.31 +    Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
    9.32 +    Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
    9.33      Output.Private_Hooks.raw_message_fn := message mbox "H";
    9.34      Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
    9.35      Output.Private_Hooks.prompt_fn := ignore;

    10.1 --- a/src/Pure/System/isar.ML	Thu Aug 18 17:30:47 2011 +0200
    10.2 +++ b/src/Pure/System/isar.ML	Thu Aug 18 17:53:32 2011 +0200
    10.3 @@ -96,7 +96,7 @@
    10.4      NONE => false
    10.5    | SOME (_, SOME exn_info) =>
    10.6       (set_exn (SOME exn_info);
    10.7 -      Toplevel.error_msg tr (ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
    10.8 +      Toplevel.error_msg tr (serial (), ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
    10.9        true)
   10.10    | SOME (st', NONE) =>
   10.11        let