| author | wenzelm | 
| Wed, 19 Dec 2018 21:37:48 +0100 | |
| changeset 69482 | 186b03abb764 | 
| parent 67178 | 70576478bda9 | 
| child 71100 | f31903cc57b0 | 
| 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 | |
| 62930 
51ac6bc389e8
shared output primitives of physical/virtual Pure;
 wenzelm parents: 
62553diff
changeset | 4 | Isabelle 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 | |
| 
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
 wenzelm parents: diff
changeset | 10 | object Output | 
| 
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
 wenzelm parents: diff
changeset | 11 | {
 | 
| 59671 
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
 wenzelm parents: 
57453diff
changeset | 12 | def clean_yxml(msg: String): String = | 
| 62938 | 13 |     try { XML.content(Protocol_Message.clean_reports(YXML.parse_body(msg))) }
 | 
| 59671 
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
 wenzelm parents: 
57453diff
changeset | 14 |     catch { case ERROR(_) => msg }
 | 
| 56782 
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
 wenzelm parents: diff
changeset | 15 | |
| 59671 
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
 wenzelm parents: 
57453diff
changeset | 16 | def writeln_text(msg: String): String = clean_yxml(msg) | 
| 65828 | 17 | |
| 18 | def warning_text(msg: String): String = | |
| 19 |     cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
 | |
| 20 | ||
| 21 | def error_message_text(msg: String): String = | |
| 22 |     cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
 | |
| 59671 
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
 wenzelm parents: 
57453diff
changeset | 23 | |
| 62553 | 24 | def writeln(msg: String, stdout: Boolean = false) | 
| 25 |   {
 | |
| 26 |     if (msg != "") {
 | |
| 67178 | 27 | if (stdout) Console.print(writeln_text(msg) + "\n") | 
| 28 | else Console.err.print(writeln_text(msg) + "\n") | |
| 62553 | 29 | } | 
| 30 | } | |
| 31 | ||
| 32 | def warning(msg: String, stdout: Boolean = false) | |
| 33 |   {
 | |
| 34 |     if (msg != "") {
 | |
| 67178 | 35 | if (stdout) Console.print(warning_text(msg) + "\n") | 
| 36 | else Console.err.print(warning_text(msg) + "\n") | |
| 62553 | 37 | } | 
| 38 | } | |
| 39 | ||
| 40 | def error_message(msg: String, stdout: Boolean = false) | |
| 41 |   {
 | |
| 42 |     if (msg != "") {
 | |
| 67178 | 43 | if (stdout) Console.print(error_message_text(msg) + "\n") | 
| 44 | else Console.err.print(error_message_text(msg) + "\n") | |
| 62553 | 45 | } | 
| 46 | } | |
| 56782 
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
 wenzelm parents: diff
changeset | 47 | } |