# HG changeset patch
# User wenzelm
# Date 1457266759 -3600
# Node ID c8c532b229477796c04835cf17e5eefdde7a0f1c
# Parent  aae9a2a855e0a9deeaead6892240a438286c421d
clarified ML syntax for strings concerning UTF8;

diff -r aae9a2a855e0 -r c8c532b22947 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sun Mar 06 11:59:35 2016 +0100
+++ b/src/Pure/General/symbol.scala	Sun Mar 06 13:19:19 2016 +0100
@@ -54,6 +54,12 @@
   def is_ascii_identifier(s: String): Boolean =
     s.length > 0 && is_ascii_letter(s(0)) && s.forall(is_ascii_letdig)
 
+  def ascii(c: Char): Symbol =
+  {
+    if (c > 127) error("Non-ASCII character: " + quote(c.toString))
+    else char_symbols(c.toInt)
+  }
+
 
   /* symbol matching */
 
diff -r aae9a2a855e0 -r c8c532b22947 src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Sun Mar 06 11:59:35 2016 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Sun Mar 06 13:19:19 2016 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML/ml_syntax.ML
     Author:     Makarius
 
-Basic ML syntax operations.
+Concrete ML syntax for basic values.
 *)
 
 signature ML_SYNTAX =
@@ -59,20 +59,25 @@
 fun print_option f NONE = "NONE"
   | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
 
+fun print_chr s =
+  if Symbol.is_char s then
+    (case ord s of
+      34 => "\\\""
+    | 92 => "\\\\"
+    | 9 => "\\t"
+    | 10 => "\\n"
+    | 11 => "\\f"
+    | 13 => "\\r"
+    | c =>
+        if c < 32 then "\\^" ^ chr (c + 64)
+        else if c < 127 then s
+        else "\\" ^ string_of_int c)
+  else error ("Bad character: " ^ quote s);
+
 fun print_char s =
-  if not (Symbol.is_char s) then s
-  else if s = "\"" then "\\\""
-  else if s = "\\" then "\\\\"
-  else if s = "\t" then "\\t"
-  else if s = "\n" then "\\n"
-  else if s = "\f" then "\\f"
-  else if s = "\r" then "\\r"
-  else
-    let val c = ord s in
-      if c < 32 then "\\^" ^ chr (c + ord "@")
-      else if c < 127 then s
-      else "\\" ^ string_of_int c
-    end;
+  if Symbol.is_char s then print_chr s
+  else if Symbol.is_utf8 s then translate_string print_chr s
+  else s;
 
 val print_string = quote o implode o map print_char o Symbol.explode;
 val print_strings = print_list print_string;
diff -r aae9a2a855e0 -r c8c532b22947 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)
+}
diff -r aae9a2a855e0 -r c8c532b22947 src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Mar 06 11:59:35 2016 +0100
+++ b/src/Pure/build-jars	Sun Mar 06 13:19:19 2016 +0100
@@ -55,6 +55,7 @@
   Isar/parse.scala
   Isar/token.scala
   ML/ml_lex.scala
+  ML/ml_syntax.scala
   PIDE/batch_session.scala
   PIDE/command.scala
   PIDE/command_span.scala