tuned;
authorwenzelm
Thu Mar 27 18:42:53 2014 +0100 (2014-03-27 ago)
changeset 5630506dcec23fb8d
parent 56304 40274e4f5ebf
child 56306 0fc032898b05
tuned;
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/PIDE/execution.ML
     1.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Mar 27 17:56:13 2014 +0100
     1.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Thu Mar 27 18:42:53 2014 +0100
     1.3 @@ -59,8 +59,8 @@
     1.4    in
     1.5      if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
     1.6      then
     1.7 -      Execution.print {name = "ML_Compiler.report", pos = Position.thread_data (), pri = 1}
     1.8 -        (fn _ => output ())
     1.9 +      Execution.print
    1.10 +        {name = "ML_Compiler.report", pos = Position.thread_data (), pri = 1} output
    1.11      else output ()
    1.12    end;
    1.13  
     2.1 --- a/src/Pure/PIDE/execution.ML	Thu Mar 27 17:56:13 2014 +0100
     2.2 +++ b/src/Pure/PIDE/execution.ML	Thu Mar 27 18:42:53 2014 +0100
     2.3 @@ -17,7 +17,7 @@
     2.4    val terminate: Document_ID.exec -> unit
     2.5    type params = {name: string, pos: Position.T, pri: int}
     2.6    val fork: params -> (unit -> 'a) -> 'a future
     2.7 -  val print: params -> (serial -> unit) -> unit
     2.8 +  val print: params -> (unit -> unit) -> unit
     2.9    val fork_prints: Document_ID.exec -> unit
    2.10    val purge: Document_ID.exec list -> unit
    2.11    val reset: unit -> Future.group list
    2.12 @@ -135,12 +135,11 @@
    2.13  
    2.14  (* print *)
    2.15  
    2.16 -fun print ({name, pos, pri}: params) pr =
    2.17 +fun print ({name, pos, pri}: params) e =
    2.18    change_state (apsnd (fn execs =>
    2.19      let
    2.20        val exec_id = the_default 0 (Position.parse_id pos);
    2.21 -      val i = serial ();
    2.22 -      val print = {name = name, pri = pri, body = fn () => pr i};
    2.23 +      val print = {name = name, pri = pri, body = e};
    2.24      in
    2.25        (case Inttab.lookup execs exec_id of
    2.26          SOME (groups, prints) => Inttab.update (exec_id, (groups, print :: prints)) execs