| author | wenzelm | 
| Tue, 05 Nov 2024 23:51:44 +0100 | |
| changeset 81354 | a1567e05f7fd | 
| parent 80817 | e31ebb2be437 | 
| child 83265 | b11587195c70 | 
| permissions | -rw-r--r-- | 
| 57453 | 1 | /* Title: Pure/General/output.scala | 
| 56782 
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
 wenzelm parents: diff
changeset | 2 | Author: Makarius | 
| 
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
 wenzelm parents: diff
changeset | 3 | |
| 77500 | 4 | Console output channels. | 
| 56782 
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
 wenzelm parents: diff
changeset | 5 | */ | 
| 
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
 wenzelm parents: diff
changeset | 6 | |
| 
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
 wenzelm parents: diff
changeset | 7 | package isabelle | 
| 
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
 wenzelm parents: diff
changeset | 8 | |
| 
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
 wenzelm parents: diff
changeset | 9 | |
| 75393 | 10 | object Output {
 | 
| 80817 | 11 | def writeln_text(msg: String): String = Protocol_Message.clean_output(msg) | 
| 65828 | 12 | |
| 71647 | 13 |   def warning_prefix(s: String): String = Library.prefix_lines("### ", s)
 | 
| 80817 | 14 | def warning_text(msg: String): String = warning_prefix(Protocol_Message.clean_output(msg)) | 
| 65828 | 15 | |
| 77501 | 16 |   def error_message_prefix(s: String): String = Library.prefix_lines("*** ", s)
 | 
| 80817 | 17 | def error_message_text(msg: String): String = | 
| 18 | error_message_prefix(Protocol_Message.clean_output(msg)) | |
| 59671 
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
 wenzelm parents: 
57453diff
changeset | 19 | |
| 77500 | 20 | def output(s: String, stdout: Boolean = false, include_empty: Boolean = false): Unit = | 
| 21 |     if (s.nonEmpty || include_empty) {
 | |
| 22 | if (stdout) Console.print(s + "\n") else Console.err.print(s + "\n") | |
| 62553 | 23 | } | 
| 24 | ||
| 77500 | 25 | def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit = | 
| 26 | output(writeln_text(msg), stdout = stdout, include_empty = include_empty) | |
| 62553 | 27 | |
| 77500 | 28 | def warning(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit = | 
| 29 | output(warning_text(msg), stdout = stdout, include_empty = include_empty) | |
| 30 | ||
| 31 | def error_message(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit = | |
| 32 | output(error_message_text(msg), stdout = stdout, include_empty = include_empty) | |
| 56782 
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
 wenzelm parents: diff
changeset | 33 | } |