# HG changeset patch # User wenzelm # Date 1358365289 -3600 # Node ID fe4714886d923bb283ad02df94626fa944dbd175 # Parent 697e3bb60a3bc45d97c907b348c33a77ed31150c identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals; diff -r 697e3bb60a3b -r fe4714886d92 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Wed Jan 16 20:40:50 2013 +0100 +++ b/src/Pure/Concurrent/future.ML Wed Jan 16 20:41:29 2013 +0100 @@ -55,6 +55,8 @@ val interruptible_task: ('a -> 'b) -> 'a -> 'b val cancel_group: group -> unit val cancel: 'a future -> unit + val error_msg: Position.T -> (serial * string) * string option -> unit + val identify_result: Position.T -> 'a Exn.result -> 'a Exn.result type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool} val default_params: params val forks: params -> (unit -> 'a) list -> 'a future list @@ -433,14 +435,24 @@ fun cancel x = cancel_group (Task_Queue.group_of_task (task_of x)); -(* future jobs *) +(* results *) + +fun error_msg pos ((serial, msg), exec_id) = + if is_none exec_id orelse exec_id = Position.get_id pos + then Output.error_msg' (serial, msg) else warning msg; -fun assign_result group result raw_res = +fun identify_result pos res = + (case res of + Exn.Exn exn => + let val exec_id = + (case Position.get_id pos of + NONE => [] + | SOME id => [(Markup.exec_idN, id)]) + in Exn.Exn (Par_Exn.identify exec_id exn) end + | _ => res); + +fun assign_result group result res = let - val res = - (case raw_res of - Exn.Exn exn => Exn.Exn (Par_Exn.identify [] exn) - | _ => raw_res); val _ = Single_Assignment.assign result res handle exn as Fail _ => (case Single_Assignment.peek result of @@ -453,6 +465,9 @@ | Exn.Res _ => true); in ok end; + +(* future jobs *) + fun future_job group interrupts (e: unit -> 'a) = let val result = Single_Assignment.var "future" : 'a result; @@ -467,7 +482,7 @@ then Multithreading.private_interrupts else Multithreading.no_interrupts) (fn _ => Position.setmp_thread_data pos e ())) () else Exn.interrupt_exn; - in assign_result group result res end; + in assign_result group result (identify_result pos res) end; in (result, job) end; @@ -563,7 +578,7 @@ val task = Task_Queue.dummy_task; val group = Task_Queue.group_of_task task; val result = Single_Assignment.var "value" : 'a result; - val _ = assign_result group result res; + val _ = assign_result group result (identify_result (Position.thread_data ()) res); in Future {promised = false, task = task, result = result} end; fun value x = value_result (Exn.Res x); @@ -619,7 +634,9 @@ else let val group = Task_Queue.group_of_task task; - fun job ok = assign_result group result (if ok then res else Exn.interrupt_exn); + val pos = Position.thread_data (); + fun job ok = + assign_result group result (if ok then identify_result pos res else Exn.interrupt_exn); val _ = Multithreading.with_attributes Multithreading.no_interrupts (fn _ => let diff -r 697e3bb60a3b -r fe4714886d92 src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Wed Jan 16 20:40:50 2013 +0100 +++ b/src/Pure/Isar/runtime.ML Wed Jan 16 20:41:29 2013 +0100 @@ -12,6 +12,7 @@ exception TOPLEVEL_ERROR val debug: bool Unsynchronized.ref val exn_context: Proof.context option -> exn -> exn + val exn_messages_ids: (exn -> Position.T) -> exn -> ((serial * string) * string option) 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 @@ -42,22 +43,28 @@ (* exn_message *) +local + fun if_context NONE _ _ = [] | if_context (SOME ctxt) f xs = map (f ctxt) xs; -fun exn_messages exn_position e = +fun identify exn = let - fun identify exn = - let val exn' = Par_Exn.identify [] exn - in (Par_Exn.the_serial exn', exn') end; + val exn' = Par_Exn.identify [] exn; + val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN; + in ((Par_Exn.the_serial exn', exn'), exec_id) 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 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)]); +in + +fun exn_messages_ids exn_position e = + let fun raised exn name msgs = let val pos = Position.here (exn_position exn) in (case msgs of @@ -66,10 +73,10 @@ | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs)) end; - fun exn_msgs (context, (i, exn)) = + fun exn_msgs (context, ((i, exn), id)) = (case exn of EXCURSION_FAIL (exn, loc) => - map (apsnd (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc))) + map (fn ((i, msg), id) => ((i, msg ^ Markup.markup Markup.no_report ("\n" ^ loc)), id)) (sorted_msgs context exn) | _ => let @@ -94,12 +101,17 @@ raised exn ("THM " ^ string_of_int i) (msg :: if_context context Display.string_of_thm thms) | _ => raised exn (General.exnMessage exn) []); - in [(i, msg)] end) + in [((i, msg), id)] end) and sorted_msgs context exn = - sort_distinct (int_ord o pairself fst) (maps exn_msgs (flatten context exn)); + sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn)); in sorted_msgs NONE e end; +end; + +fun exn_messages exn_position exn = + map #1 (exn_messages_ids exn_position exn); + fun exn_message exn_position exn = (case exn_messages exn_position exn of [] => "Interrupt" diff -r 697e3bb60a3b -r fe4714886d92 src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML Wed Jan 16 20:40:50 2013 +0100 +++ b/src/Pure/ML/ml_compiler.ML Wed Jan 16 20:41:29 2013 +0100 @@ -7,6 +7,7 @@ signature ML_COMPILER = sig val exn_position: exn -> Position.T + val exn_messages_ids: exn -> ((serial * string) * string option) list val exn_messages: exn -> (serial * string) list val exn_message: exn -> string val eval: bool -> Position.T -> ML_Lex.token list -> unit @@ -16,6 +17,7 @@ struct fun exn_position _ = Position.none; +val exn_messages_ids = Runtime.exn_messages_ids exn_position; val exn_messages = Runtime.exn_messages exn_position; val exn_message = Runtime.exn_message exn_position; diff -r 697e3bb60a3b -r fe4714886d92 src/Pure/ML/ml_compiler_polyml.ML --- a/src/Pure/ML/ml_compiler_polyml.ML Wed Jan 16 20:40:50 2013 +0100 +++ b/src/Pure/ML/ml_compiler_polyml.ML Wed Jan 16 20:41:29 2013 +0100 @@ -22,6 +22,7 @@ NONE => Position.none | SOME loc => position_of loc); +val exn_messages_ids = Runtime.exn_messages_ids exn_position; val exn_messages = Runtime.exn_messages exn_position; val exn_message = Runtime.exn_message exn_position; diff -r 697e3bb60a3b -r fe4714886d92 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Wed Jan 16 20:40:50 2013 +0100 +++ b/src/Pure/PIDE/command.ML Wed Jan 16 20:41:29 2013 +0100 @@ -64,15 +64,15 @@ fun run int tr st = (case Toplevel.transition int tr st of SOME (st', NONE) => ([], SOME st') - | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE) - | NONE => (ML_Compiler.exn_messages Runtime.TERMINATE, NONE)); + | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE) + | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE)); fun check_cmts tr cmts st = Toplevel.setmp_thread_position tr (fn () => cmts |> maps (fn cmt => (Thy_Output.check_text (Token.source_position_of cmt) st; []) - handle exn => ML_Compiler.exn_messages exn)) (); + handle exn => ML_Compiler.exn_messages_ids exn)) (); fun timing tr t = if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else (); @@ -106,7 +106,7 @@ val errs = errs1 @ errs2; val _ = timing tr (Timing.result start); val _ = Toplevel.status tr Markup.finished; - val _ = List.app (Toplevel.error_msg tr) errs; + val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs; in (case result of NONE => diff -r 697e3bb60a3b -r fe4714886d92 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Wed Jan 16 20:40:50 2013 +0100 +++ b/src/Pure/PIDE/markup.ML Wed Jan 16 20:41:29 2013 +0100 @@ -107,6 +107,7 @@ val finishedN: string val finished: T val failedN: string val failed: T val serialN: string + val exec_idN: string val initN: string val statusN: string val resultN: string @@ -364,6 +365,7 @@ (* messages *) val serialN = "serial"; +val exec_idN = "exec_id"; val initN = "init"; val statusN = "status"; diff -r 697e3bb60a3b -r fe4714886d92 src/Pure/goal.ML --- a/src/Pure/goal.ML Wed Jan 16 20:40:50 2013 +0100 +++ b/src/Pure/goal.ML Wed Jan 16 20:41:29 2013 +0100 @@ -137,8 +137,10 @@ fun fork_name name e = uninterruptible (fn _ => fn () => let - val id = the_default 0 (Position.parse_id (Position.thread_data ())); + val pos = Position.thread_data (); + val id = the_default 0 (Position.parse_id pos); val _ = count_forked 1; + val future = (singleton o Future.forks) {name = name, group = NONE, deps = [], pri = ~1, interrupts = false} @@ -146,7 +148,9 @@ let val task = the (Future.worker_task ()); val _ = status task [Markup.running]; - val result = Exn.capture (Future.interruptible_task e) (); + val result = + Exn.capture (Future.interruptible_task e) () + |> Future.identify_result pos; val _ = status task [Markup.finished, Markup.joined]; val _ = (case result of @@ -156,7 +160,7 @@ else (status task [Markup.failed]; Output.report (Markup.markup_only Markup.bad); - Output.error_msg (ML_Compiler.exn_message exn))); + List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn))); val _ = count_forked ~1; in Exn.release result end); val _ = status (Future.task_of future) [Markup.forked];