src/Pure/ROOT.scala
author wenzelm
Thu Aug 15 16:02:47 2019 +0200 (9 months ago)
changeset 70533 031620901fcd
parent 69458 5655af3ea5bd
child 71379 942cc80ba18a
permissions -rw-r--r--
support for (fully reconstructed) proof terms in Scala;
proper cache_typs;
wenzelm@57647
     1
/*  Title:      Pure/ROOT.scala
wenzelm@42720
     2
    Author:     Makarius
wenzelm@42720
     3
wenzelm@57647
     4
Root of isabelle package.
wenzelm@42720
     5
*/
wenzelm@42720
     6
wenzelm@62492
     7
package object isabelle
wenzelm@42720
     8
{
wenzelm@62492
     9
  val ERROR = Exn.ERROR
wenzelm@62492
    10
  val error = Exn.error _
wenzelm@68131
    11
  def cat_error(msgs: String*): Nothing = Exn.cat_error(msgs:_*)
wenzelm@62492
    12
wenzelm@69393
    13
  def using[A <: AutoCloseable, B](a: A)(f: A => B): B = Library.using(a)(f)
wenzelm@62492
    14
  val space_explode = Library.space_explode _
wenzelm@62492
    15
  val split_lines = Library.split_lines _
wenzelm@62492
    16
  val cat_lines = Library.cat_lines _
wenzelm@64173
    17
  val terminate_lines = Library.terminate_lines _
wenzelm@62492
    18
  val quote = Library.quote _
wenzelm@62492
    19
  val commas = Library.commas _
wenzelm@62492
    20
  val commas_quote = Library.commas_quote _
wenzelm@65761
    21
  def proper[A](x: A): Option[A] = Library.proper(x)
wenzelm@65712
    22
  val proper_string = Library.proper_string _
wenzelm@65761
    23
  def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
wenzelm@42720
    24
}