src/Pure/General/output.ML
changeset 63517 8ea738cffabe
parent 62930 51ac6bc389e8
child 65301 fca593a62785
equal deleted inserted replaced
63516:76492eaf3dc1 63517:8ea738cffabe
   122 val _ =
   122 val _ =
   123   if Thread_Data.is_virtual then ()
   123   if Thread_Data.is_virtual then ()
   124   else
   124   else
   125    (writeln_fn := (physical_writeln o implode);
   125    (writeln_fn := (physical_writeln o implode);
   126     state_fn := (fn ss => ! writeln_fn ss);
   126     state_fn := (fn ss => ! writeln_fn ss);
   127     information_fn := (fn ss => ! writeln_fn ss);
       
   128     tracing_fn := (fn ss => ! writeln_fn ss);
   127     tracing_fn := (fn ss => ! writeln_fn ss);
   129     warning_fn := (physical_writeln o prefix_lines "### " o implode);
   128     warning_fn := (physical_writeln o prefix_lines "### " o implode);
   130     legacy_fn := (fn ss => ! warning_fn ss);
   129     legacy_fn := (fn ss => ! warning_fn ss);
   131     error_message_fn := (fn (_, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
   130     error_message_fn := (fn (_, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
   132     system_message_fn := (fn ss => ! writeln_fn ss);
   131     system_message_fn := (fn ss => ! writeln_fn ss);