clarified print depth;
authorwenzelm
Fri Mar 18 21:21:09 2016 +0100 (2016-03-18)
changeset 62672068b430e678f
parent 62671 a9ee1f240b81
child 62673 b5c57430b9dd
clarified print depth;
src/HOL/Metis.thy
src/Pure/General/pretty.ML
src/Pure/ML/ml_pretty.ML
src/Pure/Tools/ml_process.scala
     1.1 --- a/src/HOL/Metis.thy	Fri Mar 18 20:35:01 2016 +0100
     1.2 +++ b/src/HOL/Metis.thy	Fri Mar 18 21:21:09 2016 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  declare [[ML_print_depth = 0]]
     1.6  ML_file "~~/src/Tools/Metis/metis.ML"
     1.7 -declare [[ML_print_depth = 10]]
     1.8 +declare [[ML_print_depth = 20]]
     1.9  
    1.10  
    1.11  subsection \<open>Literal selection and lambda-lifting helpers\<close>
     2.1 --- a/src/Pure/General/pretty.ML	Fri Mar 18 20:35:01 2016 +0100
     2.2 +++ b/src/Pure/General/pretty.ML	Fri Mar 18 21:21:09 2016 +0100
     2.3 @@ -394,9 +394,7 @@
     2.4  
     2.5  end;
     2.6  
     2.7 -val _ =
     2.8 -  PolyML.addPrettyPrinter (fn depth => fn _ => ML_Pretty.to_polyml o to_ML (depth * 2 + 1) o quote);
     2.9 -
    2.10 +val _ = PolyML.addPrettyPrinter (fn d => fn _ => ML_Pretty.to_polyml o to_ML (d + 1) o quote);
    2.11  val _ = PolyML.addPrettyPrinter (fn _ => fn _ => to_polyml o position);
    2.12  
    2.13  end;
     3.1 --- a/src/Pure/ML/ml_pretty.ML	Fri Mar 18 20:35:01 2016 +0100
     3.2 +++ b/src/Pure/ML/ml_pretty.ML	Fri Mar 18 21:21:09 2016 +0100
     3.3 @@ -96,7 +96,7 @@
     3.4  in
     3.5    fun get_print_depth () = ! depth;
     3.6    fun print_depth n = (depth := n; PolyML.print_depth n);
     3.7 -  val _ = print_depth 10;
     3.8 +  val _ = print_depth 20;
     3.9  end;
    3.10  
    3.11  
     4.1 --- a/src/Pure/Tools/ml_process.scala	Fri Mar 18 20:35:01 2016 +0100
     4.2 +++ b/src/Pure/Tools/ml_process.scala	Fri Mar 18 21:21:09 2016 +0100
     4.3 @@ -68,13 +68,13 @@
     4.4  
     4.5      val eval_process =
     4.6        if (heaps.isEmpty)
     4.7 -        List("PolyML.print_depth 10")
     4.8 +        List("PolyML.print_depth 20")
     4.9        else
    4.10          channel match {
    4.11            case None =>
    4.12 -            List("(ML_Pretty.print_depth 10; Isabelle_Process.init_options ())")
    4.13 +            List("(ML_Pretty.print_depth 20; Isabelle_Process.init_options ())")
    4.14            case Some(ch) =>
    4.15 -            List("(ML_Pretty.print_depth 10; Isabelle_Process.init_protocol " +
    4.16 +            List("(ML_Pretty.print_depth 20; Isabelle_Process.init_protocol " +
    4.17                ML_Syntax.print_string0(ch.server_name) + ")")
    4.18          }
    4.19