NEWS
changeset 56281 03c3d1a7c3b8
parent 56279 b4d874f6c6be
child 56285 9315d3988d73
     1.1 --- a/NEWS	Tue Mar 25 17:59:34 2014 +0100
     1.2 +++ b/NEWS	Tue Mar 25 19:03:02 2014 +0100
     1.3 @@ -545,8 +545,13 @@
     1.4  "ML_exception_trace", which may be also declared within the context via
     1.5  "declare [[ML_exception_trace = true]]".  Minor INCOMPATIBILITY.
     1.6  
     1.7 -* Renamed option "ML_trace" to "ML_source_trace". Minor
     1.8 -INCOMPATIBILITY.
     1.9 +* Renamed configuration option "ML_trace" to "ML_source_trace". Minor
    1.10 +INCOMPATIBILITY.
    1.11 +
    1.12 +* Configuration option "ML_print_depth" controls the pretty-printing
    1.13 +depth of the ML compiler within the context.  The old print_depth in
    1.14 +ML is still available as put_default_print_depth, but rarely used.
    1.15 +Minor INCOMPATIBILITY.
    1.16  
    1.17  * Proper context discipline for read_instantiate and instantiate_tac:
    1.18  variables that are meant to become schematic need to be given as