src/Pure/ROOT.scala
changeset 80033 71d005ffa9fe
parent 79753 a66588206ec5
child 80131 68fc6839679e
equal deleted inserted replaced
80032:98808cc7b0c1 80033:71d005ffa9fe
    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