src/Pure/ROOT.scala
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 65761 ce909161d030
child 67885 839a624aabb9
permissions -rw-r--r--
more robust sorted_entries;
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@62492
    11
  val cat_error = Exn.cat_error _
wenzelm@62492
    12
wenzelm@63789
    13
  def using[A <: { def close() }, B](x: A)(f: A => B): B = Library.using(x)(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
}