src/Pure/ML/ml_syntax.scala
changeset 67493 c4e9e0c50487
parent 66782 193c31b79a33
     1.1 --- a/src/Pure/ML/ml_syntax.scala	Tue Jan 23 17:58:09 2018 +0100
     1.2 +++ b/src/Pure/ML/ml_syntax.scala	Tue Jan 23 19:25:39 2018 +0100
     1.3 @@ -56,4 +56,10 @@
     1.4  
     1.5    def print_list[A](f: A => String)(list: List[A]): String =
     1.6      "[" + commas(list.map(f)) + "]"
     1.7 +
     1.8 +
     1.9 +  /* properties */
    1.10 +
    1.11 +  def print_properties(props: Properties.T): String =
    1.12 +    print_list(print_pair(print_string_bytes(_), print_string_bytes(_))(_))(props)
    1.13  }