src/Pure/Concurrent/future.ML

--- a/src/Pure/Concurrent/future.ML	Sun Mar 30 21:24:59 2014 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Mar 31 10:28:08 2014 +0200
@@ -56,7 +56,7 @@
   val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val cancel_group: group -> unit
   val cancel: 'a future -> unit
-  val error_msg: Position.T -> (serial * string) * string option -> unit
+  val error_message: Position.T -> (serial * string) * string option -> unit
   val identify_result: Position.T -> 'a Exn.result -> 'a Exn.result
   type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
   val default_params: params
@@ -210,7 +210,7 @@
         ("workers_active", Markup.print_int active),
         ("workers_waiting", Markup.print_int waiting)] @
         ML_Statistics.get ();
-    in Output.try_protocol_message (Markup.ML_statistics :: stats) "" end
+    in Output.try_protocol_message (Markup.ML_statistics :: stats) [] end
   else ();
 
 
@@ -257,7 +257,7 @@
           fold (fn job => fn ok => job valid andalso ok) jobs true) ());
     val _ =
       if ! Multithreading.trace >= 2 then
-        Output.try_protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) ""
+        Output.try_protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) []
       else ();
     val _ = SYNCHRONIZED "finish" (fn () =>
       let
@@ -434,7 +434,7 @@
 
 (* results *)
 
-fun error_msg pos ((serial, msg), exec_id) =
+fun error_message pos ((serial, msg), exec_id) =
   Position.setmp_thread_data pos (fn () =>
     let val id = Position.get_id pos in
       if is_none id orelse is_none exec_id orelse id = exec_id