default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
authorwenzelm
Wed Aug 12 01:39:31 2015 +0200 (2015-08-12)
changeset 60911858694df711b
parent 60910 79abcf48c377
child 60912 3852e87e9b88
default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
src/Pure/Concurrent/future.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Wed Aug 12 01:25:00 2015 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Wed Aug 12 01:39:31 2015 +0200
     1.3 @@ -429,12 +429,14 @@
     1.4    let
     1.5      val result = Single_Assignment.var "future" : 'a result;
     1.6      val pos = Position.thread_data ();
     1.7 +    val context = Context.thread_data ();
     1.8      fun job ok =
     1.9        let
    1.10          val res =
    1.11            if ok then
    1.12              Exn.capture (fn () =>
    1.13 -              Multithreading.with_attributes atts (fn _ => Position.setmp_thread_data pos e ())) ()
    1.14 +              Multithreading.with_attributes atts (fn _ =>
    1.15 +                (Position.setmp_thread_data pos o Context.setmp_thread_data context) e ())) ()
    1.16            else Exn.interrupt_exn;
    1.17        in assign_result group result (identify_result pos res) end;
    1.18    in (result, job) end;
     2.1 --- a/src/Pure/ROOT.ML	Wed Aug 12 01:25:00 2015 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Wed Aug 12 01:39:31 2015 +0200
     2.3 @@ -85,7 +85,15 @@
     2.4  use "General/change_table.ML";
     2.5  use "General/graph.ML";
     2.6  
     2.7 +
     2.8 +(* fundamental structures *)
     2.9 +
    2.10 +use "name.ML";
    2.11 +use "term.ML";
    2.12 +use "context.ML";
    2.13 +use "context_position.ML";
    2.14  use "System/options.ML";
    2.15 +use "config.ML";
    2.16  
    2.17  
    2.18  (* concurrency within the ML runtime *)
    2.19 @@ -132,15 +140,6 @@
    2.20  use "PIDE/active.ML";
    2.21  
    2.22  
    2.23 -(* fundamental structures *)
    2.24 -
    2.25 -use "name.ML";
    2.26 -use "term.ML";
    2.27 -use "context.ML";
    2.28 -use "context_position.ML";
    2.29 -use "config.ML";
    2.30 -
    2.31 -
    2.32  (* inner syntax *)
    2.33  
    2.34  use "Syntax/type_annotation.ML";