--- 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)
}