--- a/src/Pure/Admin/isabelle_cronjob.scala Sun Dec 10 18:43:08 2017 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Sun Dec 10 20:29:00 2017 +0100
@@ -346,7 +346,7 @@
res match {
case Exn.Res(_) => None
case Exn.Exn(exn) =>
- System.err.println("Exception trace for " + quote(task.name) + ":")
+ Output.writeln("Exception trace for " + quote(task.name) + ":")
exn.printStackTrace()
val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception"
Some(first_line)
--- a/src/Pure/General/output.scala Sun Dec 10 18:43:08 2017 +0100
+++ b/src/Pure/General/output.scala Sun Dec 10 20:29:00 2017 +0100
@@ -24,24 +24,24 @@
def writeln(msg: String, stdout: Boolean = false)
{
if (msg != "") {
- if (stdout) Console.println(writeln_text(msg))
- else Console.err.println(writeln_text(msg))
+ if (stdout) Console.print(writeln_text(msg) + "\n")
+ else Console.err.print(writeln_text(msg) + "\n")
}
}
def warning(msg: String, stdout: Boolean = false)
{
if (msg != "") {
- if (stdout) Console.println(warning_text(msg))
- else Console.err.println(warning_text(msg))
+ if (stdout) Console.print(warning_text(msg) + "\n")
+ else Console.err.print(warning_text(msg) + "\n")
}
}
def error_message(msg: String, stdout: Boolean = false)
{
if (msg != "") {
- if (stdout) Console.println(error_message_text(msg))
- else Console.err.println(error_message_text(msg))
+ if (stdout) Console.print(error_message_text(msg) + "\n")
+ else Console.err.print(error_message_text(msg) + "\n")
}
}
}
--- a/src/Pure/System/getopts.scala Sun Dec 10 18:43:08 2017 +0100
+++ b/src/Pure/System/getopts.scala Sun Dec 10 20:29:00 2017 +0100
@@ -29,7 +29,7 @@
{
def usage(): Nothing =
{
- Console.println(usage_text)
+ Output.writeln(usage_text, stdout = true)
sys.exit(1)
}
--- a/src/Pure/System/isabelle_process.scala Sun Dec 10 18:43:08 2017 +0100
+++ b/src/Pure/System/isabelle_process.scala Sun Dec 10 20:29:00 2017 +0100
@@ -41,7 +41,7 @@
modes: List[String] = Nil,
cwd: JFile = null,
env: Map[String, String] = Isabelle_System.settings(),
- receiver: Prover.Receiver = Console.println(_),
+ receiver: Prover.Receiver = (msg: Prover.Message) => Output.writeln(msg.toString, stdout = true),
xml_cache: XML.Cache = new XML.Cache(),
sessions: Option[Sessions.Structure] = None,
store: Sessions.Store = Sessions.store()): Prover =
--- a/src/Pure/System/options.scala Sun Dec 10 18:43:08 2017 +0100
+++ b/src/Pure/System/options.scala Sun Dec 10 20:29:00 2017 +0100
@@ -185,13 +185,13 @@
}
if (get_option != "")
- Console.println(options.check_name(get_option).value)
+ Output.writeln(options.check_name(get_option).value, stdout = true)
if (export_file != "")
File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
if (get_option == "" && export_file == "")
- Console.println(options.print)
+ Output.writeln(options.print, stdout = true)
})
}
--- a/src/Pure/System/progress.scala Sun Dec 10 18:43:08 2017 +0100
+++ b/src/Pure/System/progress.scala Sun Dec 10 20:29:00 2017 +0100
@@ -45,7 +45,7 @@
{
override def echo(msg: String)
{
- if (stderr) Console.err.println(msg) else Console.println(msg)
+ Output.writeln(msg, stdout = !stderr)
}
override def theory(session: String, theory: String): Unit =
--- a/src/Pure/Tools/doc.scala Sun Dec 10 18:43:08 2017 +0100
+++ b/src/Pure/Tools/doc.scala Sun Dec 10 20:29:00 2017 +0100
@@ -82,7 +82,7 @@
def view(path: Path)
{
- if (path.is_file) Console.println(Library.trim_line(File.read(path)))
+ if (path.is_file) Output.writeln(Library.trim_line(File.read(path)), stdout = true)
else {
val pdf = path.ext("pdf")
if (pdf.is_file) Isabelle_System.pdf_viewer(pdf)
@@ -103,7 +103,7 @@
val docs = getopts(args)
val entries = contents()
- if (docs.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
+ if (docs.isEmpty) Output.writeln(cat_lines(contents_lines().map(_._2)), stdout = true)
else {
docs.foreach(doc =>
entries.collectFirst { case Doc(name, _, path) if doc == name => path } match {
--- a/src/Pure/Tools/server.scala Sun Dec 10 18:43:08 2017 +0100
+++ b/src/Pure/Tools/server.scala Sun Dec 10 20:29:00 2017 +0100
@@ -134,11 +134,11 @@
if (operation_list) {
for (entry <- using(SQLite.open_database(Data.database))(list(_)) if entry.active)
- Console.println(entry.print)
+ Output.writeln(entry.print, stdout = true)
}
else {
val (entry, thread) = start(name, port)
- Console.println(entry.print)
+ Output.writeln(entry.print, stdout = true)
thread.foreach(_.join)
}
})
--- 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) }
}