| author | wenzelm | 
| Mon, 28 Aug 2017 20:15:11 +0200 | |
| changeset 66530 | a3a847c4fbdb | 
| parent 65828 | 02dd430d80c5 | 
| child 67178 | 70576478bda9 | 
| 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 != "") {
 | |
| 27 | if (stdout) Console.println(writeln_text(msg)) | |
| 28 | else Console.err.println(writeln_text(msg)) | |
| 29 | } | |
| 30 | } | |
| 31 | ||
| 32 | def warning(msg: String, stdout: Boolean = false) | |
| 33 |   {
 | |
| 34 |     if (msg != "") {
 | |
| 35 | if (stdout) Console.println(warning_text(msg)) | |
| 36 | else Console.err.println(warning_text(msg)) | |
| 37 | } | |
| 38 | } | |
| 39 | ||
| 40 | def error_message(msg: String, stdout: Boolean = false) | |
| 41 |   {
 | |
| 42 |     if (msg != "") {
 | |
| 65828 | 43 | if (stdout) Console.println(error_message_text(msg)) | 
| 44 | else Console.err.println(error_message_text(msg)) | |
| 62553 | 45 | } | 
| 46 | } | |
| 56782 
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
 wenzelm parents: diff
changeset | 47 | } |