src/Doc/Isar_Ref/Outer_Syntax.thy
changeset 67448 dbb1f02e667d
parent 66916 aca50a1572c5
child 67477 44b018d4aa5f
     1.1 --- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue Jan 16 11:30:03 2018 +0100
     1.2 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue Jan 16 15:42:21 2018 +0100
     1.3 @@ -230,21 +230,48 @@
     1.4  \<close>
     1.5  
     1.6  
     1.7 -subsection \<open>Comments \label{sec:comments}\<close>
     1.8 +subsection \<open>Document text\<close>
     1.9  
    1.10  text \<open>
    1.11 -  Large chunks of plain @{syntax text} are usually given @{syntax verbatim},
    1.12 -  i.e.\ enclosed in \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>, or as @{syntax cartouche} \<open>\<open>\<dots>\<close>\<close>. For
    1.13 -  convenience, any of the smaller text units conforming to @{syntax name} are
    1.14 -  admitted as well. A marginal @{syntax comment} is of the form \<^verbatim>\<open>--\<close>~@{syntax
    1.15 -  text} or \<^verbatim>\<open>\<comment>\<close>~@{syntax text}. Any number of these may occur within
    1.16 -  Isabelle/Isar commands.
    1.17 +  A chunk of document @{syntax text} is usually given as @{syntax cartouche}
    1.18 +  \<open>\<open>\<dots>\<close>\<close> or @{syntax verbatim}, i.e.\ enclosed in \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>. For
    1.19 +  convenience, any of the smaller text unit that conforms to @{syntax name} is
    1.20 +  admitted as well.
    1.21  
    1.22    @{rail \<open>
    1.23      @{syntax_def text}: @{syntax embedded} | @{syntax verbatim}
    1.24 -    ;
    1.25 -    @{syntax_def comment}: ('--' | @'\<comment>') @{syntax text}
    1.26    \<close>}
    1.27 +
    1.28 +  Typical uses are document markup commands, like \<^theory_text>\<open>chapter\<close>, \<^theory_text>\<open>section\<close> etc.
    1.29 +  (\secref{sec:markup}).
    1.30 +\<close>
    1.31 +
    1.32 +
    1.33 +subsection \<open>Document comments \label{sec:comments}\<close>
    1.34 +
    1.35 +text \<open>
    1.36 +  Formal comments are an integral part of the document, but are logically void
    1.37 +  and removed from the resulting theory or term content. The output of
    1.38 +  document preparation (\chref{ch:document-prep}) supports various styles,
    1.39 +  according to the following kinds of comments.
    1.40 +
    1.41 +    \<^item> Marginal comment of the form \<^verbatim>\<open>\<comment>\<close>~\<open>\<open>text\<close>\<close> or \<open>\<comment> \<open>text\<close>\<close>, usually with a
    1.42 +    single space between the comment symbol and the argument cartouche. The
    1.43 +    given argument is typeset as regular text, with formal antiquotations
    1.44 +    (\secref{sec:antiq}).
    1.45 +
    1.46 +    \<^item> Canceled text of the form \<^verbatim>\<open>\<^cancel>\<close>\<open>\<open>text\<close>\<close> (no white space between the
    1.47 +    control symbol and the argument cartouche). The argument is typeset as
    1.48 +    formal Isabelle source and overlaid with a ``strike-through'' pattern,
    1.49 +    e.g. \<^theory_text>\<open>\<^cancel>\<open>bad\<close>\<close>.
    1.50 +
    1.51 +    \<^item> Raw {\LaTeX} source of the form \<^verbatim>\<open>\<^latex>\<close>\<open>\<open>argument\<close>\<close> (no white space
    1.52 +    between the control symbol and the argument cartouche). This allows to
    1.53 +    augment the generated {\TeX} source arbitrarily, without any sanity
    1.54 +    checks!
    1.55 +
    1.56 +  These formal comments work uniformly in outer syntax, inner syntax (term
    1.57 +  language), Isabelle/ML, and some other embedded languages of Isabelle.
    1.58  \<close>
    1.59  
    1.60