author | wenzelm |
Mon, 24 Oct 2016 12:16:12 +0200 | |
changeset 64370 | 865b39487b5d |
parent 62938 | 79f41fbdf74a |
child 65828 | 02dd430d80c5 |
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 |
|
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:
57453
diff
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:
57453
diff
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:
57453
diff
changeset
|
16 |
def writeln_text(msg: String): String = clean_yxml(msg) |
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
57453
diff
changeset
|
17 |
def warning_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("### " + _)) |
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
57453
diff
changeset
|
18 |
def error_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("*** " + _)) |
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
57453
diff
changeset
|
19 |
|
62553 | 20 |
def writeln(msg: String, stdout: Boolean = false) |
21 |
{ |
|
22 |
if (msg != "") { |
|
23 |
if (stdout) Console.println(writeln_text(msg)) |
|
24 |
else Console.err.println(writeln_text(msg)) |
|
25 |
} |
|
26 |
} |
|
27 |
||
28 |
def warning(msg: String, stdout: Boolean = false) |
|
29 |
{ |
|
30 |
if (msg != "") { |
|
31 |
if (stdout) Console.println(warning_text(msg)) |
|
32 |
else Console.err.println(warning_text(msg)) |
|
33 |
} |
|
34 |
} |
|
35 |
||
36 |
def error_message(msg: String, stdout: Boolean = false) |
|
37 |
{ |
|
38 |
if (msg != "") { |
|
39 |
if (stdout) Console.println(error_text(msg)) |
|
40 |
else Console.err.println(error_text(msg)) |
|
41 |
} |
|
42 |
} |
|
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
43 |
} |