author | wenzelm |
Tue, 10 Mar 2015 20:12:30 +0100 | |
changeset 59671 | 9715eb8e9408 |
parent 57453 | 77d13a98f1c8 |
child 62297 | b886c0946308 |
permissions | -rw-r--r-- |
57453 | 1 |
/* Title: Pure/General/output.scala |
2 |
Module: PIDE |
|
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
4 |
|
56830
e760242101fc
tuned signature -- channels for diagnostic output for system tools means stderr;
wenzelm
parents:
56782
diff
changeset
|
5 |
Isabelle channels for diagnostic output. |
56782
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 |
|
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
8 |
package isabelle |
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 |
|
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
11 |
object Output |
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
12 |
{ |
59671
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
57453
diff
changeset
|
13 |
def clean_yxml(msg: String): String = |
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
57453
diff
changeset
|
14 |
try { XML.content(YXML.parse_body(msg)) } |
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
57453
diff
changeset
|
15 |
catch { case ERROR(_) => msg } |
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
16 |
|
59671
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
57453
diff
changeset
|
17 |
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
|
18 |
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
|
19 |
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
|
20 |
|
9715eb8e9408
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents:
57453
diff
changeset
|
21 |
def writeln(msg: String) { Console.err.println(writeln_text(msg)) } |
56831
e3ccf0809d51
prefer scala.Console with its support for thread-local redirection;
wenzelm
parents:
56830
diff
changeset
|
22 |
def warning(msg: String) { Console.err.println(warning_text(msg)) } |
e3ccf0809d51
prefer scala.Console with its support for thread-local redirection;
wenzelm
parents:
56830
diff
changeset
|
23 |
def error_message(msg: String) { Console.err.println(error_text(msg)) } |
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
24 |
} |