less markup by default -- this is stored persistently in Isabelle/Scala;
authorwenzelm
Wed Mar 26 20:08:07 2014 +0100 (2014-03-26 ago)
changeset 562965413b6379c0e
parent 56295 a40e67ce4f84
child 56297 3925634718fb
less markup by default -- this is stored persistently in Isabelle/Scala;
removed dead code;
src/Pure/PIDE/execution.ML
     1.1 --- a/src/Pure/PIDE/execution.ML	Wed Mar 26 19:42:16 2014 +0100
     1.2 +++ b/src/Pure/PIDE/execution.ML	Wed Mar 26 20:08:07 2014 +0100
     1.3 @@ -87,8 +87,11 @@
     1.4  (* fork *)
     1.5  
     1.6  fun status task markups =
     1.7 -  let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]
     1.8 -  in Output.status (implode (map (Markup.markup_only o props) markups)) end;
     1.9 +  let
    1.10 +    val props =
    1.11 +      if ! Multithreading.trace >= 2
    1.12 +      then [(Markup.taskN, Task_Queue.str_of_task task)] else [];
    1.13 +  in Output.status (implode (map (Markup.markup_only o Markup.properties props) markups)) end;
    1.14  
    1.15  type params = {name: string, pos: Position.T, pri: int};
    1.16  
    1.17 @@ -150,13 +153,7 @@
    1.18        if null prints orelse null (tl prints) orelse not (Multithreading.enabled ())
    1.19        then List.app (fn {body, ...} => body ()) (rev prints)
    1.20        else
    1.21 -        let
    1.22 -          val pos = Position.thread_data ();
    1.23 -          val pri =
    1.24 -            (case Future.worker_task () of
    1.25 -              SOME task => Task_Queue.pri_of_task task
    1.26 -            | NONE => 0);
    1.27 -        in
    1.28 +        let val pos = Position.thread_data () in
    1.29            List.app (fn {name, pri, body} =>
    1.30              ignore (fork {name = name, pos = pos, pri = pri} body)) (rev prints)
    1.31          end