author | wenzelm |
Tue, 29 Apr 2014 13:32:13 +0200 | |
changeset 56782 | 433cf57550fa |
child 56830 | e760242101fc |
permissions | -rw-r--r-- |
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/General/output.ML |
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 |
|
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
4 |
Isabelle output channels: plain text without markup. |
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 |
{ |
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
12 |
def warning_text(msg: String): String = cat_lines(split_lines(msg).map("### " + _)) |
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
13 |
def error_text(msg: String): String = cat_lines(split_lines(msg).map("*** " + _)) |
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
14 |
|
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
15 |
def warning(msg: String) { System.err.println(warning_text(msg)) } |
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
16 |
def error_message(msg: String) { System.err.println(error_text(msg)) } |
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
17 |
} |
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff
changeset
|
18 |