src/Pure/PIDE/execution.ML
changeset 61077 06cca32aa519
parent 59467 58c4f3e1870f
child 62891 7a11ea5c9626
     1.1 --- a/src/Pure/PIDE/execution.ML	Tue Sep 01 22:32:58 2015 +0200
     1.2 +++ b/src/Pure/PIDE/execution.ML	Tue Sep 01 23:10:23 2015 +0200
     1.3 @@ -108,7 +108,8 @@
     1.4                val _ = status task [Markup.running];
     1.5                val result =
     1.6                  Exn.capture (Future.interruptible_task e) ()
     1.7 -                |> Future.identify_result pos;
     1.8 +                |> Future.identify_result pos
     1.9 +                |> Exn.map_exn Runtime.thread_context;
    1.10                val _ = status task [Markup.joined];
    1.11                val _ =
    1.12                  (case result of