1.1 --- a/src/Pure/ML/ml_process.scala Sun Oct 08 12:36:00 2017 +0200
1.2 +++ b/src/Pure/ML/ml_process.scala Sun Oct 08 12:50:18 2017 +0200
1.3 @@ -75,14 +75,14 @@
1.4 else
1.5 List(
1.6 "(PolyML.SaveState.loadHierarchy " +
1.7 - ML_Syntax.print_list(ML_Syntax.print_string0)(heaps) +
1.8 + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) +
1.9 "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
1.10 - ML_Syntax.print_string0(": " + logic_name + "\n") +
1.11 + ML_Syntax.print_string_bytes(": " + logic_name + "\n") +
1.12 "); OS.Process.exit OS.Process.failure)")
1.13
1.14 val eval_modes =
1.15 if (modes.isEmpty) Nil
1.16 - else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string0)(modes))
1.17 + else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes))
1.18
1.19 // options
1.20 val isabelle_process_options = Isabelle_System.tmp_file("options")
1.21 @@ -98,9 +98,9 @@
1.22 def print_table(table: List[(String, String)]): String =
1.23 ML_Syntax.print_list(
1.24 ML_Syntax.print_pair(
1.25 - ML_Syntax.print_string0, ML_Syntax.print_string0))(table)
1.26 + ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table)
1.27 def print_list(list: List[String]): String =
1.28 - ML_Syntax.print_list(ML_Syntax.print_string0)(list)
1.29 + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
1.30 List("Resources.init_session_base" +
1.31 " {global_theories = " + print_table(base.global_theories.toList) +
1.32 ", loaded_theories = " + print_list(base.loaded_theories.keys) +
1.33 @@ -116,7 +116,7 @@
1.34 case None =>
1.35 List("Isabelle_Process.init_options ()")
1.36 case Some(ch) =>
1.37 - List("Isabelle_Process.init_protocol " + ML_Syntax.print_string0(ch.server_name))
1.38 + List("Isabelle_Process.init_protocol " + ML_Syntax.print_string_bytes(ch.server_name))
1.39 }
1.40
1.41 // ISABELLE_TMP
1.42 @@ -178,7 +178,7 @@
1.43 Run the raw Isabelle ML process in batch mode.
1.44 """,
1.45 "T:" -> (arg =>
1.46 - eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
1.47 + eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))),
1.48 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
1.49 "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
1.50 "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),