NEWS
changeset 67368 e9bee1ddfe19
parent 67356 ba226b87c69e
child 67381 146757999c8d
     1.1 --- a/NEWS	Sun Jan 07 21:28:03 2018 +0100
     1.2 +++ b/NEWS	Sun Jan 07 21:32:21 2018 +0100
     1.3 @@ -9,10 +9,6 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 -* Inner syntax comments may be written as "\<comment> \<open>text\<close>", similar to
     1.8 -marginal comments in outer syntax: antiquotations are supported as usual
     1.9 -(wrt. the overall command context).
    1.10 -
    1.11  * The old 'def' command has been discontinued (legacy since
    1.12  Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
    1.13  object-logic equality or equivalence.
    1.14 @@ -107,6 +103,11 @@
    1.15  
    1.16  *** Document preparation ***
    1.17  
    1.18 +* Embedded languages such as inner syntax and ML may contain formal
    1.19 +comments of the form "\<comment> \<open>text\<close>". As in marginal comments of outer
    1.20 +syntax, antiquotations are interpreted wrt. the presentation context of
    1.21 +the enclosing command.
    1.22 +
    1.23  * System option "document_tags" specifies a default for otherwise
    1.24  untagged commands. This is occasionally useful to control the global
    1.25  visibility of commands via session options (e.g. in ROOT).