# HG changeset patch
# User wenzelm
# Date 1395942173 -3600
# Node ID 06dcec23fb8dfc41283ebb040fc42fa354034e24
# Parent  40274e4f5ebf9e3d77d07b985e7a7d8e972176e6
tuned;

diff -r 40274e4f5ebf -r 06dcec23fb8d src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Mar 27 17:56:13 2014 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Thu Mar 27 18:42:53 2014 +0100
@@ -59,8 +59,8 @@
   in
     if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
     then
-      Execution.print {name = "ML_Compiler.report", pos = Position.thread_data (), pri = 1}
-        (fn _ => output ())
+      Execution.print
+        {name = "ML_Compiler.report", pos = Position.thread_data (), pri = 1} output
     else output ()
   end;
 
diff -r 40274e4f5ebf -r 06dcec23fb8d src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Thu Mar 27 17:56:13 2014 +0100
+++ b/src/Pure/PIDE/execution.ML	Thu Mar 27 18:42:53 2014 +0100
@@ -17,7 +17,7 @@
   val terminate: Document_ID.exec -> unit
   type params = {name: string, pos: Position.T, pri: int}
   val fork: params -> (unit -> 'a) -> 'a future
-  val print: params -> (serial -> unit) -> unit
+  val print: params -> (unit -> unit) -> unit
   val fork_prints: Document_ID.exec -> unit
   val purge: Document_ID.exec list -> unit
   val reset: unit -> Future.group list
@@ -135,12 +135,11 @@
 
 (* print *)
 
-fun print ({name, pos, pri}: params) pr =
+fun print ({name, pos, pri}: params) e =
   change_state (apsnd (fn execs =>
     let
       val exec_id = the_default 0 (Position.parse_id pos);
-      val i = serial ();
-      val print = {name = name, pri = pri, body = fn () => pr i};
+      val print = {name = name, pri = pri, body = e};
     in
       (case Inttab.lookup execs exec_id of
         SOME (groups, prints) => Inttab.update (exec_id, (groups, print :: prints)) execs