# HG changeset patch
# User wenzelm
# Date 1458157838 -3600
# Node ID 751cf9f3d433c718f450b34fcfba61c958343cbf
# Parent  0189fe0f64529da0e5f80a381cac5f08a07ccf2e
tuned signature;

diff -r 0189fe0f6452 -r 751cf9f3d433 src/Pure/ML/ml_syntax.scala
--- a/src/Pure/ML/ml_syntax.scala	Wed Mar 16 15:08:22 2016 +0100
+++ b/src/Pure/ML/ml_syntax.scala	Wed Mar 16 20:50:38 2016 +0100
@@ -31,7 +31,7 @@
   def print_string(str: String): String =
     quote(Symbol.iterator(str).map(print_char(_)).mkString)
 
-  def print_string_raw(str: String): String =
+  def print_string0(str: String): String =
     quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
 
   def print_list[A](f: A => String)(list: List[A]): String =
diff -r 0189fe0f6452 -r 751cf9f3d433 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Mar 16 15:08:22 2016 +0100
+++ b/src/Pure/Tools/build.scala	Wed Mar 16 20:50:38 2016 +0100
@@ -236,7 +236,7 @@
     def output_path: Option[Path] = if (do_output) Some(output) else None
     def output_save_state: String =
       if (do_output)
-        "PolyML.SaveState.saveChild (" + ML_Syntax.print_string_raw(File.platform_path(output)) +
+        "PolyML.SaveState.saveChild (" + ML_Syntax.print_string0(File.platform_path(output)) +
           ", List.length (PolyML.SaveState.showHierarchy ()))"
       else ""
     output.file.delete
@@ -278,7 +278,7 @@
                 }))
             val eval =
               "Command_Line.tool0 (fn () => (" +
-              "Build.build " + ML_Syntax.print_string_raw(File.standard_path(args_file)) +
+              "Build.build " + ML_Syntax.print_string0(File.standard_path(args_file)) +
               (if (do_output) "; ML_Heap.share_common_data (); " + output_save_state
                else "") + "));"
             ML_Process(info.options, parent, List("--eval", eval), cwd = info.dir.file,
diff -r 0189fe0f6452 -r 751cf9f3d433 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Wed Mar 16 15:08:22 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala	Wed Mar 16 20:50:38 2016 +0100
@@ -50,14 +50,14 @@
       else
         List(
           "(PolyML.SaveState.loadHierarchy " +
-            ML_Syntax.print_list(ML_Syntax.print_string_raw)(heaps) +
+            ML_Syntax.print_list(ML_Syntax.print_string0)(heaps) +
           "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
-          ML_Syntax.print_string_raw(": " + logic_name + "\n") +
+          ML_Syntax.print_string0(": " + 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_string_raw _)(modes))
+      else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string0)(modes))
 
     // options
     val isabelle_process_options = Isabelle_System.tmp_file("options")
@@ -76,7 +76,7 @@
             List("(default_print_depth 10; Isabelle_Process.init_options ())")
           case Some(ch) =>
             List("(default_print_depth 10; Isabelle_Process.init_protocol " +
-              ML_Syntax.print_string_raw(ch.server_name) + ")")
+              ML_Syntax.print_string0(ch.server_name) + ")")
         }
 
     // ISABELLE_TMP