NEWS
changeset 61595 3591274c607e
parent 61579 634cd44bb1d3
child 61597 53e32a9b66b8
     1.1 --- a/NEWS	Fri Nov 06 23:31:11 2015 +0100
     1.2 +++ b/NEWS	Fri Nov 06 23:31:50 2015 +0100
     1.3 @@ -79,10 +79,15 @@
     1.4  
     1.5  * There is a new short form for antiquotations with a single argument
     1.6  that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and
     1.7 -\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. The
     1.8 +\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}.
     1.9 +\<^name> without following cartouche is equivalent to @{name}. The
    1.10  standard Isabelle fonts provide glyphs to render important control
    1.11  symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
    1.12  
    1.13 +* Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with
    1.14 +corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using
    1.15 +standard LaTeX macros of the same names.
    1.16 +
    1.17  * System option "document_symbols" determines completion of Isabelle
    1.18  symbols within document source.
    1.19  
    1.20 @@ -113,13 +118,6 @@
    1.21    \<^enum>  enumerate
    1.22    \<^descr>  description
    1.23  
    1.24 -* Text may contain control symbols for markup and formatting as follows:
    1.25 -
    1.26 -  \<^noindent>   \noindent
    1.27 -  \<^smallskip>   \smallskip
    1.28 -  \<^medskip>   \medskip
    1.29 -  \<^bigskip>   \bigskip
    1.30 -
    1.31  * Command 'text_raw' has been clarified: input text is processed as in
    1.32  'text' (with antiquotations and control symbols). The key difference is
    1.33  the lack of the surrounding isabelle markup environment in output.