# HG changeset patch
# User wenzelm
# Date 1507459823 -7200
# Node ID df1f43d477f5b5f9166f12dbc22d6e082a0cbc55
# Parent  bbe87f1b5e5d7929635055588e5630661f507eaf# Parent  193c31b79a33806de7c6f04f1329eb4d902dcad6
merged

diff -r bbe87f1b5e5d -r df1f43d477f5 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Sun Oct 08 12:42:20 2017 +0200
+++ b/src/Pure/ML/ml_process.scala	Sun Oct 08 12:50:23 2017 +0200
@@ -75,14 +75,14 @@
       else
         List(
           "(PolyML.SaveState.loadHierarchy " +
-            ML_Syntax.print_list(ML_Syntax.print_string0)(heaps) +
+            ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) +
           "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
-          ML_Syntax.print_string0(": " + logic_name + "\n") +
+          ML_Syntax.print_string_bytes(": " + logic_name + "\n") +
           "); OS.Process.exit OS.Process.failure)")
 
     val eval_modes =
       if (modes.isEmpty) Nil
-      else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string0)(modes))
+      else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes))
 
     // options
     val isabelle_process_options = Isabelle_System.tmp_file("options")
@@ -98,9 +98,9 @@
           def print_table(table: List[(String, String)]): String =
             ML_Syntax.print_list(
               ML_Syntax.print_pair(
-                ML_Syntax.print_string, ML_Syntax.print_string))(table)
+                ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table)
           def print_list(list: List[String]): String =
-            ML_Syntax.print_list(ML_Syntax.print_string)(list)
+            ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
           List("Resources.init_session_base" +
             " {global_theories = " + print_table(base.global_theories.toList) +
             ", loaded_theories = " + print_list(base.loaded_theories.keys) +
@@ -116,7 +116,7 @@
           case None =>
             List("Isabelle_Process.init_options ()")
           case Some(ch) =>
-            List("Isabelle_Process.init_protocol " + ML_Syntax.print_string0(ch.server_name))
+            List("Isabelle_Process.init_protocol " + ML_Syntax.print_string_bytes(ch.server_name))
         }
 
     // ISABELLE_TMP
@@ -178,7 +178,7 @@
   Run the raw Isabelle ML process in batch mode.
 """,
       "T:" -> (arg =>
-        eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
+        eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
       "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
diff -r bbe87f1b5e5d -r df1f43d477f5 src/Pure/ML/ml_syntax.scala
--- a/src/Pure/ML/ml_syntax.scala	Sun Oct 08 12:42:20 2017 +0200
+++ b/src/Pure/ML/ml_syntax.scala	Sun Oct 08 12:50:23 2017 +0200
@@ -20,7 +20,7 @@
 
   /* string */
 
-  private def print_chr(c: Byte): String =
+  private def print_byte(c: Byte): String =
     c match {
       case 34 => "\\\""
       case 92 => "\\\\"
@@ -35,15 +35,15 @@
         else "\\" + Library.signed_string_of_int(c)
     }
 
-  def print_char(s: Symbol.Symbol): String =
+  private def print_symbol(s: Symbol.Symbol): String =
     if (s.startsWith("\\<")) s
-    else UTF8.bytes(s).iterator.map(print_chr(_)).mkString
+    else UTF8.bytes(s).iterator.map(print_byte(_)).mkString
 
-  def print_string(str: String): String =
-    quote(Symbol.iterator(str).map(print_char(_)).mkString)
+  def print_string_bytes(str: String): String =
+    quote(UTF8.bytes(str).iterator.map(print_byte(_)).mkString)
 
-  def print_string0(str: String): String =
-    quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
+  def print_string_symbols(str: String): String =
+    quote(Symbol.iterator(str).map(print_symbol(_)).mkString)
 
 
   /* pair */
diff -r bbe87f1b5e5d -r df1f43d477f5 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Oct 08 12:42:20 2017 +0200
+++ b/src/Pure/Tools/build.scala	Sun Oct 08 12:50:23 2017 +0200
@@ -228,7 +228,7 @@
 
         def save_heap: String =
           "ML_Heap.share_common_data (); ML_Heap.save_child " +
-            ML_Syntax.print_string0(File.platform_path(output))
+            ML_Syntax.print_string_bytes(File.platform_path(output))
 
         if (pide && !Sessions.is_pure(name)) {
           val resources = new Resources(deps(parent))
@@ -262,7 +262,7 @@
 
           val eval =
             "Command_Line.tool0 (fn () => (" +
-            "Build.build " + ML_Syntax.print_string0(File.standard_path(args_file)) +
+            "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) +
             (if (do_output) "; " + save_heap else "") + "));"
 
           val process =