tuned signature;
authorwenzelm
Wed Mar 16 20:50:38 2016 +0100 (2016-03-16)
changeset 62638751cf9f3d433
parent 62637 0189fe0f6452
child 62639 699e86051e35
tuned signature;
src/Pure/ML/ml_syntax.scala
src/Pure/Tools/build.scala
src/Pure/Tools/ml_process.scala
     1.1 --- a/src/Pure/ML/ml_syntax.scala	Wed Mar 16 15:08:22 2016 +0100
     1.2 +++ b/src/Pure/ML/ml_syntax.scala	Wed Mar 16 20:50:38 2016 +0100
     1.3 @@ -31,7 +31,7 @@
     1.4    def print_string(str: String): String =
     1.5      quote(Symbol.iterator(str).map(print_char(_)).mkString)
     1.6  
     1.7 -  def print_string_raw(str: String): String =
     1.8 +  def print_string0(str: String): String =
     1.9      quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
    1.10  
    1.11    def print_list[A](f: A => String)(list: List[A]): String =
     2.1 --- a/src/Pure/Tools/build.scala	Wed Mar 16 15:08:22 2016 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Wed Mar 16 20:50:38 2016 +0100
     2.3 @@ -236,7 +236,7 @@
     2.4      def output_path: Option[Path] = if (do_output) Some(output) else None
     2.5      def output_save_state: String =
     2.6        if (do_output)
     2.7 -        "PolyML.SaveState.saveChild (" + ML_Syntax.print_string_raw(File.platform_path(output)) +
     2.8 +        "PolyML.SaveState.saveChild (" + ML_Syntax.print_string0(File.platform_path(output)) +
     2.9            ", List.length (PolyML.SaveState.showHierarchy ()))"
    2.10        else ""
    2.11      output.file.delete
    2.12 @@ -278,7 +278,7 @@
    2.13                  }))
    2.14              val eval =
    2.15                "Command_Line.tool0 (fn () => (" +
    2.16 -              "Build.build " + ML_Syntax.print_string_raw(File.standard_path(args_file)) +
    2.17 +              "Build.build " + ML_Syntax.print_string0(File.standard_path(args_file)) +
    2.18                (if (do_output) "; ML_Heap.share_common_data (); " + output_save_state
    2.19                 else "") + "));"
    2.20              ML_Process(info.options, parent, List("--eval", eval), cwd = info.dir.file,
     3.1 --- a/src/Pure/Tools/ml_process.scala	Wed Mar 16 15:08:22 2016 +0100
     3.2 +++ b/src/Pure/Tools/ml_process.scala	Wed Mar 16 20:50:38 2016 +0100
     3.3 @@ -50,14 +50,14 @@
     3.4        else
     3.5          List(
     3.6            "(PolyML.SaveState.loadHierarchy " +
     3.7 -            ML_Syntax.print_list(ML_Syntax.print_string_raw)(heaps) +
     3.8 +            ML_Syntax.print_list(ML_Syntax.print_string0)(heaps) +
     3.9            "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " +
    3.10 -          ML_Syntax.print_string_raw(": " + logic_name + "\n") +
    3.11 +          ML_Syntax.print_string0(": " + logic_name + "\n") +
    3.12            "); OS.Process.exit OS.Process.failure)")
    3.13  
    3.14      val eval_modes =
    3.15        if (modes.isEmpty) Nil
    3.16 -      else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_raw _)(modes))
    3.17 +      else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string0)(modes))
    3.18  
    3.19      // options
    3.20      val isabelle_process_options = Isabelle_System.tmp_file("options")
    3.21 @@ -76,7 +76,7 @@
    3.22              List("(default_print_depth 10; Isabelle_Process.init_options ())")
    3.23            case Some(ch) =>
    3.24              List("(default_print_depth 10; Isabelle_Process.init_protocol " +
    3.25 -              ML_Syntax.print_string_raw(ch.server_name) + ")")
    3.26 +              ML_Syntax.print_string0(ch.server_name) + ")")
    3.27          }
    3.28  
    3.29      // ISABELLE_TMP