src/Pure/ML/ml_syntax.scala
changeset 66782 193c31b79a33
parent 65431 4a3e6cda3b94
     1.1 --- a/src/Pure/ML/ml_syntax.scala	Fri Apr 07 19:35:39 2017 +0200
     1.2 +++ b/src/Pure/ML/ml_syntax.scala	Sun Oct 08 12:50:18 2017 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  
     1.5    /* string */
     1.6  
     1.7 -  private def print_chr(c: Byte): String =
     1.8 +  private def print_byte(c: Byte): String =
     1.9      c match {
    1.10        case 34 => "\\\""
    1.11        case 92 => "\\\\"
    1.12 @@ -35,15 +35,15 @@
    1.13          else "\\" + Library.signed_string_of_int(c)
    1.14      }
    1.15  
    1.16 -  def print_char(s: Symbol.Symbol): String =
    1.17 +  private def print_symbol(s: Symbol.Symbol): String =
    1.18      if (s.startsWith("\\<")) s
    1.19 -    else UTF8.bytes(s).iterator.map(print_chr(_)).mkString
    1.20 +    else UTF8.bytes(s).iterator.map(print_byte(_)).mkString
    1.21  
    1.22 -  def print_string(str: String): String =
    1.23 -    quote(Symbol.iterator(str).map(print_char(_)).mkString)
    1.24 +  def print_string_bytes(str: String): String =
    1.25 +    quote(UTF8.bytes(str).iterator.map(print_byte(_)).mkString)
    1.26  
    1.27 -  def print_string0(str: String): String =
    1.28 -    quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
    1.29 +  def print_string_symbols(str: String): String =
    1.30 +    quote(Symbol.iterator(str).map(print_symbol(_)).mkString)
    1.31  
    1.32  
    1.33    /* pair */