# HG changeset patch
# User wenzelm
# Date 1395860887 -3600
# Node ID 5413b6379c0e74b0621caa48f90973afb1395e34
# Parent  a40e67ce4f8490fb8a2428fbefbd9c219ee0c271
less markup by default -- this is stored persistently in Isabelle/Scala;
removed dead code;

diff -r a40e67ce4f84 -r 5413b6379c0e src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Wed Mar 26 19:42:16 2014 +0100
+++ b/src/Pure/PIDE/execution.ML	Wed Mar 26 20:08:07 2014 +0100
@@ -87,8 +87,11 @@
 (* fork *)
 
 fun status task markups =
-  let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]
-  in Output.status (implode (map (Markup.markup_only o props) markups)) end;
+  let
+    val props =
+      if ! Multithreading.trace >= 2
+      then [(Markup.taskN, Task_Queue.str_of_task task)] else [];
+  in Output.status (implode (map (Markup.markup_only o Markup.properties props) markups)) end;
 
 type params = {name: string, pos: Position.T, pri: int};
 
@@ -150,13 +153,7 @@
       if null prints orelse null (tl prints) orelse not (Multithreading.enabled ())
       then List.app (fn {body, ...} => body ()) (rev prints)
       else
-        let
-          val pos = Position.thread_data ();
-          val pri =
-            (case Future.worker_task () of
-              SOME task => Task_Queue.pri_of_task task
-            | NONE => 0);
-        in
+        let val pos = Position.thread_data () in
           List.app (fn {name, pri, body} =>
             ignore (fork {name = name, pos = pos, pri = pri} body)) (rev prints)
         end