--- a/src/Pure/Tools/print_operation.ML Mon Sep 21 21:46:14 2015 +0200
+++ b/src/Pure/Tools/print_operation.ML Mon Sep 21 23:22:11 2015 +0200
@@ -46,7 +46,7 @@
val _ =
Query_Operation.register {name = "print_operation", pri = Task_Queue.urgent_pri}
- (fn {state, args, output_result} =>
+ (fn {state, args, writeln_result, ...} =>
let
val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
fun err s = Pretty.mark_str (Markup.bad, s);
@@ -54,7 +54,7 @@
(case AList.lookup (op =) (Synchronized.value print_operations) name of
SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
| NONE => [err ("Unknown print operation: " ^ quote name)]);
- in output_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
+ in writeln_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
end;