tuned;
authorwenzelm
Sun Aug 25 20:43:10 2013 +0200 (2013-08-25 ago)
changeset 531932ddc5e788f7c
parent 53192 04df1d236e1c
child 53194 1943db7bc34c
tuned;
src/Pure/PIDE/execution.ML
     1.1 --- a/src/Pure/PIDE/execution.ML	Sun Aug 25 20:32:26 2013 +0200
     1.2 +++ b/src/Pure/PIDE/execution.ML	Sun Aug 25 20:43:10 2013 +0200
     1.3 @@ -80,23 +80,16 @@
     1.4  
     1.5  (* fork *)
     1.6  
     1.7 -local
     1.8 -
     1.9  fun status task markups =
    1.10    let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]
    1.11    in Output.status (implode (map (Markup.markup_only o props) markups)) end;
    1.12  
    1.13 -fun register exec =
    1.14 -  change_state (fn (execution, execs) => (execution, Inttab.cons_list exec execs));
    1.15 -
    1.16 -in
    1.17 -
    1.18  fun fork {name, pos, pri} e =
    1.19    uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
    1.20      let
    1.21        val exec_id = the_default 0 (Position.parse_id pos);
    1.22        val group = Future.worker_subgroup ();
    1.23 -      val _ = register (exec_id, group);
    1.24 +      val _ = change_state (apsnd (Inttab.cons_list (exec_id, group)));
    1.25  
    1.26        val future =
    1.27          (singleton o Future.forks)
    1.28 @@ -122,8 +115,6 @@
    1.29        val _ = status (Future.task_of future) [Markup.forked];
    1.30      in future end)) ();
    1.31  
    1.32 -end;
    1.33 -
    1.34  
    1.35  (* cleanup *)
    1.36