proper output of raw ML;
authorwenzelm
Sun Oct 08 12:36:00 2017 +0200 (6 months ago)
changeset 66781dac4cfbfede8
parent 66780 bf54ca580bf2
child 66782 193c31b79a33
proper output of raw ML;
src/Pure/ML/ml_process.scala
     1.1 --- a/src/Pure/ML/ml_process.scala	Sat Oct 07 20:31:01 2017 +0200
     1.2 +++ b/src/Pure/ML/ml_process.scala	Sun Oct 08 12:36:00 2017 +0200
     1.3 @@ -98,9 +98,9 @@
     1.4            def print_table(table: List[(String, String)]): String =
     1.5              ML_Syntax.print_list(
     1.6                ML_Syntax.print_pair(
     1.7 -                ML_Syntax.print_string, ML_Syntax.print_string))(table)
     1.8 +                ML_Syntax.print_string0, ML_Syntax.print_string0))(table)
     1.9            def print_list(list: List[String]): String =
    1.10 -            ML_Syntax.print_list(ML_Syntax.print_string)(list)
    1.11 +            ML_Syntax.print_list(ML_Syntax.print_string0)(list)
    1.12            List("Resources.init_session_base" +
    1.13              " {global_theories = " + print_table(base.global_theories.toList) +
    1.14              ", loaded_theories = " + print_list(base.loaded_theories.keys) +