| author | wenzelm | 
| Fri, 09 Oct 2020 13:12:56 +0200 | |
| changeset 72411 | b8cc129ece05 | 
| 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: 
68144diff
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 | } |