thread context for exceptions from forks, e.g. relevant when printing errors;
authorwenzelm
Tue Sep 01 23:10:23 2015 +0200 (2015-09-01 ago)
changeset 6107706cca32aa519
parent 61076 bdc1e2f0a86a
child 61078 528dec1c400b
thread context for exceptions from forks, e.g. relevant when printing errors;
tuned signature;
src/HOL/Library/code_test.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/Pure/Concurrent/future.ML
src/Pure/General/exn.ML
src/Pure/Isar/runtime.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/execution.ML
src/Pure/Syntax/syntax_phases.ML
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/HOL/Library/code_test.ML	Tue Sep 01 22:32:58 2015 +0200
     1.2 +++ b/src/HOL/Library/code_test.ML	Tue Sep 01 23:10:23 2015 +0200
     1.3 @@ -180,7 +180,7 @@
     1.4        Exn.interruptible_capture evaluate (Code_Target.evaluator ctxt target program deps true vs_ty);
     1.5      fun postproc f = map (apsnd (map_option (map f)))
     1.6    in
     1.7 -    Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t)
     1.8 +    Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t)
     1.9    end;
    1.10  
    1.11  (* Term preprocessing *)
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Sep 01 22:32:58 2015 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Sep 01 23:10:23 2015 +0200
     2.3 @@ -307,7 +307,7 @@
     2.4      fun evaluator program _ vs_ty_t deps =
     2.5        Exn.interruptible_capture (value opts ctxt cookie)
     2.6          (Code_Target.evaluator ctxt target program deps true vs_ty_t);
     2.7 -  in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t) end;
     2.8 +  in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end;
     2.9  
    2.10  
    2.11  (** counterexample generator **)
     3.1 --- a/src/Pure/Concurrent/future.ML	Tue Sep 01 22:32:58 2015 +0200
     3.2 +++ b/src/Pure/Concurrent/future.ML	Tue Sep 01 23:10:23 2015 +0200
     3.3 @@ -399,14 +399,12 @@
     3.4      end) ();
     3.5  
     3.6  fun identify_result pos res =
     3.7 -  (case res of
     3.8 -    Exn.Exn exn =>
     3.9 -      let val exec_id =
    3.10 -        (case Position.get_id pos of
    3.11 -          NONE => []
    3.12 -        | SOME id => [(Markup.exec_idN, id)])
    3.13 -      in Exn.Exn (Par_Exn.identify exec_id exn) end
    3.14 -  | _ => res);
    3.15 +  res |> Exn.map_exn (fn exn =>
    3.16 +    let val exec_id =
    3.17 +      (case Position.get_id pos of
    3.18 +        NONE => []
    3.19 +      | SOME id => [(Markup.exec_idN, id)])
    3.20 +    in Par_Exn.identify exec_id exn end);
    3.21  
    3.22  fun assign_result group result res =
    3.23    let
     4.1 --- a/src/Pure/General/exn.ML	Tue Sep 01 22:32:58 2015 +0200
     4.2 +++ b/src/Pure/General/exn.ML	Tue Sep 01 23:10:23 2015 +0200
     4.3 @@ -11,8 +11,9 @@
     4.4    val get_exn: 'a result -> exn option
     4.5    val capture: ('a -> 'b) -> 'a -> 'b result
     4.6    val release: 'a result -> 'a
     4.7 -  val map_result: ('a -> 'b) -> 'a result -> 'b result
     4.8 -  val maps_result: ('a -> 'b result) -> 'a result -> 'b result
     4.9 +  val map_res: ('a -> 'b) -> 'a result -> 'b result
    4.10 +  val maps_res: ('a -> 'b result) -> 'a result -> 'b result
    4.11 +  val map_exn: (exn -> exn) -> 'a result -> 'a result
    4.12    exception Interrupt
    4.13    val interrupt: unit -> 'a
    4.14    val is_interrupt: exn -> bool
    4.15 @@ -44,10 +45,13 @@
    4.16  fun release (Res y) = y
    4.17    | release (Exn e) = reraise e;
    4.18  
    4.19 -fun map_result f (Res x) = Res (f x)
    4.20 -  | map_result f (Exn e) = Exn e;
    4.21 +fun map_res f (Res x) = Res (f x)
    4.22 +  | map_res f (Exn e) = Exn e;
    4.23  
    4.24 -fun maps_result f = (fn Res x => x | Exn e => Exn e) o map_result f;
    4.25 +fun maps_res f = (fn Res x => x | Exn e => Exn e) o map_res f;
    4.26 +
    4.27 +fun map_exn f (Res x) = Res x
    4.28 +  | map_exn f (Exn e) = Exn (f e);
    4.29  
    4.30  
    4.31  (* interrupts *)
     5.1 --- a/src/Pure/Isar/runtime.ML	Tue Sep 01 22:32:58 2015 +0200
     5.2 +++ b/src/Pure/Isar/runtime.ML	Tue Sep 01 23:10:23 2015 +0200
     5.3 @@ -10,6 +10,7 @@
     5.4    exception EXCURSION_FAIL of exn * string
     5.5    exception TOPLEVEL_ERROR
     5.6    val exn_context: Proof.context option -> exn -> exn
     5.7 +  val thread_context: exn -> exn
     5.8    type error = ((serial * string) * string option)
     5.9    val exn_messages_ids: exn -> error list
    5.10    val exn_messages: exn -> (serial * string) list
    5.11 @@ -41,6 +42,9 @@
    5.12  fun exn_context NONE exn = exn
    5.13    | exn_context (SOME ctxt) exn = if Exn.is_interrupt exn then exn else CONTEXT (ctxt, exn);
    5.14  
    5.15 +fun thread_context exn =
    5.16 +  exn_context (Option.map Context.proof_of (Context.thread_data ())) exn;
    5.17 +
    5.18  
    5.19  (* exn_message *)
    5.20  
     6.1 --- a/src/Pure/PIDE/document.ML	Tue Sep 01 22:32:58 2015 +0200
     6.2 +++ b/src/Pure/PIDE/document.ML	Tue Sep 01 23:10:23 2015 +0200
     6.3 @@ -364,7 +364,7 @@
     6.4    | SOME content => content);
     6.5  
     6.6  fun resolve_blob state (blob_digest: blob_digest) =
     6.7 -  blob_digest |> Exn.map_result (fn (file_node, raw_digest) =>
     6.8 +  blob_digest |> Exn.map_res (fn (file_node, raw_digest) =>
     6.9      (file_node, Option.map (the_blob state) raw_digest));
    6.10  
    6.11  fun blob_reports pos (blob_digest: blob_digest) =
     7.1 --- a/src/Pure/PIDE/execution.ML	Tue Sep 01 22:32:58 2015 +0200
     7.2 +++ b/src/Pure/PIDE/execution.ML	Tue Sep 01 23:10:23 2015 +0200
     7.3 @@ -108,7 +108,8 @@
     7.4                val _ = status task [Markup.running];
     7.5                val result =
     7.6                  Exn.capture (Future.interruptible_task e) ()
     7.7 -                |> Future.identify_result pos;
     7.8 +                |> Future.identify_result pos
     7.9 +                |> Exn.map_exn Runtime.thread_context;
    7.10                val _ = status task [Markup.joined];
    7.11                val _ =
    7.12                  (case result of
     8.1 --- a/src/Pure/Syntax/syntax_phases.ML	Tue Sep 01 22:32:58 2015 +0200
     8.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Tue Sep 01 23:10:23 2015 +0200
     8.3 @@ -353,7 +353,7 @@
     8.4      val parse_rules = Syntax.parse_rules syn;
     8.5      val (ambig_msgs, asts) = parse_asts ctxt false root input;
     8.6      val results =
     8.7 -      (map o apsnd o Exn.maps_result)
     8.8 +      (map o apsnd o Exn.maps_res)
     8.9          (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr)) asts;
    8.10    in (ambig_msgs, results) end;
    8.11  
    8.12 @@ -405,7 +405,7 @@
    8.13  
    8.14            val results' =
    8.15              if parsed_len > 1 then
    8.16 -              (grouped 10 (Par_List.map_name "Syntax_Phases.parse_term") o apsnd o Exn.maps_result)
    8.17 +              (grouped 10 (Par_List.map_name "Syntax_Phases.parse_term") o apsnd o Exn.maps_res)
    8.18                  check results
    8.19              else results;
    8.20            val reports' = fst (hd results');
     9.1 --- a/src/Tools/Code/code_runtime.ML	Tue Sep 01 22:32:58 2015 +0200
     9.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Sep 01 23:10:23 2015 +0200
     9.3 @@ -131,7 +131,7 @@
     9.4        else ()
     9.5      fun evaluator program _ vs_ty_t deps =
     9.6        evaluation cookie ctxt (obtain_evaluator ctxt some_target program deps) vs_ty_t args;
     9.7 -  in Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t end;
     9.8 +  in Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t end;
     9.9  
    9.10  fun dynamic_value_strict cookie ctxt some_target postproc t args =
    9.11    Exn.release (dynamic_value_exn cookie ctxt some_target postproc t args);
    9.12 @@ -148,7 +148,7 @@
    9.13  fun static_value_exn cookie { ctxt, target, lift_postproc, consts } =
    9.14    let
    9.15      val evaluator = Code_Thingol.static_value { ctxt = ctxt,
    9.16 -      lift_postproc = Exn.map_result o lift_postproc, consts = consts }
    9.17 +      lift_postproc = Exn.map_res o lift_postproc, consts = consts }
    9.18        (static_evaluator cookie ctxt target);
    9.19    in fn ctxt' => evaluator ctxt' o reject_vars ctxt' end;
    9.20  
    9.21 @@ -314,7 +314,7 @@
    9.22      val cs_code = map (Axclass.unoverload_const thy) consts;
    9.23      val cTs = map2 (fn (_, T) => fn c => (c, T)) consts cs_code;
    9.24      val evaluator = Code_Thingol.static_value { ctxt = ctxt,
    9.25 -      lift_postproc = Exn.map_result o lift_postproc, consts = cs_code }
    9.26 +      lift_postproc = Exn.map_res o lift_postproc, consts = cs_code }
    9.27        (compile_evaluator cookie ctxt cs_code cTs T);
    9.28    in fn ctxt' =>
    9.29      evaluator ctxt' o reject_vars ctxt' o Syntax.check_term ctxt' o Type.constraint T