# HG changeset patch
# User wenzelm
# Date 1515357141 -3600
# Node ID e9bee1ddfe19c1cd5652b25fc35ee4cf72b7f17f
# Parent  2b11c071d01685189bf11a02f6212ebddf0a5643
clarified NEWS;

diff -r 2b11c071d016 -r e9bee1ddfe19 NEWS
--- a/NEWS	Sun Jan 07 21:28:03 2018 +0100
+++ b/NEWS	Sun Jan 07 21:32:21 2018 +0100
@@ -9,10 +9,6 @@
 
 *** General ***
 
-* Inner syntax comments may be written as "\<comment> \<open>text\<close>", similar to
-marginal comments in outer syntax: antiquotations are supported as usual
-(wrt. the overall command context).
-
 * The old 'def' command has been discontinued (legacy since
 Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
 object-logic equality or equivalence.
@@ -107,6 +103,11 @@
 
 *** Document preparation ***
 
+* 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
+the enclosing command.
+
 * System option "document_tags" specifies a default for otherwise
 untagged commands. This is occasionally useful to control the global
 visibility of commands via session options (e.g. in ROOT).