more uniform Execution.fork vs. Execution.print;
authorwenzelm
Wed Mar 26 12:32:51 2014 +0100 (2014-03-26 ago)
changeset 562921a91a0da65ab
parent 56291 e79f76a48449
child 56293 9bc33476f6ac
more uniform Execution.fork vs. Execution.print;
asynchronous Execution.fork_prints, entrusted to Execution.fork management (NB: Command.print_finished is only relevant for persistent print functions);
src/Pure/PIDE/command.ML
src/Pure/PIDE/execution.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Wed Mar 26 12:15:42 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Wed Mar 26 12:32:51 2014 +0100
     1.3 @@ -359,7 +359,7 @@
     1.4      (fn {args, exec_id, ...} =>
     1.5        if null args then
     1.6          SOME {delay = NONE, pri = 1, persistent = false, strict = true,
     1.7 -          print_fn = fn _ => fn _ => Execution.apply_prints exec_id}
     1.8 +          print_fn = fn _ => fn _ => Execution.fork_prints exec_id}
     1.9        else NONE);
    1.10  
    1.11  val _ =
     2.1 --- a/src/Pure/PIDE/execution.ML	Wed Mar 26 12:15:42 2014 +0100
     2.2 +++ b/src/Pure/PIDE/execution.ML	Wed Mar 26 12:32:51 2014 +0100
     2.3 @@ -15,9 +15,10 @@
     2.4    val peek: Document_ID.exec -> Future.group list
     2.5    val cancel: Document_ID.exec -> unit
     2.6    val terminate: Document_ID.exec -> unit
     2.7 -  val fork: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
     2.8 -  val print: (serial -> unit) -> unit
     2.9 -  val apply_prints: Document_ID.exec -> unit
    2.10 +  type params = {name: string, pos: Position.T, pri: int}
    2.11 +  val fork: params -> (unit -> 'a) -> 'a future
    2.12 +  val print: params -> (serial -> unit) -> unit
    2.13 +  val fork_prints: Document_ID.exec -> unit
    2.14    val purge: Document_ID.exec list -> unit
    2.15    val reset: unit -> Future.group list
    2.16    val shutdown: unit -> unit
    2.17 @@ -28,7 +29,8 @@
    2.18  
    2.19  (* global state *)
    2.20  
    2.21 -type exec_state = Future.group list * (unit -> unit) list;  (*active forks, prints*)
    2.22 +type print = {name: string, pri: int, body: unit -> unit};
    2.23 +type exec_state = Future.group list * print list;  (*active forks, prints*)
    2.24  type state =
    2.25    Document_ID.execution * (*overall document execution*)
    2.26    exec_state Inttab.table;  (*running command execs*)
    2.27 @@ -88,7 +90,9 @@
    2.28    let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]
    2.29    in Output.status (implode (map (Markup.markup_only o props) markups)) end;
    2.30  
    2.31 -fun fork {name, pos, pri} e =
    2.32 +type params = {name: string, pos: Position.T, pri: int};
    2.33 +
    2.34 +fun fork ({name, pos, pri}: params) e =
    2.35    uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
    2.36      let
    2.37        val exec_id = the_default 0 (Position.parse_id pos);
    2.38 @@ -128,23 +132,23 @@
    2.39  
    2.40  (* print *)
    2.41  
    2.42 -fun print pr =
    2.43 +fun print ({name, pos, pri}: params) pr =
    2.44    change_state (apsnd (fn execs =>
    2.45      let
    2.46 -      val exec_id = the_default 0 (Position.parse_id (Position.thread_data ()));
    2.47 +      val exec_id = the_default 0 (Position.parse_id pos);
    2.48        val i = serial ();
    2.49 +      val print = {name = name, pri = pri, body = fn () => pr i};
    2.50      in
    2.51        (case Inttab.lookup execs exec_id of
    2.52 -        SOME (groups, prints) =>
    2.53 -          Inttab.update (exec_id, (groups, (fn () => pr i) :: prints)) execs
    2.54 +        SOME (groups, prints) => Inttab.update (exec_id, (groups, print :: prints)) execs
    2.55        | NONE => raise Fail (unregistered exec_id))
    2.56      end));
    2.57  
    2.58 -fun apply_prints exec_id =
    2.59 +fun fork_prints exec_id =
    2.60    (case Inttab.lookup (#2 (get_state ())) exec_id of
    2.61      SOME (_, prints) =>
    2.62        if null prints orelse null (tl prints) orelse not (Multithreading.enabled ())
    2.63 -      then List.app (fn e => e ()) (rev prints)
    2.64 +      then List.app (fn {body, ...} => body ()) (rev prints)
    2.65        else
    2.66          let
    2.67            val pos = Position.thread_data ();
    2.68 @@ -152,8 +156,10 @@
    2.69              (case Future.worker_task () of
    2.70                SOME task => Task_Queue.pri_of_task task
    2.71              | NONE => 0);
    2.72 -          val futures = map (fork {name = "Execution.print", pos = pos, pri = pri}) (rev prints);
    2.73 -        in ignore (Future.joins futures) end
    2.74 +        in
    2.75 +          List.app (fn {name, pri, body} =>
    2.76 +            ignore (fork {name = name, pos = pos, pri = pri} body)) (rev prints)
    2.77 +        end
    2.78    | NONE => raise Fail (unregistered exec_id));
    2.79  
    2.80