more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
authorwenzelm
Wed Jan 16 16:26:36 2013 +0100 (2013-01-16)
changeset 50911ee7fe4230642
parent 50910 54f06ba192ef
child 50912 8d391f185cac
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/par_exn.ML
src/Pure/General/position.ML
src/Pure/Isar/runtime.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ML/exn_properties_dummy.ML
src/Pure/ML/exn_properties_polyml.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/PIDE/command.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/isabelle_process.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Wed Jan 16 11:31:08 2013 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Wed Jan 16 16:26:36 2013 +0100
     1.3 @@ -439,7 +439,7 @@
     1.4    let
     1.5      val res =
     1.6        (case raw_res of
     1.7 -        Exn.Exn exn => Exn.Exn (Par_Exn.set_serial exn)
     1.8 +        Exn.Exn exn => Exn.Exn (Par_Exn.identify [] exn)
     1.9        | _ => raw_res);
    1.10      val _ = Single_Assignment.assign result res
    1.11        handle exn as Fail _ =>
     2.1 --- a/src/Pure/Concurrent/par_exn.ML	Wed Jan 16 11:31:08 2013 +0100
     2.2 +++ b/src/Pure/Concurrent/par_exn.ML	Wed Jan 16 16:26:36 2013 +0100
     2.3 @@ -7,8 +7,8 @@
     2.4  
     2.5  signature PAR_EXN =
     2.6  sig
     2.7 -  val serial: exn -> serial * exn
     2.8 -  val set_serial: exn -> exn
     2.9 +  val identify: Properties.entry list -> exn -> exn
    2.10 +  val the_serial: exn -> int
    2.11    val make: exn list -> exn
    2.12    val dest: exn -> exn list option
    2.13    val is_interrupted: 'a Exn.result list -> bool
    2.14 @@ -21,18 +21,17 @@
    2.15  
    2.16  (* identification via serial numbers *)
    2.17  
    2.18 -fun serial exn =
    2.19 -  (case get_exn_serial exn of
    2.20 -    SOME i => (i, exn)
    2.21 -  | NONE =>
    2.22 -      let
    2.23 -        val i = Library.serial ();
    2.24 -        val exn' = uninterruptible (fn _ => set_exn_serial i) exn;
    2.25 -      in (i, exn') end);
    2.26 +fun identify default_props exn =
    2.27 +  let
    2.28 +    val props = Exn_Properties.get exn;
    2.29 +    val update_serial =
    2.30 +      if Properties.defined props Markup.serialN then []
    2.31 +      else [(Markup.serialN, serial_string ())];
    2.32 +    val update_props = filter_out (Properties.defined props o #1) default_props;
    2.33 +  in Exn_Properties.update (update_serial @ update_props) exn end;
    2.34  
    2.35 -fun set_serial exn = #2 (serial exn);
    2.36 -
    2.37 -val the_serial = the o get_exn_serial;
    2.38 +fun the_serial exn =
    2.39 +  Markup.parse_int (the (Properties.get (Exn_Properties.get exn) Markup.serialN));
    2.40  
    2.41  val exn_ord = rev_order o int_ord o pairself the_serial;
    2.42  
    2.43 @@ -44,7 +43,7 @@
    2.44      no occurrences of Par_Exn or Exn.Interrupt*)
    2.45  
    2.46  fun par_exns (Par_Exn exns) = exns
    2.47 -  | par_exns exn = if Exn.is_interrupt exn then [] else [set_serial exn];
    2.48 +  | par_exns exn = if Exn.is_interrupt exn then [] else [identify [] exn];
    2.49  
    2.50  fun make exns =
    2.51    (case Ord_List.unions exn_ord (map par_exns exns) of
     3.1 --- a/src/Pure/General/position.ML	Wed Jan 16 11:31:08 2013 +0100
     3.2 +++ b/src/Pure/General/position.ML	Wed Jan 16 16:26:36 2013 +0100
     3.3 @@ -26,6 +26,7 @@
     3.4    val id_only: string -> T
     3.5    val get_id: T -> string option
     3.6    val put_id: string -> T -> T
     3.7 +  val parse_id: T -> int option
     3.8    val of_properties: Properties.T -> T
     3.9    val properties_of: T -> Properties.T
    3.10    val def_properties_of: T -> Properties.T
    3.11 @@ -123,6 +124,8 @@
    3.12  fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
    3.13  fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
    3.14  
    3.15 +fun parse_id pos = Option.map Markup.parse_int (get_id pos);
    3.16 +
    3.17  
    3.18  (* markup properties *)
    3.19  
     4.1 --- a/src/Pure/Isar/runtime.ML	Wed Jan 16 11:31:08 2013 +0100
     4.2 +++ b/src/Pure/Isar/runtime.ML	Wed Jan 16 16:26:36 2013 +0100
     4.3 @@ -47,6 +47,17 @@
     4.4  
     4.5  fun exn_messages exn_position e =
     4.6    let
     4.7 +    fun identify exn =
     4.8 +      let val exn' = Par_Exn.identify [] exn
     4.9 +      in (Par_Exn.the_serial exn', exn') end;
    4.10 +
    4.11 +    fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
    4.12 +      | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
    4.13 +      | flatten context exn =
    4.14 +          (case Par_Exn.dest exn of
    4.15 +            SOME exns => maps (flatten context) exns
    4.16 +          | NONE => [(context, identify exn)]);
    4.17 +
    4.18      fun raised exn name msgs =
    4.19        let val pos = Position.here (exn_position exn) in
    4.20          (case msgs of
    4.21 @@ -55,13 +66,6 @@
    4.22          | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
    4.23        end;
    4.24  
    4.25 -    fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
    4.26 -      | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
    4.27 -      | flatten context exn =
    4.28 -          (case Par_Exn.dest exn of
    4.29 -            SOME exns => maps (flatten context) exns
    4.30 -          | NONE => [(context, Par_Exn.serial exn)]);
    4.31 -
    4.32      fun exn_msgs (context, (i, exn)) =
    4.33        (case exn of
    4.34          EXCURSION_FAIL (exn, loc) =>
     5.1 --- a/src/Pure/ML-Systems/polyml.ML	Wed Jan 16 11:31:08 2013 +0100
     5.2 +++ b/src/Pure/ML-Systems/polyml.ML	Wed Jan 16 16:26:36 2013 +0100
     5.3 @@ -11,22 +11,6 @@
     5.4      NONE => raise exn
     5.5    | SOME location => PolyML.raiseWithLocation (exn, location));
     5.6  
     5.7 -fun set_exn_serial i exn = (*requires uninterruptible*)
     5.8 -  let
     5.9 -    val (file, startLine, endLine) =
    5.10 -      (case PolyML.exceptionLocation exn of
    5.11 -        NONE => ("", 0, 0)
    5.12 -      | SOME {file, startLine, endLine, startPosition, ...} => (file, startLine, endLine));
    5.13 -    val location =
    5.14 -      {file = file, startLine = startLine, endLine = endLine,
    5.15 -        startPosition = ~ i, endPosition = 0};
    5.16 -  in PolyML.raiseWithLocation (exn, location) handle e => e end;
    5.17 -
    5.18 -fun get_exn_serial exn =
    5.19 -  (case Option.map #startPosition (PolyML.exceptionLocation exn) of
    5.20 -    NONE => NONE
    5.21 -  | SOME i => if i >= 0 then NONE else SOME (~ i));
    5.22 -
    5.23  exception Interrupt = SML90.Interrupt;
    5.24  
    5.25  use "General/exn.ML";
     6.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Jan 16 11:31:08 2013 +0100
     6.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Jan 16 16:26:36 2013 +0100
     6.3 @@ -7,8 +7,6 @@
     6.4  
     6.5  exception Interrupt;
     6.6  fun reraise exn = raise exn;
     6.7 -fun set_exn_serial (_: int) (exn: exn) = exn;
     6.8 -fun get_exn_serial (exn: exn) : int option = NONE;
     6.9  
    6.10  use "ML-Systems/overloading_smlnj.ML";
    6.11  use "General/exn.ML";
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/ML/exn_properties_dummy.ML	Wed Jan 16 16:26:36 2013 +0100
     7.3 @@ -0,0 +1,20 @@
     7.4 +(*  Title:      Pure/ML/exn_properties_dummy.ML
     7.5 +    Author:     Makarius
     7.6 +
     7.7 +Exception properties -- dummy version.
     7.8 +*)
     7.9 +
    7.10 +signature EXN_PROPERTIES =
    7.11 +sig
    7.12 +  val get: exn -> Properties.T
    7.13 +  val update: Properties.entry list -> exn -> exn
    7.14 +end;
    7.15 +
    7.16 +structure Exn_Properties: EXN_PROPERTIES =
    7.17 +struct
    7.18 +
    7.19 +fun get _ = [];
    7.20 +fun update _ exn = exn;
    7.21 +
    7.22 +end;
    7.23 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Pure/ML/exn_properties_polyml.ML	Wed Jan 16 16:26:36 2013 +0100
     8.3 @@ -0,0 +1,50 @@
     8.4 +(*  Title:      Pure/ML/exn_properties_polyml.ML
     8.5 +    Author:     Makarius
     8.6 +
     8.7 +Exception properties for Poly/ML.
     8.8 +*)
     8.9 +
    8.10 +signature EXN_PROPERTIES =
    8.11 +sig
    8.12 +  val of_location: PolyML.location -> Properties.T
    8.13 +  val get: exn -> Properties.T
    8.14 +  val update: Properties.entry list -> exn -> exn
    8.15 +end;
    8.16 +
    8.17 +structure Exn_Properties: EXN_PROPERTIES =
    8.18 +struct
    8.19 +
    8.20 +fun of_location (loc: PolyML.location) =
    8.21 +  (case YXML.parse_body (#file loc) of
    8.22 +    [] => []
    8.23 +  | [XML.Text file] => [(Markup.fileN, file)]
    8.24 +  | body => XML.Decode.properties body);
    8.25 +
    8.26 +fun get exn =
    8.27 +  (case PolyML.exceptionLocation exn of
    8.28 +    NONE => []
    8.29 +  | SOME loc => of_location loc);
    8.30 +
    8.31 +fun update entries exn =
    8.32 +  let
    8.33 +    val loc =
    8.34 +      the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
    8.35 +        (PolyML.exceptionLocation exn);
    8.36 +    val props = of_location loc;
    8.37 +    val props' = fold Properties.put entries props;
    8.38 +  in
    8.39 +    if props = props' then exn
    8.40 +    else
    8.41 +      let
    8.42 +        val loc' =
    8.43 +          {file = YXML.string_of_body (XML.Encode.properties props'),
    8.44 +            startLine = #startLine loc, endLine = #endLine loc,
    8.45 +            startPosition = #startPosition loc, endPosition = #endPosition loc};
    8.46 +      in
    8.47 +        uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) ()
    8.48 +          handle exn' => exn'
    8.49 +      end
    8.50 +  end;
    8.51 +
    8.52 +end;
    8.53 +
     9.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Wed Jan 16 11:31:08 2013 +0100
     9.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Wed Jan 16 16:26:36 2013 +0100
     9.3 @@ -11,12 +11,8 @@
     9.4  
     9.5  fun position_of (loc: PolyML.location) =
     9.6    let
     9.7 -    val {file = text, startLine = line, startPosition = offset,
     9.8 -      endLine = _, endPosition = end_offset} = loc;
     9.9 -    val props =
    9.10 -      (case YXML.parse text of
    9.11 -        XML.Elem ((e, atts), _) => if e = Markup.positionN then atts else []
    9.12 -      | XML.Text s => Position.file_name s);
    9.13 +    val {startLine = line, startPosition = offset, endPosition = end_offset, ...} = loc;
    9.14 +    val props = Exn_Properties.of_location loc;
    9.15    in
    9.16      Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
    9.17    end;
    9.18 @@ -71,10 +67,7 @@
    9.19  
    9.20      (* input *)
    9.21  
    9.22 -    val location_props =
    9.23 -      op ^
    9.24 -        (YXML.output_markup (Markup.position |> Markup.properties
    9.25 -          (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))));
    9.26 +    val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
    9.27  
    9.28      val input_buffer =
    9.29        Unsynchronized.ref (toks |> map
    10.1 --- a/src/Pure/PIDE/command.ML	Wed Jan 16 11:31:08 2013 +0100
    10.2 +++ b/src/Pure/PIDE/command.ML	Wed Jan 16 16:26:36 2013 +0100
    10.3 @@ -65,7 +65,7 @@
    10.4    (case Toplevel.transition int tr st of
    10.5      SOME (st', NONE) => ([], SOME st')
    10.6    | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
    10.7 -  | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
    10.8 +  | NONE => (ML_Compiler.exn_messages Runtime.TERMINATE, NONE));
    10.9  
   10.10  fun check_cmts tr cmts st =
   10.11    Toplevel.setmp_thread_position tr
    11.1 --- a/src/Pure/ROOT	Wed Jan 16 11:31:08 2013 +0100
    11.2 +++ b/src/Pure/ROOT	Wed Jan 16 16:26:36 2013 +0100
    11.3 @@ -139,6 +139,8 @@
    11.4      "ML/ml_compiler_polyml.ML"
    11.5      "ML/ml_context.ML"
    11.6      "ML/ml_env.ML"
    11.7 +    "ML/exn_properties_dummy.ML"
    11.8 +    "ML/exn_properties_polyml.ML"
    11.9      "ML/ml_lex.ML"
   11.10      "ML/ml_parse.ML"
   11.11      "ML/ml_statistics_dummy.ML"
    12.1 --- a/src/Pure/ROOT.ML	Wed Jan 16 11:31:08 2013 +0100
    12.2 +++ b/src/Pure/ROOT.ML	Wed Jan 16 16:26:36 2013 +0100
    12.3 @@ -70,6 +70,10 @@
    12.4  
    12.5  (* concurrency within the ML runtime *)
    12.6  
    12.7 +if ML_System.is_polyml
    12.8 +then use "ML/exn_properties_polyml.ML"
    12.9 +else use "ML/exn_properties_dummy.ML";
   12.10 +
   12.11  if ML_System.name = "polyml-5.5.0"
   12.12  then use "ML/ml_statistics_polyml-5.5.0.ML"
   12.13  else use "ML/ml_statistics_dummy.ML";
    13.1 --- a/src/Pure/System/isabelle_process.ML	Wed Jan 16 11:31:08 2013 +0100
    13.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Jan 16 16:26:36 2013 +0100
    13.3 @@ -74,17 +74,16 @@
    13.4    Synchronized.change command_tracing_messages (K Inttab.empty);
    13.5  
    13.6  fun update_tracing () =
    13.7 -  (case Position.get_id (Position.thread_data ()) of
    13.8 +  (case Position.parse_id (Position.thread_data ()) of
    13.9      NONE => ()
   13.10    | SOME id =>
   13.11        let
   13.12 -        val i = Markup.parse_int id;
   13.13          val (n, ok) =
   13.14            Synchronized.change_result command_tracing_messages (fn tab =>
   13.15              let
   13.16 -              val n = the_default 0 (Inttab.lookup tab i) + 1;
   13.17 +              val n = the_default 0 (Inttab.lookup tab id) + 1;
   13.18                val ok = n <= ! tracing_messages;
   13.19 -            in ((n, ok), Inttab.update (i, n) tab) end);
   13.20 +            in ((n, ok), Inttab.update (id, n) tab) end);
   13.21        in
   13.22          if ok then ()
   13.23          else
   13.24 @@ -97,7 +96,7 @@
   13.25                handle Fail _ => error "Stopped";
   13.26            in
   13.27              Synchronized.change command_tracing_messages
   13.28 -              (Inttab.map_default (i, 0) (fn k => k - m))
   13.29 +              (Inttab.map_default (id, 0) (fn k => k - m))
   13.30            end
   13.31        end);
   13.32  
    14.1 --- a/src/Pure/goal.ML	Wed Jan 16 11:31:08 2013 +0100
    14.2 +++ b/src/Pure/goal.ML	Wed Jan 16 16:26:36 2013 +0100
    14.3 @@ -137,10 +137,7 @@
    14.4  fun fork_name name e =
    14.5    uninterruptible (fn _ => fn () =>
    14.6      let
    14.7 -      val id =
    14.8 -        (case Position.get_id (Position.thread_data ()) of
    14.9 -          NONE => 0
   14.10 -        | SOME id => Markup.parse_int id);
   14.11 +      val id = the_default 0 (Position.parse_id (Position.thread_data ()));
   14.12        val _ = count_forked 1;
   14.13        val future =
   14.14          (singleton o Future.forks)