author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 73340 | 0ffcad1f6130 |
child 77500 | bbb78dba6f68 |
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:
62553
diff
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 |
|
75393 | 10 |
object Output { |
59671
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
57453
diff
changeset
|
11 |
def clean_yxml(msg: String): String = |
62938 | 12 |
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:
57453
diff
changeset
|
13 |
catch { case ERROR(_) => msg } |
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
14 |
|
59671
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
57453
diff
changeset
|
15 |
def writeln_text(msg: String): String = clean_yxml(msg) |
65828 | 16 |
|
71647 | 17 |
def warning_prefix(s: String): String = Library.prefix_lines("### ", s) |
18 |
def warning_text(msg: String): String = warning_prefix(clean_yxml(msg)) |
|
65828 | 19 |
|
71647 | 20 |
def error_prefix(s: String): String = Library.prefix_lines("*** ", s) |
21 |
def error_message_text(msg: String): String = error_prefix(clean_yxml(msg)) |
|
59671
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
57453
diff
changeset
|
22 |
|
75393 | 23 |
def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit = { |
71100
f31903cc57b0
clarified Console_Progress.echo: include empty lines as in other Progress instances, especially relevant for Progress.bash (e.g. "isabelle phabricator ./bin/config help");
wenzelm
parents:
67178
diff
changeset
|
24 |
if (msg.nonEmpty || include_empty) { |
67178 | 25 |
if (stdout) Console.print(writeln_text(msg) + "\n") |
26 |
else Console.err.print(writeln_text(msg) + "\n") |
|
62553 | 27 |
} |
28 |
} |
|
29 |
||
75393 | 30 |
def warning(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit = { |
71100
f31903cc57b0
clarified Console_Progress.echo: include empty lines as in other Progress instances, especially relevant for Progress.bash (e.g. "isabelle phabricator ./bin/config help");
wenzelm
parents:
67178
diff
changeset
|
31 |
if (msg.nonEmpty || include_empty) { |
67178 | 32 |
if (stdout) Console.print(warning_text(msg) + "\n") |
33 |
else Console.err.print(warning_text(msg) + "\n") |
|
62553 | 34 |
} |
35 |
} |
|
36 |
||
75393 | 37 |
def error_message(msg: String, stdout: Boolean = false, include_empty: Boolean = false): Unit = { |
71100
f31903cc57b0
clarified Console_Progress.echo: include empty lines as in other Progress instances, especially relevant for Progress.bash (e.g. "isabelle phabricator ./bin/config help");
wenzelm
parents:
67178
diff
changeset
|
38 |
if (msg.nonEmpty || include_empty) { |
67178 | 39 |
if (stdout) Console.print(error_message_text(msg) + "\n") |
40 |
else Console.err.print(error_message_text(msg) + "\n") |
|
62553 | 41 |
} |
42 |
} |
|
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
43 |
} |