tuned;
authorwenzelm
Wed Mar 26 08:59:53 2014 +0100 (2014-03-26)
changeset 562859315d3988d73
parent 56284 fc4cf41d3504
child 56286 7ede6ca96c61
tuned;
NEWS
src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/Tools/proof_general_pure.ML
     1.1 --- a/NEWS	Tue Mar 25 20:12:53 2014 +0100
     1.2 +++ b/NEWS	Wed Mar 26 08:59:53 2014 +0100
     1.3 @@ -550,8 +550,8 @@
     1.4  
     1.5  * Configuration option "ML_print_depth" controls the pretty-printing
     1.6  depth of the ML compiler within the context.  The old print_depth in
     1.7 -ML is still available as put_default_print_depth, but rarely used.
     1.8 -Minor INCOMPATIBILITY.
     1.9 +ML is still available as default_print_depth, but rarely used.  Minor
    1.10 +INCOMPATIBILITY.
    1.11  
    1.12  * Proper context discipline for read_instantiate and instantiate_tac:
    1.13  variables that are meant to become schematic need to be given as
     2.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Mar 25 20:12:53 2014 +0100
     2.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Wed Mar 26 08:59:53 2014 +0100
     2.3 @@ -43,7 +43,7 @@
     2.4    if test_all @{context} then ()
     2.5    else
     2.6      (Options.default_put_bool @{option ML_exception_trace} true;
     2.7 -     put_default_print_depth 200;  (* FIXME proper ML_print_depth within context!? *)
     2.8 +     default_print_depth 200;  (* FIXME proper ML_print_depth within context!? *)
     2.9       PolyML.Compiler.maxInlineSize := 0)
    2.10  *}
    2.11  
     3.1 --- a/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 20:12:53 2014 +0100
     3.2 +++ b/src/Pure/ML-Systems/polyml.ML	Wed Mar 26 08:59:53 2014 +0100
     3.3 @@ -130,8 +130,8 @@
     3.4    val depth = Unsynchronized.ref 10;
     3.5  in
     3.6    fun get_default_print_depth () = ! depth;
     3.7 -  fun put_default_print_depth n = (depth := n; PolyML.print_depth n);
     3.8 -  val _ = put_default_print_depth 10;
     3.9 +  fun default_print_depth n = (depth := n; PolyML.print_depth n);
    3.10 +  val _ = default_print_depth 10;
    3.11  end;
    3.12  
    3.13  val error_depth = PolyML.error_depth;
     4.1 --- a/src/Pure/ML-Systems/smlnj.ML	Tue Mar 25 20:12:53 2014 +0100
     4.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Mar 26 08:59:53 2014 +0100
     4.3 @@ -57,11 +57,11 @@
     4.4    val depth = ref (10: int);
     4.5  in
     4.6    fun get_default_print_depth () = ! depth;
     4.7 -  fun put_default_print_depth n =
     4.8 +  fun default_print_depth n =
     4.9     (depth := n;
    4.10      Control.Print.printDepth := dest_int n div 2;
    4.11      Control.Print.printLength := dest_int n);
    4.12 -  val _ = put_default_print_depth 10;
    4.13 +  val _ = default_print_depth 10;
    4.14  end;
    4.15  
    4.16  val ml_make_string = "(fn _ => \"?\")";
     5.1 --- a/src/Pure/Tools/proof_general_pure.ML	Tue Mar 25 20:12:53 2014 +0100
     5.2 +++ b/src/Pure/Tools/proof_general_pure.ML	Wed Mar 26 08:59:53 2014 +0100
     5.3 @@ -77,7 +77,7 @@
     5.4    ProofGeneral.preference ProofGeneral.category_advanced_display
     5.5      NONE
     5.6      (Markup.print_int o get_default_print_depth)
     5.7 -    (put_default_print_depth o Markup.parse_int)
     5.8 +    (default_print_depth o Markup.parse_int)
     5.9      ProofGeneral.pgipint
    5.10      "print-depth"
    5.11      "Setting for the ML print depth";