author | wenzelm |
Fri, 21 Apr 2017 15:26:24 +0200 | |
changeset 65534 | b6250ee6ce79 |
parent 64370 | 865b39487b5d |
child 65712 | ddd6dfc28e80 |
permissions | -rw-r--r-- |
57647 | 1 |
/* Title: Pure/ROOT.scala |
42720
caa4f1279154
added toplevel isabelle package -- reduce warnings with scala-2.9.0.final;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
caa4f1279154
added toplevel isabelle package -- reduce warnings with scala-2.9.0.final;
wenzelm
parents:
diff
changeset
|
3 |
|
57647 | 4 |
Root of isabelle package. |
42720
caa4f1279154
added toplevel isabelle package -- reduce warnings with scala-2.9.0.final;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
caa4f1279154
added toplevel isabelle package -- reduce warnings with scala-2.9.0.final;
wenzelm
parents:
diff
changeset
|
6 |
|
62492 | 7 |
package object isabelle |
42720
caa4f1279154
added toplevel isabelle package -- reduce warnings with scala-2.9.0.final;
wenzelm
parents:
diff
changeset
|
8 |
{ |
62492 | 9 |
val ERROR = Exn.ERROR |
10 |
val error = Exn.error _ |
|
11 |
val cat_error = Exn.cat_error _ |
|
12 |
||
63789 | 13 |
def using[A <: { def close() }, B](x: A)(f: A => B): B = Library.using(x)(f) |
62492 | 14 |
val space_explode = Library.space_explode _ |
15 |
val split_lines = Library.split_lines _ |
|
16 |
val cat_lines = Library.cat_lines _ |
|
64173 | 17 |
val terminate_lines = Library.terminate_lines _ |
62492 | 18 |
val quote = Library.quote _ |
19 |
val commas = Library.commas _ |
|
20 |
val commas_quote = Library.commas_quote _ |
|
42720
caa4f1279154
added toplevel isabelle package -- reduce warnings with scala-2.9.0.final;
wenzelm
parents:
diff
changeset
|
21 |
} |