src/Pure/ML/ml_syntax.scala

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_syntax.scala	Sun Mar 06 13:19:19 2016 +0100
@@ -0,0 +1,36 @@
+/*  Title:      Pure/ML/ml_syntax.scala
+    Author:     Makarius
+
+Concrete ML syntax for basic values.
+*/
+
+package isabelle
+
+
+object ML_Syntax
+{
+  private def print_chr(c: Byte): String =
+    c match {
+      case 34 => "\\\""
+      case 92 => "\\\\"
+      case 9 => "\\t"
+      case 10 => "\\n"
+      case 12 => "\\f"
+      case 13 => "\\r"
+      case _ =>
+        if (c < 0) "\\" + Library.signed_string_of_int(256 + c)
+        else if (c < 32) new String(Array[Char](92, 94, (c + 64).toChar))
+        else if (c < 127) Symbol.ascii(c.toChar)
+        else "\\" + Library.signed_string_of_int(c)
+    }
+
+  def print_char(s: Symbol.Symbol): String =
+    if (s.startsWith("\\<")) s
+    else UTF8.bytes(s).iterator.map(print_chr(_)).mkString
+
+  def print_string(str: String): String =
+    quote(Symbol.iterator(str).map(print_char(_)).mkString)
+
+  def print_string_raw(str: String): String =
+    quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
+}