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