| author | wenzelm |
| Wed, 11 Nov 2020 21:00:14 +0100 | |
| changeset 72574 | d892f6d66402 |
| parent 71379 | 942cc80ba18a |
| child 73136 | ca17e9ebfdf1 |
| 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 _ |
|
| 68131 | 11 |
def cat_error(msgs: String*): Nothing = Exn.cat_error(msgs:_*) |
| 62492 | 12 |
|
|
69393
ed0824ef337e
static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents:
68144
diff
changeset
|
13 |
def using[A <: AutoCloseable, B](a: A)(f: A => B): B = Library.using(a)(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 _ |
|
| 65712 | 21 |
val proper_string = Library.proper_string _ |
| 65761 | 22 |
def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list) |
|
42720
caa4f1279154
added toplevel isabelle package -- reduce warnings with scala-2.9.0.final;
wenzelm
parents:
diff
changeset
|
23 |
} |