tuned signature -- channels for diagnostic output for system tools means stderr;
authorwenzelm
Fri May 02 19:51:40 2014 +0200 (2014-05-02)
changeset 56830e760242101fc
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
     1.1 --- a/src/Pure/General/output.ML	Fri May 02 19:30:34 2014 +0200
     1.2 +++ b/src/Pure/General/output.ML	Fri May 02 19:51:40 2014 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/General/output.ML
     1.5      Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
     1.6  
     1.7 -Isabelle output channels.
     1.8 +Isabelle channels for diagnostic output.
     1.9  *)
    1.10  
    1.11  signature BASIC_OUTPUT =
     2.1 --- a/src/Pure/General/output.scala	Fri May 02 19:30:34 2014 +0200
     2.2 +++ b/src/Pure/General/output.scala	Fri May 02 19:51:40 2014 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  /*  Title:      Pure/General/output.ML
     2.5      Author:     Makarius
     2.6  
     2.7 -Isabelle output channels: plain text without markup.
     2.8 +Isabelle channels for diagnostic output.
     2.9  */
    2.10  
    2.11  package isabelle
    2.12 @@ -12,6 +12,7 @@
    2.13    def warning_text(msg: String): String = cat_lines(split_lines(msg).map("### " + _))
    2.14    def error_text(msg: String): String = cat_lines(split_lines(msg).map("*** " + _))
    2.15  
    2.16 +  def writeln(msg: String) { System.err.println(msg) }
    2.17    def warning(msg: String) { System.err.println(warning_text(msg)) }
    2.18    def error_message(msg: String) { System.err.println(error_text(msg)) }
    2.19  }
     3.1 --- a/src/Pure/Tools/check_source.scala	Fri May 02 19:30:34 2014 +0200
     3.2 +++ b/src/Pure/Tools/check_source.scala	Fri May 02 19:51:40 2014 +0200
     3.3 @@ -40,7 +40,7 @@
     3.4  
     3.5    def check_hg(root: Path)
     3.6    {
     3.7 -    System.err.println("Checking " + root + " ...")
     3.8 +    Output.writeln("Checking " + root + " ...")
     3.9      Isabelle_System.hg("--repository " + Isabelle_System.shell_path(root) + " root").check_error
    3.10      for {
    3.11        file <- Isabelle_System.hg("manifest", root).check_error.out_lines
     4.1 --- a/src/Pure/Tools/keywords.scala	Fri May 02 19:30:34 2014 +0200
     4.2 +++ b/src/Pure/Tools/keywords.scala	Fri May 02 19:51:40 2014 +0200
     4.3 @@ -141,7 +141,7 @@
     4.4      }
     4.5  
     4.6      val file = if (name == "") "isar-keywords.el" else "isar-keywords-" + name + ".el"
     4.7 -    System.err.println(file)
     4.8 +    Output.writeln(file)
     4.9      File.write(Path.explode(file), output)
    4.10    }
    4.11