# HG changeset patch
# User wenzelm
# Date 1313682812 -7200
# Node ID 3eaad39e520c22d81c1c82598ea960155c9350b7
# Parent  3ff2fd162aeed58e88f44eae59105add1c6fef5c
more careful treatment of exception serial numbers, with propagation to message channel;

diff -r 3ff2fd162aee -r 3eaad39e520c src/Pure/Concurrent/par_exn.ML
--- a/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 17:30:47 2011 +0200
+++ b/src/Pure/Concurrent/par_exn.ML	Thu Aug 18 17:53:32 2011 +0200
@@ -9,7 +9,7 @@
 sig
   val serial: exn -> serial * exn
   val make: exn list -> exn
-  val dest: exn -> exn list option
+  val dest: exn -> (serial * exn) list option
   val release_all: 'a Exn.result list -> 'a list
   val release_first: 'a Exn.result list -> 'a list
 end;
@@ -24,7 +24,9 @@
     SOME i => (i, exn)
   | NONE => let val i = Library.serial () in (i, set_exn_serial i exn) end);
 
-val exn_ord = rev_order o int_ord o pairself (the o get_exn_serial);
+val the_serial = the o get_exn_serial;
+
+val exn_ord = rev_order o int_ord o pairself the_serial;
 
 
 (* parallel exceptions *)
@@ -41,8 +43,8 @@
     [] => Exn.Interrupt
   | es => Par_Exn es);
 
-fun dest (Par_Exn exns) = SOME exns
-  | dest _ = NONE;
+fun dest (Par_Exn exns) = SOME (map (`the_serial) exns)
+  | dest exn = if Exn.is_interrupt exn then SOME [] else NONE;
 
 
 (* parallel results *)
diff -r 3ff2fd162aee -r 3eaad39e520c src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Thu Aug 18 17:30:47 2011 +0200
+++ b/src/Pure/General/output.ML	Thu Aug 18 17:53:32 2011 +0200
@@ -31,13 +31,14 @@
     val urgent_message_fn: (output -> unit) Unsynchronized.ref
     val tracing_fn: (output -> unit) Unsynchronized.ref
     val warning_fn: (output -> unit) Unsynchronized.ref
-    val error_fn: (output -> unit) Unsynchronized.ref
+    val error_fn: (serial * output -> unit) Unsynchronized.ref
     val prompt_fn: (output -> unit) Unsynchronized.ref
     val status_fn: (output -> unit) Unsynchronized.ref
     val report_fn: (output -> unit) Unsynchronized.ref
     val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
   end
   val urgent_message: string -> unit
+  val error_msg': serial * string -> unit
   val error_msg: string -> unit
   val prompt: string -> unit
   val status: string -> unit
@@ -92,7 +93,8 @@
   val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
   val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
   val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
-  val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
+  val error_fn =
+    Unsynchronized.ref (fn (_: serial, s) => raw_stdout (suffix "\n" (prefix_lines "*** " s)));
   val prompt_fn = Unsynchronized.ref raw_stdout;
   val status_fn = Unsynchronized.ref (fn _: output => ());
   val report_fn = Unsynchronized.ref (fn _: output => ());
@@ -104,7 +106,8 @@
 fun urgent_message s = ! Private_Hooks.urgent_message_fn (output s);
 fun tracing s = ! Private_Hooks.tracing_fn (output s);
 fun warning s = ! Private_Hooks.warning_fn (output s);
-fun error_msg s = ! Private_Hooks.error_fn (output s);
+fun error_msg' (i, s) = ! Private_Hooks.error_fn (i, output s);
+fun error_msg s = error_msg' (serial (), s);
 fun prompt s = ! Private_Hooks.prompt_fn (output s);
 fun status s = ! Private_Hooks.status_fn (output s);
 fun report s = ! Private_Hooks.report_fn (output s);
diff -r 3ff2fd162aee -r 3eaad39e520c src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Thu Aug 18 17:30:47 2011 +0200
+++ b/src/Pure/Isar/runtime.ML	Thu Aug 18 17:53:32 2011 +0200
@@ -12,7 +12,7 @@
   exception TOPLEVEL_ERROR
   val debug: bool Unsynchronized.ref
   val exn_context: Proof.context option -> exn -> exn
-  val exn_messages: (exn -> Position.T) -> exn -> string list
+  val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list
   val exn_message: (exn -> Position.T) -> exn -> string
   val debugging: ('a -> 'b) -> 'a -> 'b
   val controlled_execution: ('a -> 'b) -> 'a -> 'b
@@ -57,47 +57,55 @@
 
     val detailed = ! debug;
 
-    fun exn_msgs context exn =
-      if Exn.is_interrupt exn then []
-      else
-        (case Par_Exn.dest exn of
-          SOME exns => maps (exn_msgs context) (rev exns)
-        | NONE =>
+    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 => map (pair context) exns
+          | NONE => [(context, Par_Exn.serial exn)]);
+
+    fun exn_msgs (context, (i, exn)) =
+      (case exn of
+        EXCURSION_FAIL (exn, loc) =>
+          map (apsnd (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)))
+            (sorted_msgs context exn)
+      | _ =>
+        let
+          val msg =
             (case exn of
-              Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
-            | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
-            | EXCURSION_FAIL (exn, loc) =>
-                map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc))
-                  (exn_msgs context exn)
-            | TERMINATE => ["Exit"]
-            | TimeLimit.TimeOut => ["Timeout"]
-            | TOPLEVEL_ERROR => ["Error"]
-            | ERROR msg => [msg]
-            | Fail msg => [raised exn "Fail" [msg]]
+              TERMINATE => "Exit"
+            | TimeLimit.TimeOut => "Timeout"
+            | TOPLEVEL_ERROR => "Error"
+            | ERROR msg => msg
+            | Fail msg => raised exn "Fail" [msg]
             | THEORY (msg, thys) =>
-                [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
+                raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
             | Ast.AST (msg, asts) =>
-                [raised exn "AST" (msg ::
-                  (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
+                raised exn "AST" (msg ::
+                  (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))
             | TYPE (msg, Ts, ts) =>
-                [raised exn "TYPE" (msg ::
+                raised exn "TYPE" (msg ::
                   (if detailed then
                     if_context context Syntax.string_of_typ Ts @
                     if_context context Syntax.string_of_term ts
-                   else []))]
+                   else []))
             | TERM (msg, ts) =>
-                [raised exn "TERM" (msg ::
-                  (if detailed then if_context context Syntax.string_of_term ts else []))]
+                raised exn "TERM" (msg ::
+                  (if detailed then if_context context Syntax.string_of_term ts else []))
             | THM (msg, i, thms) =>
-                [raised exn ("THM " ^ string_of_int i) (msg ::
-                  (if detailed then if_context context Display.string_of_thm thms else []))]
-            | _ => [raised exn (General.exnMessage exn) []]));
-  in exn_msgs NONE e end;
+                raised exn ("THM " ^ string_of_int i) (msg ::
+                  (if detailed then if_context context Display.string_of_thm thms else []))
+            | _ => raised exn (General.exnMessage exn) []);
+        in [(i, msg)] end)
+      and sorted_msgs context exn =
+        sort (int_ord o pairself fst) (maps exn_msgs (flatten context exn));
+
+  in sorted_msgs NONE e end;
 
 fun exn_message exn_position exn =
   (case exn_messages exn_position exn of
     [] => "Interrupt"
-  | msgs => cat_lines msgs);
+  | msgs => cat_lines (map snd msgs));
 
 
 (** controlled execution **)
diff -r 3ff2fd162aee -r 3eaad39e520c src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Aug 18 17:30:47 2011 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Aug 18 17:53:32 2011 +0200
@@ -84,7 +84,7 @@
   val unknown_context: transition -> transition
   val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
   val status: transition -> Markup.T -> unit
-  val error_msg: transition -> string -> unit
+  val error_msg: transition -> serial * string -> unit
   val add_hook: (transition -> state -> state -> unit) -> unit
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val command: transition -> state -> state
@@ -567,7 +567,7 @@
   setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
 
 fun error_msg tr msg =
-  setmp_thread_position tr (fn () => Output.error_msg msg) ();
+  setmp_thread_position tr (fn () => Output.error_msg' msg) ();
 
 
 (* post-transition hooks *)
diff -r 3ff2fd162aee -r 3eaad39e520c src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Thu Aug 18 17:30:47 2011 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Thu Aug 18 17:53:32 2011 +0200
@@ -7,7 +7,7 @@
 signature ML_COMPILER =
 sig
   val exn_position: exn -> Position.T
-  val exn_messages: exn -> string list
+  val exn_messages: exn -> (serial * string) list
   val exn_message: exn -> string
   val eval: bool -> Position.T -> ML_Lex.token list -> unit
 end
diff -r 3ff2fd162aee -r 3eaad39e520c src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Aug 18 17:30:47 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Aug 18 17:53:32 2011 +0200
@@ -268,7 +268,7 @@
       (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
         [] => Exn.interrupt ()
       | errs => (errs, NONE))
-  | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
+  | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
 
 in
 
diff -r 3ff2fd162aee -r 3eaad39e520c src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Aug 18 17:30:47 2011 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Aug 18 17:53:32 2011 +0200
@@ -84,7 +84,7 @@
   Output.Private_Hooks.urgent_message_fn := message (special "I") (special "J") "";
   Output.Private_Hooks.tracing_fn := message (special "I" ^ special "V") (special "J") "";
   Output.Private_Hooks.warning_fn := message (special "K") (special "L") "### ";
-  Output.Private_Hooks.error_fn := message (special "M") (special "N") "*** ";
+  Output.Private_Hooks.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
   Output.Private_Hooks.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
 
 fun panic s =
diff -r 3ff2fd162aee -r 3eaad39e520c src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Aug 18 17:30:47 2011 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Aug 18 17:53:32 2011 +0200
@@ -166,7 +166,7 @@
   Output.Private_Hooks.urgent_message_fn := (fn s => normalmsg Status s);
   Output.Private_Hooks.tracing_fn := (fn s => normalmsg Tracing s);
   Output.Private_Hooks.warning_fn := (fn s => errormsg Message Warning s);
-  Output.Private_Hooks.error_fn := (fn s => errormsg Message Fatal s));
+  Output.Private_Hooks.error_fn := (fn (_, s) => errormsg Message Fatal s));
 
 
 (* immediate messages *)
diff -r 3ff2fd162aee -r 3eaad39e520c src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Thu Aug 18 17:30:47 2011 +0200
+++ b/src/Pure/System/isabelle_process.ML	Thu Aug 18 17:53:32 2011 +0200
@@ -72,11 +72,11 @@
     val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
   in Mailbox.send mbox (chunk header @ chunk body) end;
 
-fun standard_message mbox with_serial ch body =
+fun standard_message mbox opt_serial ch body =
   if body = "" then ()
   else
     message mbox ch
-      ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
+      ((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
         (Position.properties_of (Position.thread_data ()))) body;
 
 fun message_output mbox out_stream =
@@ -103,12 +103,12 @@
     val mbox = Mailbox.create () : string list Mailbox.T;
     val _ = Simple_Thread.fork false (message_output mbox out_stream);
   in
-    Output.Private_Hooks.status_fn := standard_message mbox false "B";
-    Output.Private_Hooks.report_fn := standard_message mbox false "C";
-    Output.Private_Hooks.writeln_fn := standard_message mbox true "D";
-    Output.Private_Hooks.tracing_fn := standard_message mbox true "E";
-    Output.Private_Hooks.warning_fn := standard_message mbox true "F";
-    Output.Private_Hooks.error_fn := standard_message mbox true "G";
+    Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
+    Output.Private_Hooks.report_fn := standard_message mbox NONE "C";
+    Output.Private_Hooks.writeln_fn := (fn s => standard_message mbox (SOME (serial ())) "D" s);
+    Output.Private_Hooks.tracing_fn := (fn s => standard_message mbox (SOME (serial ())) "E" s);
+    Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
+    Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
     Output.Private_Hooks.raw_message_fn := message mbox "H";
     Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
     Output.Private_Hooks.prompt_fn := ignore;
diff -r 3ff2fd162aee -r 3eaad39e520c src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Thu Aug 18 17:30:47 2011 +0200
+++ b/src/Pure/System/isar.ML	Thu Aug 18 17:53:32 2011 +0200
@@ -96,7 +96,7 @@
     NONE => false
   | SOME (_, SOME exn_info) =>
      (set_exn (SOME exn_info);
-      Toplevel.error_msg tr (ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
+      Toplevel.error_msg tr (serial (), ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
       true)
   | SOME (st', NONE) =>
       let