# HG changeset patch
# User wenzelm
# Date 1512934140 -3600
# Node ID 70576478bda95f1655b1823e99bfd4850a005c71
# Parent  af5b89bc065c504985fcd59c1f901da0506da5ad
avoid println with its extra CR on Windows;

diff -r af5b89bc065c -r 70576478bda9 src/Pure/Admin/isabelle_cronjob.scala
--- 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)
diff -r af5b89bc065c -r 70576478bda9 src/Pure/General/output.scala
--- 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")
     }
   }
 }
diff -r af5b89bc065c -r 70576478bda9 src/Pure/System/getopts.scala
--- 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)
   }
 
diff -r af5b89bc065c -r 70576478bda9 src/Pure/System/isabelle_process.scala
--- 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 =
diff -r af5b89bc065c -r 70576478bda9 src/Pure/System/options.scala
--- 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)
   })
 }
 
diff -r af5b89bc065c -r 70576478bda9 src/Pure/System/progress.scala
--- 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 =
diff -r af5b89bc065c -r 70576478bda9 src/Pure/Tools/doc.scala
--- 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 {
diff -r af5b89bc065c -r 70576478bda9 src/Pure/Tools/server.scala
--- 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)
       }
     })
diff -r af5b89bc065c -r 70576478bda9 src/Tools/jEdit/src/scala_console.scala
--- 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) }
   }