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