1/* Title: Pure/ML/ml_syntax.scala 2 Author: Makarius 3 4Concrete ML syntax for basic values. 5*/ 6 7package isabelle 8 9 10object ML_Syntax 11{ 12 /* int */ 13 14 private def signed_int(s: String): String = 15 if (s(0) == '-') "~" + s.substring(1) else s 16 17 def print_int(i: Int): String = signed_int(Value.Int(i)) 18 def print_long(i: Long): String = signed_int(Value.Long(i)) 19 20 21 /* string */ 22 23 private def print_byte(c: Byte): String = 24 c match { 25 case 34 => "\\\"" 26 case 92 => "\\\\" 27 case 9 => "\\t" 28 case 10 => "\\n" 29 case 12 => "\\f" 30 case 13 => "\\r" 31 case _ => 32 if (c < 0) "\\" + Library.signed_string_of_int(256 + c) 33 else if (c < 32) new String(Array[Char](92, 94, (c + 64).toChar)) 34 else if (c < 127) Symbol.ascii(c.toChar) 35 else "\\" + Library.signed_string_of_int(c) 36 } 37 38 private def print_symbol(s: Symbol.Symbol): String = 39 if (s.startsWith("\\<")) s 40 else UTF8.bytes(s).iterator.map(print_byte(_)).mkString 41 42 def print_string_bytes(str: String): String = 43 quote(UTF8.bytes(str).iterator.map(print_byte(_)).mkString) 44 45 def print_string_symbols(str: String): String = 46 quote(Symbol.iterator(str).map(print_symbol(_)).mkString) 47 48 49 /* pair */ 50 51 def print_pair[A, B](f: A => String, g: B => String)(pair: (A, B)): String = 52 "(" + f(pair._1) + ", " + g(pair._2) + ")" 53 54 55 /* list */ 56 57 def print_list[A](f: A => String)(list: List[A]): String = 58 "[" + commas(list.map(f)) + "]" 59 60 61 /* properties */ 62 63 def print_properties(props: Properties.T): String = 64 print_list(print_pair(print_string_bytes(_), print_string_bytes(_))(_))(props) 65} 66