src/Pure/ROOT.scala
changeset 79528 667cb8b79909
parent 79508 b2861a2c2aa2
child 79749 a861b0df74b4
equal deleted inserted replaced
79527:f1f08ca40d96 79528:667cb8b79909
    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