src/Pure/Tools/print_operation.ML
changeset 82583 abd3885a3fcf
parent 76403 fb9c567a67cd
--- a/src/Pure/Tools/print_operation.ML	Thu Apr 24 21:39:40 2025 +0200
+++ b/src/Pure/Tools/print_operation.ML	Thu Apr 24 22:45:04 2025 +0200
@@ -40,7 +40,7 @@
 
 val _ =
   Query_Operation.register {name = "print_operation", pri = Task_Queue.urgent_pri}
-    (fn {state, args, writeln_result, ...} =>
+    (fn {state, args, writelns_result, ...} =>
       let
         val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
         fun err s = Pretty.mark_str (Markup.bad (), s);
@@ -48,7 +48,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 writeln_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
+      in writelns_result (Pretty.strings_of (Pretty.chunks (maps print args))) end);
 
 end;