# HG changeset patch
# User wenzelm
# Date 1399053100 -7200
# Node ID e760242101fcdf8d9ca56f6fb59672e5e4ecc139
# Parent  f151ade98b15699c939c58efae699e6a75f29a45
tuned signature -- channels for diagnostic output for system tools means stderr;

diff -r f151ade98b15 -r e760242101fc src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Fri May 02 19:30:34 2014 +0200
+++ b/src/Pure/General/output.ML	Fri May 02 19:51:40 2014 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/General/output.ML
     Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
 
-Isabelle output channels.
+Isabelle channels for diagnostic output.
 *)
 
 signature BASIC_OUTPUT =
diff -r f151ade98b15 -r e760242101fc src/Pure/General/output.scala
--- a/src/Pure/General/output.scala	Fri May 02 19:30:34 2014 +0200
+++ b/src/Pure/General/output.scala	Fri May 02 19:51:40 2014 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/General/output.ML
     Author:     Makarius
 
-Isabelle output channels: plain text without markup.
+Isabelle channels for diagnostic output.
 */
 
 package isabelle
@@ -12,6 +12,7 @@
   def warning_text(msg: String): String = cat_lines(split_lines(msg).map("### " + _))
   def error_text(msg: String): String = cat_lines(split_lines(msg).map("*** " + _))
 
+  def writeln(msg: String) { System.err.println(msg) }
   def warning(msg: String) { System.err.println(warning_text(msg)) }
   def error_message(msg: String) { System.err.println(error_text(msg)) }
 }
diff -r f151ade98b15 -r e760242101fc src/Pure/Tools/check_source.scala
--- a/src/Pure/Tools/check_source.scala	Fri May 02 19:30:34 2014 +0200
+++ b/src/Pure/Tools/check_source.scala	Fri May 02 19:51:40 2014 +0200
@@ -40,7 +40,7 @@
 
   def check_hg(root: Path)
   {
-    System.err.println("Checking " + root + " ...")
+    Output.writeln("Checking " + root + " ...")
     Isabelle_System.hg("--repository " + Isabelle_System.shell_path(root) + " root").check_error
     for {
       file <- Isabelle_System.hg("manifest", root).check_error.out_lines
diff -r f151ade98b15 -r e760242101fc src/Pure/Tools/keywords.scala
--- a/src/Pure/Tools/keywords.scala	Fri May 02 19:30:34 2014 +0200
+++ b/src/Pure/Tools/keywords.scala	Fri May 02 19:51:40 2014 +0200
@@ -141,7 +141,7 @@
     }
 
     val file = if (name == "") "isar-keywords.el" else "isar-keywords-" + name + ".el"
-    System.err.println(file)
+    Output.writeln(file)
     File.write(Path.explode(file), output)
   }