src/Tools/jEdit/src/scala_console.scala
changeset 67178 70576478bda9
parent 66923 914935f8a462
     1.1 --- a/src/Tools/jEdit/src/scala_console.scala	Sun Dec 10 18:43:08 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/scala_console.scala	Sun Dec 10 20:29:00 2017 +0100
     1.3 @@ -110,7 +110,7 @@
     1.4  
     1.5    private def report_error(str: String)
     1.6    {
     1.7 -    if (global_console == null || global_err == null) System.err.println(str)
     1.8 +    if (global_console == null || global_err == null) isabelle.Output.writeln(str)
     1.9      else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) }
    1.10    }
    1.11