--- a/NEWS Wed Sep 01 23:43:45 2010 +0200
+++ b/NEWS Thu Sep 02 00:48:07 2010 +0200
@@ -23,7 +23,7 @@
at the cost of clarity of file dependencies. Recall that Isabelle/ML
files exclusively use the .ML extension. Minor INCOMPATIBILTY.
-* Various options that affect document antiquotations are now properly
+* Various options that affect pretty printing etc. are now properly
handled within the context via configuration options, instead of
unsynchronized references. There are both ML Config.T entities and
Isar declaration attributes to access these.
@@ -36,15 +36,11 @@
Thy_Output.source thy_output_source
Thy_Output.break thy_output_break
+ show_question_marks show_question_marks
+
Note that the corresponding "..._default" references may be only
changed globally at the ROOT session setup, but *not* within a theory.
-* ML structure Unsynchronized never opened, not even in Isar
-interaction mode as before. Old Unsynchronized.set etc. have been
-discontinued -- use plain := instead. This should be *rare* anyway,
-since modern tools always work via official context data, notably
-configuration options.
-
*** Pure ***
@@ -217,6 +213,15 @@
*** ML ***
+* Configuration option show_question_marks only affects regular pretty
+printing of types and terms, not raw Term.string_of_vname.
+
+* ML structure Unsynchronized never opened, not even in Isar
+interaction mode as before. Old Unsynchronized.set etc. have been
+discontinued -- use plain := instead. This should be *rare* anyway,
+since modern tools always work via official context data, notably
+configuration options.
+
* ML antiquotations @{theory} and @{theory_ref} refer to named
theories from the ancestry of the current context, not any accidental
theory loader state as before. Potential INCOMPATIBILITY, subtle