src/Pure/ROOT.scala
changeset 78620 6a9c5ea774e8
parent 78593 55ca7578d3e9
child 79013 4fb5e6499da9
equal deleted inserted replaced
78619:193a24f78b00 78620:6a9c5ea774e8
    27   val proper_string = Library.proper_string _
    27   val proper_string = Library.proper_string _
    28   def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
    28   def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
    29   def if_proper[A](x: Iterable[A], body: => String): String = Library.if_proper(x, body)
    29   def if_proper[A](x: Iterable[A], body: => String): String = Library.if_proper(x, body)
    30   def if_proper(b: Boolean, body: => String): String = Library.if_proper(b, body)
    30   def if_proper(b: Boolean, body: => String): String = Library.if_proper(b, body)
    31 }
    31 }
    32