src/Pure/PIDE/execution.ML
changeset 56296 5413b6379c0e
parent 56292 1a91a0da65ab
child 56297 3925634718fb
equal deleted inserted replaced
56295:a40e67ce4f84 56296:5413b6379c0e
    85 
    85 
    86 
    86 
    87 (* fork *)
    87 (* fork *)
    88 
    88 
    89 fun status task markups =
    89 fun status task markups =
    90   let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]
    90   let
    91   in Output.status (implode (map (Markup.markup_only o props) markups)) end;
    91     val props =
       
    92       if ! Multithreading.trace >= 2
       
    93       then [(Markup.taskN, Task_Queue.str_of_task task)] else [];
       
    94   in Output.status (implode (map (Markup.markup_only o Markup.properties props) markups)) end;
    92 
    95 
    93 type params = {name: string, pos: Position.T, pri: int};
    96 type params = {name: string, pos: Position.T, pri: int};
    94 
    97 
    95 fun fork ({name, pos, pri}: params) e =
    98 fun fork ({name, pos, pri}: params) e =
    96   uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
    99   uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
   148   (case Inttab.lookup (#2 (get_state ())) exec_id of
   151   (case Inttab.lookup (#2 (get_state ())) exec_id of
   149     SOME (_, prints) =>
   152     SOME (_, prints) =>
   150       if null prints orelse null (tl prints) orelse not (Multithreading.enabled ())
   153       if null prints orelse null (tl prints) orelse not (Multithreading.enabled ())
   151       then List.app (fn {body, ...} => body ()) (rev prints)
   154       then List.app (fn {body, ...} => body ()) (rev prints)
   152       else
   155       else
   153         let
   156         let val pos = Position.thread_data () in
   154           val pos = Position.thread_data ();
       
   155           val pri =
       
   156             (case Future.worker_task () of
       
   157               SOME task => Task_Queue.pri_of_task task
       
   158             | NONE => 0);
       
   159         in
       
   160           List.app (fn {name, pri, body} =>
   157           List.app (fn {name, pri, body} =>
   161             ignore (fork {name = name, pos = pos, pri = pri} body)) (rev prints)
   158             ignore (fork {name = name, pos = pos, pri = pri} body)) (rev prints)
   162         end
   159         end
   163   | NONE => raise Fail (unregistered exec_id));
   160   | NONE => raise Fail (unregistered exec_id));
   164 
   161