| author | wenzelm | 
| Sun, 17 Feb 2019 22:15:02 +0100 | |
| changeset 69817 | 5f160df596c1 | 
| parent 69458 | 5655af3ea5bd | 
| child 71379 | 942cc80ba18a | 
| 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 _  | 
|
| 65761 | 21  | 
def proper[A](x: A): Option[A] = Library.proper(x)  | 
| 65712 | 22  | 
val proper_string = Library.proper_string _  | 
| 65761 | 23  | 
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
 | 
24  | 
}  |