diff -r bcee022fbe30 -r abd3885a3fcf src/Pure/Tools/print_operation.ML --- 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;