# HG changeset patch # User wenzelm # Date 1358349996 -3600 # Node ID ee7fe4230642f1023ae641bcacd2de6b66577cb1 # Parent 54f06ba192efc5acb76571e1e96c787a56440a14 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset; diff -r 54f06ba192ef -r ee7fe4230642 src/Pure/Concurrent/future.ML --- 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 _ => diff -r 54f06ba192ef -r ee7fe4230642 src/Pure/Concurrent/par_exn.ML --- 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 diff -r 54f06ba192ef -r ee7fe4230642 src/Pure/General/position.ML --- 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 *) diff -r 54f06ba192ef -r ee7fe4230642 src/Pure/Isar/runtime.ML --- 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) => diff -r 54f06ba192ef -r ee7fe4230642 src/Pure/ML-Systems/polyml.ML --- 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"; diff -r 54f06ba192ef -r ee7fe4230642 src/Pure/ML-Systems/smlnj.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"; diff -r 54f06ba192ef -r ee7fe4230642 src/Pure/ML/exn_properties_dummy.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; + diff -r 54f06ba192ef -r ee7fe4230642 src/Pure/ML/exn_properties_polyml.ML --- /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; + diff -r 54f06ba192ef -r ee7fe4230642 src/Pure/ML/ml_compiler_polyml.ML --- 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 diff -r 54f06ba192ef -r ee7fe4230642 src/Pure/PIDE/command.ML --- 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 diff -r 54f06ba192ef -r ee7fe4230642 src/Pure/ROOT --- 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" diff -r 54f06ba192ef -r ee7fe4230642 src/Pure/ROOT.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"; diff -r 54f06ba192ef -r ee7fe4230642 src/Pure/System/isabelle_process.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); diff -r 54f06ba192ef -r ee7fe4230642 src/Pure/goal.ML --- 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)