clarified signature;
authorwenzelm
Sun Oct 08 12:50:18 2017 +0200 (8 months ago)
changeset 66782193c31b79a33
parent 66781 dac4cfbfede8
child 66784 df1f43d477f5
clarified signature;
src/Pure/ML/ml_process.scala
src/Pure/ML/ml_syntax.scala
src/Pure/Tools/build.scala
     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)),
     2.1 --- a/src/Pure/ML/ml_syntax.scala	Sun Oct 08 12:36:00 2017 +0200
     2.2 +++ b/src/Pure/ML/ml_syntax.scala	Sun Oct 08 12:50:18 2017 +0200
     2.3 @@ -20,7 +20,7 @@
     2.4  
     2.5    /* string */
     2.6  
     2.7 -  private def print_chr(c: Byte): String =
     2.8 +  private def print_byte(c: Byte): String =
     2.9      c match {
    2.10        case 34 => "\\\""
    2.11        case 92 => "\\\\"
    2.12 @@ -35,15 +35,15 @@
    2.13          else "\\" + Library.signed_string_of_int(c)
    2.14      }
    2.15  
    2.16 -  def print_char(s: Symbol.Symbol): String =
    2.17 +  private def print_symbol(s: Symbol.Symbol): String =
    2.18      if (s.startsWith("\\<")) s
    2.19 -    else UTF8.bytes(s).iterator.map(print_chr(_)).mkString
    2.20 +    else UTF8.bytes(s).iterator.map(print_byte(_)).mkString
    2.21  
    2.22 -  def print_string(str: String): String =
    2.23 -    quote(Symbol.iterator(str).map(print_char(_)).mkString)
    2.24 +  def print_string_bytes(str: String): String =
    2.25 +    quote(UTF8.bytes(str).iterator.map(print_byte(_)).mkString)
    2.26  
    2.27 -  def print_string0(str: String): String =
    2.28 -    quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
    2.29 +  def print_string_symbols(str: String): String =
    2.30 +    quote(Symbol.iterator(str).map(print_symbol(_)).mkString)
    2.31  
    2.32  
    2.33    /* pair */
     3.1 --- a/src/Pure/Tools/build.scala	Sun Oct 08 12:36:00 2017 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Sun Oct 08 12:50:18 2017 +0200
     3.3 @@ -228,7 +228,7 @@
     3.4  
     3.5          def save_heap: String =
     3.6            "ML_Heap.share_common_data (); ML_Heap.save_child " +
     3.7 -            ML_Syntax.print_string0(File.platform_path(output))
     3.8 +            ML_Syntax.print_string_bytes(File.platform_path(output))
     3.9  
    3.10          if (pide && !Sessions.is_pure(name)) {
    3.11            val resources = new Resources(deps(parent))
    3.12 @@ -262,7 +262,7 @@
    3.13  
    3.14            val eval =
    3.15              "Command_Line.tool0 (fn () => (" +
    3.16 -            "Build.build " + ML_Syntax.print_string0(File.standard_path(args_file)) +
    3.17 +            "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) +
    3.18              (if (do_output) "; " + save_heap else "") + "));"
    3.19  
    3.20            val process =