src/Pure/General/pretty.ML

   val output: output_ops -> T -> Bytes.T
   val string_of_ops: output_ops -> T -> string
   val string_of: T -> string
   val pure_string_of: T -> string
   val writeln: T -> unit
+  val writeln_urgent: T -> unit
   val markup_chunks: Markup.T -> T list -> T
   val chunks: T list -> T
   val chunks2: T list -> T
   val block_enclose: T * T -> T list -> T
   val writeln_chunks: T list -> unit

 fun string_of_ops ops = Bytes.content o output ops;
 fun string_of prt = string_of_ops (output_ops NONE) prt;
 
 val pure_string_of = string_of_ops (pure_output_ops NONE);
 
-fun writeln prt =
-  Output.writelns (Bytes.contents (output (output_ops NONE) prt));
+fun gen_writeln urgent prt =
+  (if urgent then Output.writelns_urgent else Output.writelns)
+    (Bytes.contents (output (output_ops NONE) prt));
+
+val writeln = gen_writeln false;
+val writeln_urgent = gen_writeln true;
 
 
 (* chunks *)
 
 fun markup_chunks m prts = markup m (fbreaks (map (text_fold o single) prts));