# HG changeset patch
# User wenzelm
# Date 1441141823 -7200
# Node ID 06cca32aa519733b4e3aecb45e6df3102347dcee
# Parent  bdc1e2f0a86a94e422877ca475f1fa0065ac6e63
thread context for exceptions from forks, e.g. relevant when printing errors;
tuned signature;

diff -r bdc1e2f0a86a -r 06cca32aa519 src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Tue Sep 01 22:32:58 2015 +0200
+++ b/src/HOL/Library/code_test.ML	Tue Sep 01 23:10:23 2015 +0200
@@ -180,7 +180,7 @@
       Exn.interruptible_capture evaluate (Code_Target.evaluator ctxt target program deps true vs_ty);
     fun postproc f = map (apsnd (map_option (map f)))
   in
-    Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t)
+    Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t)
   end;
 
 (* Term preprocessing *)
diff -r bdc1e2f0a86a -r 06cca32aa519 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Sep 01 22:32:58 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Sep 01 23:10:23 2015 +0200
@@ -307,7 +307,7 @@
     fun evaluator program _ vs_ty_t deps =
       Exn.interruptible_capture (value opts ctxt cookie)
         (Code_Target.evaluator ctxt target program deps true vs_ty_t);
-  in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t) end;
+  in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end;
 
 
 (** counterexample generator **)
diff -r bdc1e2f0a86a -r 06cca32aa519 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Sep 01 22:32:58 2015 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Sep 01 23:10:23 2015 +0200
@@ -399,14 +399,12 @@
     end) ();
 
 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);
+  res |> Exn.map_exn (fn exn =>
+    let val exec_id =
+      (case Position.get_id pos of
+        NONE => []
+      | SOME id => [(Markup.exec_idN, id)])
+    in Par_Exn.identify exec_id exn end);
 
 fun assign_result group result res =
   let
diff -r bdc1e2f0a86a -r 06cca32aa519 src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Tue Sep 01 22:32:58 2015 +0200
+++ b/src/Pure/General/exn.ML	Tue Sep 01 23:10:23 2015 +0200
@@ -11,8 +11,9 @@
   val get_exn: 'a result -> exn option
   val capture: ('a -> 'b) -> 'a -> 'b result
   val release: 'a result -> 'a
-  val map_result: ('a -> 'b) -> 'a result -> 'b result
-  val maps_result: ('a -> 'b result) -> 'a result -> 'b result
+  val map_res: ('a -> 'b) -> 'a result -> 'b result
+  val maps_res: ('a -> 'b result) -> 'a result -> 'b result
+  val map_exn: (exn -> exn) -> 'a result -> 'a result
   exception Interrupt
   val interrupt: unit -> 'a
   val is_interrupt: exn -> bool
@@ -44,10 +45,13 @@
 fun release (Res y) = y
   | release (Exn e) = reraise e;
 
-fun map_result f (Res x) = Res (f x)
-  | map_result f (Exn e) = Exn e;
+fun map_res f (Res x) = Res (f x)
+  | map_res f (Exn e) = Exn e;
 
-fun maps_result f = (fn Res x => x | Exn e => Exn e) o map_result f;
+fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f;
+
+fun map_exn f (Res x) = Res x
+  | map_exn f (Exn e) = Exn (f e);
 
 
 (* interrupts *)
diff -r bdc1e2f0a86a -r 06cca32aa519 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Tue Sep 01 22:32:58 2015 +0200
+++ b/src/Pure/Isar/runtime.ML	Tue Sep 01 23:10:23 2015 +0200
@@ -10,6 +10,7 @@
   exception EXCURSION_FAIL of exn * string
   exception TOPLEVEL_ERROR
   val exn_context: Proof.context option -> exn -> exn
+  val thread_context: exn -> exn
   type error = ((serial * string) * string option)
   val exn_messages_ids: exn -> error list
   val exn_messages: exn -> (serial * string) list
@@ -41,6 +42,9 @@
 fun exn_context NONE exn = exn
   | exn_context (SOME ctxt) exn = if Exn.is_interrupt exn then exn else CONTEXT (ctxt, exn);
 
+fun thread_context exn =
+  exn_context (Option.map Context.proof_of (Context.thread_data ())) exn;
+
 
 (* exn_message *)
 
diff -r bdc1e2f0a86a -r 06cca32aa519 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Sep 01 22:32:58 2015 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Sep 01 23:10:23 2015 +0200
@@ -364,7 +364,7 @@
   | SOME content => content);
 
 fun resolve_blob state (blob_digest: blob_digest) =
-  blob_digest |> Exn.map_result (fn (file_node, raw_digest) =>
+  blob_digest |> Exn.map_res (fn (file_node, raw_digest) =>
     (file_node, Option.map (the_blob state) raw_digest));
 
 fun blob_reports pos (blob_digest: blob_digest) =
diff -r bdc1e2f0a86a -r 06cca32aa519 src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Tue Sep 01 22:32:58 2015 +0200
+++ b/src/Pure/PIDE/execution.ML	Tue Sep 01 23:10:23 2015 +0200
@@ -108,7 +108,8 @@
               val _ = status task [Markup.running];
               val result =
                 Exn.capture (Future.interruptible_task e) ()
-                |> Future.identify_result pos;
+                |> Future.identify_result pos
+                |> Exn.map_exn Runtime.thread_context;
               val _ = status task [Markup.joined];
               val _ =
                 (case result of
diff -r bdc1e2f0a86a -r 06cca32aa519 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Sep 01 22:32:58 2015 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Sep 01 23:10:23 2015 +0200
@@ -353,7 +353,7 @@
     val parse_rules = Syntax.parse_rules syn;
     val (ambig_msgs, asts) = parse_asts ctxt false root input;
     val results =
-      (map o apsnd o Exn.maps_result)
+      (map o apsnd o Exn.maps_res)
         (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr)) asts;
   in (ambig_msgs, results) end;
 
@@ -405,7 +405,7 @@
 
           val results' =
             if parsed_len > 1 then
-              (grouped 10 (Par_List.map_name "Syntax_Phases.parse_term") o apsnd o Exn.maps_result)
+              (grouped 10 (Par_List.map_name "Syntax_Phases.parse_term") o apsnd o Exn.maps_res)
                 check results
             else results;
           val reports' = fst (hd results');
diff -r bdc1e2f0a86a -r 06cca32aa519 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Tue Sep 01 22:32:58 2015 +0200
+++ b/src/Tools/Code/code_runtime.ML	Tue Sep 01 23:10:23 2015 +0200
@@ -131,7 +131,7 @@
       else ()
     fun evaluator program _ vs_ty_t deps =
       evaluation cookie ctxt (obtain_evaluator ctxt some_target program deps) vs_ty_t args;
-  in Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t end;
+  in Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t end;
 
 fun dynamic_value_strict cookie ctxt some_target postproc t args =
   Exn.release (dynamic_value_exn cookie ctxt some_target postproc t args);
@@ -148,7 +148,7 @@
 fun static_value_exn cookie { ctxt, target, lift_postproc, consts } =
   let
     val evaluator = Code_Thingol.static_value { ctxt = ctxt,
-      lift_postproc = Exn.map_result o lift_postproc, consts = consts }
+      lift_postproc = Exn.map_res o lift_postproc, consts = consts }
       (static_evaluator cookie ctxt target);
   in fn ctxt' => evaluator ctxt' o reject_vars ctxt' end;
 
@@ -314,7 +314,7 @@
     val cs_code = map (Axclass.unoverload_const thy) consts;
     val cTs = map2 (fn (_, T) => fn c => (c, T)) consts cs_code;
     val evaluator = Code_Thingol.static_value { ctxt = ctxt,
-      lift_postproc = Exn.map_result o lift_postproc, consts = cs_code }
+      lift_postproc = Exn.map_res o lift_postproc, consts = cs_code }
       (compile_evaluator cookie ctxt cs_code cTs T);
   in fn ctxt' =>
     evaluator ctxt' o reject_vars ctxt' o Syntax.check_term ctxt' o Type.constraint T