more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;

--- a/src/Pure/Concurrent/future.ML	Wed Jan 16 11:31:08 2013 +0100
+++ b/src/Pure/Concurrent/future.ML	Wed Jan 16 16:26:36 2013 +0100
@@ -439,7 +439,7 @@
   let
     val res =
       (case raw_res of
-        Exn.Exn exn => Exn.Exn (Par_Exn.set_serial exn)
+        Exn.Exn exn => Exn.Exn (Par_Exn.identify [] exn)
       | _ => raw_res);
     val _ = Single_Assignment.assign result res
       handle exn as Fail _ =>

--- a/src/Pure/Concurrent/par_exn.ML	Wed Jan 16 11:31:08 2013 +0100
+++ b/src/Pure/Concurrent/par_exn.ML	Wed Jan 16 16:26:36 2013 +0100
@@ -7,8 +7,8 @@
 
 signature PAR_EXN =
 sig
-  val serial: exn -> serial * exn
-  val set_serial: exn -> exn
+  val identify: Properties.entry list -> exn -> exn
+  val the_serial: exn -> int
   val make: exn list -> exn
   val dest: exn -> exn list option
   val is_interrupted: 'a Exn.result list -> bool
@@ -21,18 +21,17 @@
 
 (* identification via serial numbers *)
 
-fun serial exn =
-  (case get_exn_serial exn of
-    SOME i => (i, exn)
-  | NONE =>
-      let
-        val i = Library.serial ();
-        val exn' = uninterruptible (fn _ => set_exn_serial i) exn;
-      in (i, exn') end);
+fun identify default_props exn =
+  let
+    val props = Exn_Properties.get exn;
+    val update_serial =
+      if Properties.defined props Markup.serialN then []
+      else [(Markup.serialN, serial_string ())];
+    val update_props = filter_out (Properties.defined props o #1) default_props;
+  in Exn_Properties.update (update_serial @ update_props) exn end;
 
-fun set_serial exn = #2 (serial exn);
-
-val the_serial = the o get_exn_serial;
+fun the_serial exn =
+  Markup.parse_int (the (Properties.get (Exn_Properties.get exn) Markup.serialN));
 
 val exn_ord = rev_order o int_ord o pairself the_serial;
 
@@ -44,7 +43,7 @@
     no occurrences of Par_Exn or Exn.Interrupt*)
 
 fun par_exns (Par_Exn exns) = exns
-  | par_exns exn = if Exn.is_interrupt exn then [] else [set_serial exn];
+  | par_exns exn = if Exn.is_interrupt exn then [] else [identify [] exn];
 
 fun make exns =
   (case Ord_List.unions exn_ord (map par_exns exns) of

--- a/src/Pure/General/position.ML	Wed Jan 16 11:31:08 2013 +0100
+++ b/src/Pure/General/position.ML	Wed Jan 16 16:26:36 2013 +0100
@@ -26,6 +26,7 @@
   val id_only: string -> T
   val get_id: T -> string option
   val put_id: string -> T -> T
+  val parse_id: T -> int option
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
   val def_properties_of: T -> Properties.T
@@ -123,6 +124,8 @@
 fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
 fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
 
+fun parse_id pos = Option.map Markup.parse_int (get_id pos);
+
 
 (* markup properties *)
 

--- a/src/Pure/Isar/runtime.ML	Wed Jan 16 11:31:08 2013 +0100
+++ b/src/Pure/Isar/runtime.ML	Wed Jan 16 16:26:36 2013 +0100
@@ -47,6 +47,17 @@
 
 fun exn_messages exn_position e =
   let
+    fun identify exn =
+      let val exn' = Par_Exn.identify [] exn
+      in (Par_Exn.the_serial exn', exn') end;
+
+    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 => maps (flatten context) exns
+          | NONE => [(context, identify exn)]);
+
     fun raised exn name msgs =
       let val pos = Position.here (exn_position exn) in
         (case msgs of
@@ -55,13 +66,6 @@
         | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
       end;
 
-    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 => maps (flatten context) exns
-          | NONE => [(context, Par_Exn.serial exn)]);
-
     fun exn_msgs (context, (i, exn)) =
       (case exn of
         EXCURSION_FAIL (exn, loc) =>

--- a/src/Pure/ML-Systems/polyml.ML	Wed Jan 16 11:31:08 2013 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Jan 16 16:26:36 2013 +0100
@@ -11,22 +11,6 @@
     NONE => raise exn
   | SOME location => PolyML.raiseWithLocation (exn, location));
 
-fun set_exn_serial i exn = (*requires uninterruptible*)
-  let
-    val (file, startLine, endLine) =
-      (case PolyML.exceptionLocation exn of
-        NONE => ("", 0, 0)
-      | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine));
-    val location =
-      {file = file, startLine = startLine, endLine = endLine,
-        startPosition = ~ i, endPosition = 0};
-  in PolyML.raiseWithLocation (exn, location) handle e => e end;
-
-fun get_exn_serial exn =
-  (case Option.map #startPosition (PolyML.exceptionLocation exn) of
-    NONE => NONE
-  | SOME i => if i >= 0 then NONE else SOME (~ i));
-
 exception Interrupt = SML90.Interrupt;
 
 use "General/exn.ML";

--- a/src/Pure/ML-Systems/smlnj.ML	Wed Jan 16 11:31:08 2013 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Jan 16 16:26:36 2013 +0100
@@ -7,8 +7,6 @@
 
 exception Interrupt;
 fun reraise exn = raise exn;
-fun set_exn_serial (_: int) (exn: exn) = exn;
-fun get_exn_serial (exn: exn) : int option = NONE;
 
 use "ML-Systems/overloading_smlnj.ML";
 use "General/exn.ML";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/exn_properties_dummy.ML	Wed Jan 16 16:26:36 2013 +0100
@@ -0,0 +1,20 @@
+(*  Title:      Pure/ML/exn_properties_dummy.ML
+    Author:     Makarius
+
+Exception properties -- dummy version.
+*)
+
+signature EXN_PROPERTIES =
+sig
+  val get: exn -> Properties.T
+  val update: Properties.entry list -> exn -> exn
+end;
+
+structure Exn_Properties: EXN_PROPERTIES =
+struct
+
+fun get _ = [];
+fun update _ exn = exn;
+
+end;
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/exn_properties_polyml.ML	Wed Jan 16 16:26:36 2013 +0100
@@ -0,0 +1,50 @@
+(*  Title:      Pure/ML/exn_properties_polyml.ML
+    Author:     Makarius
+
+Exception properties for Poly/ML.
+*)
+
+signature EXN_PROPERTIES =
+sig
+  val of_location: PolyML.location -> Properties.T
+  val get: exn -> Properties.T
+  val update: Properties.entry list -> exn -> exn
+end;
+
+structure Exn_Properties: EXN_PROPERTIES =
+struct
+
+fun of_location (loc: PolyML.location) =
+  (case YXML.parse_body (#file loc) of
+    [] => []
+  | [XML.Text file] => [(Markup.fileN, file)]
+  | body => XML.Decode.properties body);
+
+fun get exn =
+  (case PolyML.exceptionLocation exn of
+    NONE => []
+  | SOME loc => of_location loc);
+
+fun update entries exn =
+  let
+    val loc =
+      the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
+        (PolyML.exceptionLocation exn);
+    val props = of_location loc;
+    val props' = fold Properties.put entries props;
+  in
+    if props = props' then exn
+    else
+      let
+        val loc' =
+          {file = YXML.string_of_body (XML.Encode.properties props'),
+            startLine = #startLine loc, endLine = #endLine loc,
+            startPosition = #startPosition loc, endPosition = #endPosition loc};
+      in
+        uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) ()
+          handle exn' => exn'
+      end
+  end;
+
+end;
+

--- a/src/Pure/ML/ml_compiler_polyml.ML	Wed Jan 16 11:31:08 2013 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Wed Jan 16 16:26:36 2013 +0100
@@ -11,12 +11,8 @@
 
 fun position_of (loc: PolyML.location) =
   let
-    val {file = text, startLine = line, startPosition = offset,
-      endLine = _, endPosition = end_offset} = loc;
-    val props =
-      (case YXML.parse text of
-        XML.Elem ((e, atts), _) => if e = Markup.positionN then atts else []
-      | XML.Text s => Position.file_name s);
+    val {startLine = line, startPosition = offset, endPosition = end_offset, ...} = loc;
+    val props = Exn_Properties.of_location loc;
   in
     Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
   end;
@@ -71,10 +67,7 @@
 
     (* input *)
 
-    val location_props =
-      op ^
-        (YXML.output_markup (Markup.position |> Markup.properties
-          (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))));
+    val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
 
     val input_buffer =
       Unsynchronized.ref (toks |> map

--- a/src/Pure/PIDE/command.ML	Wed Jan 16 11:31:08 2013 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Jan 16 16:26:36 2013 +0100
@@ -65,7 +65,7 @@
   (case Toplevel.transition int tr st of
     SOME (st', NONE) => ([], SOME st')
   | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
-  | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
+  | NONE => (ML_Compiler.exn_messages Runtime.TERMINATE, NONE));
 
 fun check_cmts tr cmts st =
   Toplevel.setmp_thread_position tr

--- a/src/Pure/ROOT	Wed Jan 16 11:31:08 2013 +0100
+++ b/src/Pure/ROOT	Wed Jan 16 16:26:36 2013 +0100
@@ -139,6 +139,8 @@
     "ML/ml_compiler_polyml.ML"
     "ML/ml_context.ML"
     "ML/ml_env.ML"
+    "ML/exn_properties_dummy.ML"
+    "ML/exn_properties_polyml.ML"
     "ML/ml_lex.ML"
     "ML/ml_parse.ML"
     "ML/ml_statistics_dummy.ML"

--- a/src/Pure/ROOT.ML	Wed Jan 16 11:31:08 2013 +0100
+++ b/src/Pure/ROOT.ML	Wed Jan 16 16:26:36 2013 +0100
@@ -70,6 +70,10 @@
 
 (* concurrency within the ML runtime *)
 
+if ML_System.is_polyml
+then use "ML/exn_properties_polyml.ML"
+else use "ML/exn_properties_dummy.ML";
+
 if ML_System.name = "polyml-5.5.0"
 then use "ML/ml_statistics_polyml-5.5.0.ML"
 else use "ML/ml_statistics_dummy.ML";

--- a/src/Pure/System/isabelle_process.ML	Wed Jan 16 11:31:08 2013 +0100
+++ b/src/Pure/System/isabelle_process.ML	Wed Jan 16 16:26:36 2013 +0100
@@ -74,17 +74,16 @@
   Synchronized.change command_tracing_messages (K Inttab.empty);
 
 fun update_tracing () =
-  (case Position.get_id (Position.thread_data ()) of
+  (case Position.parse_id (Position.thread_data ()) of
     NONE => ()
   | SOME id =>
       let
-        val i = Markup.parse_int id;
         val (n, ok) =
           Synchronized.change_result command_tracing_messages (fn tab =>
             let
-              val n = the_default 0 (Inttab.lookup tab i) + 1;
+              val n = the_default 0 (Inttab.lookup tab id) + 1;
               val ok = n <= ! tracing_messages;
-            in ((n, ok), Inttab.update (i, n) tab) end);
+            in ((n, ok), Inttab.update (id, n) tab) end);
       in
         if ok then ()
         else
@@ -97,7 +96,7 @@
               handle Fail _ => error "Stopped";
           in
             Synchronized.change command_tracing_messages
-              (Inttab.map_default (i, 0) (fn k => k - m))
+              (Inttab.map_default (id, 0) (fn k => k - m))
           end
       end);
 

--- a/src/Pure/goal.ML	Wed Jan 16 11:31:08 2013 +0100
+++ b/src/Pure/goal.ML	Wed Jan 16 16:26:36 2013 +0100
@@ -137,10 +137,7 @@
 fun fork_name name e =
   uninterruptible (fn _ => fn () =>
     let
-      val id =
-        (case Position.get_id (Position.thread_data ()) of
-          NONE => 0
-        | SOME id => Markup.parse_int id);
+      val id = the_default 0 (Position.parse_id (Position.thread_data ()));
       val _ = count_forked 1;
       val future =
         (singleton o Future.forks)