added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
authorwenzelm
Wed Mar 26 12:15:42 2014 +0100 (2014-03-26 ago)
changeset 56291e79f76a48449
parent 56288 bf1bdf335ea0
child 56292 1a91a0da65ab
added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
misc tuning;
src/Pure/PIDE/command.ML
src/Pure/PIDE/execution.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Wed Mar 26 09:19:04 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Wed Mar 26 12:15:42 2014 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4      eval -> print list -> print list option
     1.5    type print_fn = Toplevel.transition -> Toplevel.state -> unit
     1.6    type print_function =
     1.7 -    {command_name: string, args: string list} ->
     1.8 +    {command_name: string, args: string list, exec_id: Document_ID.exec} ->
     1.9        {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
    1.10    val print_function: string -> print_function -> unit
    1.11    val no_print_function: string -> unit
    1.12 @@ -172,9 +172,10 @@
    1.13  
    1.14  datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo};
    1.15  
    1.16 -fun eval_eq (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) = exec_id = exec_id';
    1.17 +fun eval_exec_id (Eval {exec_id, ...}) = exec_id;
    1.18 +val eval_eq = op = o pairself eval_exec_id;
    1.19  
    1.20 -fun eval_running (Eval {exec_id, ...}) = Execution.is_running_exec exec_id;
    1.21 +val eval_running = Execution.is_running_exec o eval_exec_id;
    1.22  fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process;
    1.23  
    1.24  fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
    1.25 @@ -260,10 +261,13 @@
    1.26   {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool,
    1.27    exec_id: Document_ID.exec, print_process: unit memo};
    1.28  
    1.29 +fun print_exec_id (Print {exec_id, ...}) = exec_id;
    1.30 +val print_eq = op = o pairself print_exec_id;
    1.31 +
    1.32  type print_fn = Toplevel.transition -> Toplevel.state -> unit;
    1.33  
    1.34  type print_function =
    1.35 -  {command_name: string, args: string list} ->
    1.36 +  {command_name: string, args: string list, exec_id: Document_ID.exec} ->
    1.37      {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option;
    1.38  
    1.39  local
    1.40 @@ -277,8 +281,6 @@
    1.41        if Exn.is_interrupt exn then reraise exn
    1.42        else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
    1.43  
    1.44 -fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
    1.45 -
    1.46  fun print_finished (Print {print_process, ...}) = memo_finished print_process;
    1.47  
    1.48  fun print_persistent (Print {persistent, ...}) = persistent;
    1.49 @@ -315,7 +317,7 @@
    1.50  
    1.51      fun new_print name args get_pr =
    1.52        let
    1.53 -        val params = {command_name = command_name, args = args};
    1.54 +        val params = {command_name = command_name, args = args, exec_id = eval_exec_id eval};
    1.55        in
    1.56          (case Exn.capture (Toplevel.controlled_execution NONE get_pr) params of
    1.57            Exn.Res NONE => NONE
    1.58 @@ -353,6 +355,14 @@
    1.59  end;
    1.60  
    1.61  val _ =
    1.62 +  print_function "Execution.print"
    1.63 +    (fn {args, exec_id, ...} =>
    1.64 +      if null args then
    1.65 +        SOME {delay = NONE, pri = 1, persistent = false, strict = true,
    1.66 +          print_fn = fn _ => fn _ => Execution.apply_prints exec_id}
    1.67 +      else NONE);
    1.68 +
    1.69 +val _ =
    1.70    print_function "print_state"
    1.71      (fn {command_name, ...} =>
    1.72        SOME {delay = NONE, pri = 1, persistent = false, strict = true,
    1.73 @@ -373,8 +383,7 @@
    1.74    (Eval {exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
    1.75  
    1.76  fun exec_ids NONE = []
    1.77 -  | exec_ids (SOME (Eval {exec_id, ...}, prints)) =
    1.78 -      exec_id :: map (fn Print {exec_id, ...} => exec_id) prints;
    1.79 +  | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints;
    1.80  
    1.81  local
    1.82  
     2.1 --- a/src/Pure/PIDE/execution.ML	Wed Mar 26 09:19:04 2014 +0100
     2.2 +++ b/src/Pure/PIDE/execution.ML	Wed Mar 26 12:15:42 2014 +0100
     2.3 @@ -16,6 +16,8 @@
     2.4    val cancel: Document_ID.exec -> unit
     2.5    val terminate: Document_ID.exec -> unit
     2.6    val fork: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
     2.7 +  val print: (serial -> unit) -> unit
     2.8 +  val apply_prints: Document_ID.exec -> unit
     2.9    val purge: Document_ID.exec list -> unit
    2.10    val reset: unit -> Future.group list
    2.11    val shutdown: unit -> unit
    2.12 @@ -26,18 +28,19 @@
    2.13  
    2.14  (* global state *)
    2.15  
    2.16 -datatype state = State of
    2.17 -  {execution: Document_ID.execution,  (*overall document execution*)
    2.18 -   execs: Future.group list Inttab.table};  (*command execs with registered forks*)
    2.19 +type exec_state = Future.group list * (unit -> unit) list;  (*active forks, prints*)
    2.20 +type state =
    2.21 +  Document_ID.execution * (*overall document execution*)
    2.22 +  exec_state Inttab.table;  (*running command execs*)
    2.23  
    2.24 -fun make_state (execution, execs) = State {execution = execution, execs = execs};
    2.25 -fun map_state f (State {execution, execs}) = make_state (f (execution, execs));
    2.26 -
    2.27 -val init_state = make_state (Document_ID.none, Inttab.make [(Document_ID.none, [])]);
    2.28 +val init_state: state = (Document_ID.none, Inttab.make [(Document_ID.none, ([], []))]);
    2.29  val state = Synchronized.var "Execution.state" init_state;
    2.30  
    2.31 -fun get_state () = let val State args = Synchronized.value state in args end;
    2.32 -fun change_state f = Synchronized.change state (map_state f);
    2.33 +fun get_state () = Synchronized.value state;
    2.34 +fun change_state_result f = Synchronized.change_result state f;
    2.35 +fun change_state f = Synchronized.change state f;
    2.36 +
    2.37 +fun unregistered exec_id = "Unregistered execution: " ^ Document_ID.print exec_id;
    2.38  
    2.39  
    2.40  (* unique running execution *)
    2.41 @@ -50,29 +53,30 @@
    2.42  
    2.43  fun discontinue () = change_state (apfst (K Document_ID.none));
    2.44  
    2.45 -fun is_running execution_id = execution_id = #execution (get_state ());
    2.46 +fun is_running execution_id = execution_id = #1 (get_state ());
    2.47  
    2.48  
    2.49  (* execs *)
    2.50  
    2.51  fun is_running_exec exec_id =
    2.52 -  Inttab.defined (#execs (get_state ())) exec_id;
    2.53 +  Inttab.defined (#2 (get_state ())) exec_id;
    2.54  
    2.55  fun running execution_id exec_id groups =
    2.56 -  Synchronized.change_result state
    2.57 -    (fn State {execution = execution_id', execs} =>
    2.58 -      let
    2.59 -        val continue = execution_id = execution_id';
    2.60 -        val execs' =
    2.61 -          if continue then
    2.62 -            Inttab.update_new (exec_id, groups) execs
    2.63 -              handle Inttab.DUP dup =>
    2.64 -                raise Fail ("Execution already registered: " ^ Document_ID.print dup)
    2.65 -          else execs;
    2.66 -      in (continue, make_state (execution_id', execs')) end);
    2.67 +  change_state_result (fn (execution_id', execs) =>
    2.68 +    let
    2.69 +      val continue = execution_id = execution_id';
    2.70 +      val execs' =
    2.71 +        if continue then
    2.72 +          Inttab.update_new (exec_id, (groups, [])) execs
    2.73 +            handle Inttab.DUP dup =>
    2.74 +              raise Fail ("Execution already registered: " ^ Document_ID.print dup)
    2.75 +        else execs;
    2.76 +    in (continue, (execution_id', execs')) end);
    2.77  
    2.78  fun peek exec_id =
    2.79 -  Inttab.lookup_list (#execs (get_state ())) exec_id;
    2.80 +  (case Inttab.lookup (#2 (get_state ())) exec_id of
    2.81 +    SOME (groups, _) => groups
    2.82 +  | NONE => []);
    2.83  
    2.84  fun cancel exec_id = List.app Future.cancel_group (peek exec_id);
    2.85  fun terminate exec_id = List.app Future.terminate (peek exec_id);
    2.86 @@ -90,9 +94,10 @@
    2.87        val exec_id = the_default 0 (Position.parse_id pos);
    2.88        val group = Future.worker_subgroup ();
    2.89        val _ = change_state (apsnd (fn execs =>
    2.90 -        if Inttab.defined execs exec_id
    2.91 -        then Inttab.cons_list (exec_id, group) execs
    2.92 -        else raise Fail ("Cannot fork from unregistered execution: " ^ Document_ID.print exec_id)));
    2.93 +        (case Inttab.lookup execs exec_id of
    2.94 +          SOME (groups, prints) =>
    2.95 +            Inttab.update (exec_id, (group :: groups, prints)) execs
    2.96 +        | NONE => raise Fail (unregistered exec_id))));
    2.97  
    2.98        val future =
    2.99          (singleton o Future.forks)
   2.100 @@ -121,6 +126,37 @@
   2.101      in future end)) ();
   2.102  
   2.103  
   2.104 +(* print *)
   2.105 +
   2.106 +fun print pr =
   2.107 +  change_state (apsnd (fn execs =>
   2.108 +    let
   2.109 +      val exec_id = the_default 0 (Position.parse_id (Position.thread_data ()));
   2.110 +      val i = serial ();
   2.111 +    in
   2.112 +      (case Inttab.lookup execs exec_id of
   2.113 +        SOME (groups, prints) =>
   2.114 +          Inttab.update (exec_id, (groups, (fn () => pr i) :: prints)) execs
   2.115 +      | NONE => raise Fail (unregistered exec_id))
   2.116 +    end));
   2.117 +
   2.118 +fun apply_prints exec_id =
   2.119 +  (case Inttab.lookup (#2 (get_state ())) exec_id of
   2.120 +    SOME (_, prints) =>
   2.121 +      if null prints orelse null (tl prints) orelse not (Multithreading.enabled ())
   2.122 +      then List.app (fn e => e ()) (rev prints)
   2.123 +      else
   2.124 +        let
   2.125 +          val pos = Position.thread_data ();
   2.126 +          val pri =
   2.127 +            (case Future.worker_task () of
   2.128 +              SOME task => Task_Queue.pri_of_task task
   2.129 +            | NONE => 0);
   2.130 +          val futures = map (fork {name = "Execution.print", pos = pos, pri = pri}) (rev prints);
   2.131 +        in ignore (Future.joins futures) end
   2.132 +  | NONE => raise Fail (unregistered exec_id));
   2.133 +
   2.134 +
   2.135  (* cleanup *)
   2.136  
   2.137  fun purge exec_ids =
   2.138 @@ -128,7 +164,7 @@
   2.139      let
   2.140        val execs' = fold Inttab.delete_safe exec_ids execs;
   2.141        val () =
   2.142 -        (execs', ()) |-> Inttab.fold (fn (exec_id, groups) => fn () =>
   2.143 +        (execs', ()) |-> Inttab.fold (fn (exec_id, (groups, _)) => fn () =>
   2.144            if Inttab.defined execs' exec_id then ()
   2.145            else groups |> List.app (fn group =>
   2.146              if Task_Queue.is_canceled group then ()
   2.147 @@ -136,8 +172,8 @@
   2.148      in execs' end);
   2.149  
   2.150  fun reset () =
   2.151 -  Synchronized.change_result state (fn State {execs, ...} =>
   2.152 -    let val groups = Inttab.fold (append o #2) execs []
   2.153 +  change_state_result (fn (_, execs) =>
   2.154 +    let val groups = Inttab.fold (append o #1 o #2) execs []
   2.155      in (groups, init_state) end);
   2.156  
   2.157  fun shutdown () =