tuned signature -- channels for diagnostic output for system tools means stderr;
authorwenzelm
Fri, 02 May 2014 19:51:40 +0200
changeset 56830 e760242101fc
parent 56829 f151ade98b15
child 56831 e3ccf0809d51
tuned signature -- channels for diagnostic output for system tools means stderr;
src/Pure/General/output.ML
src/Pure/General/output.scala
src/Pure/Tools/check_source.scala
src/Pure/Tools/keywords.scala
--- 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 =
--- 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)) }
 }
--- 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
--- 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)
   }