--- 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 =
--- 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,
--- 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