src/Pure/Tools/simplifier_trace.ML

 
 
 (** markup **)
 
 fun output_result (id, data) =
-  Output.result (Markup.serial_properties id) data
+  Output.result (Markup.serial_properties id) [data]
 
 val parentN = "parent"
 val textN = "text"
 val memoryN = "memory"
 val successN = "success"

 (** tracing output **)
 
 fun send_request (result_id, content) =
   let
     fun break () =
-      (Output.protocol_message (Markup.simp_trace_cancel result_id) "";
+      (Output.protocol_message (Markup.simp_trace_cancel result_id) [];
        Synchronized.change futures (Inttab.delete_safe result_id))
     val promise = Future.promise break : string future
   in
     Synchronized.change futures (Inttab.update_new (result_id, promise));
     output_result (result_id, content);