--- 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;
--- 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