NEWS
changeset 67448 dbb1f02e667d
parent 67446 1f4d167b6ac9
child 67507 5db077cfe1b2
     1.1 --- a/NEWS	Tue Jan 16 11:30:03 2018 +0100
     1.2 +++ b/NEWS	Tue Jan 16 15:42:21 2018 +0100
     1.3 @@ -123,8 +123,14 @@
     1.4  
     1.5  *** Document preparation ***
     1.6  
     1.7 -* \<^cancel>\<open>text\<close> cancels unused text within inner syntax: it is ignored within
     1.8 -the formal language, but shown in the document with strike-out style.
     1.9 +* Formal comments work uniformly in outer syntax, inner syntax (term
    1.10 +language), Isabelle/ML and some other embedded languages of Isabelle.
    1.11 +See also "Document comments" in the isar-ref manual. The following forms
    1.12 +are supported:
    1.13 +
    1.14 +  - marginal text comment: \<comment> \<open>\<dots>\<close>
    1.15 +  - canceled source: \<^cancel>\<open>\<dots>\<close>
    1.16 +  - raw LaTeX: \<^latex>\<open>\<dots>\<close>
    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