--- a/NEWS Fri Jan 12 20:19:59 2018 +0100
+++ b/NEWS Sat Jan 13 11:22:46 2018 +0100
@@ -118,6 +118,11 @@
*** Document preparation ***
+* Unused formal text within inner syntax may be marked as
+\<^cancel>\<open>text\<close>. Thus it is ignored within the formal language, but
+still printed in the document (with special markup). This is an official
+way to "comment-out" some text.
+
* Embedded languages such as inner syntax and ML may contain formal
comments of the form "\<comment> \<open>text\<close>". As in marginal comments of outer
syntax, antiquotations are interpreted wrt. the presentation context of