more documentation;
authorwenzelm
Tue Jan 16 15:42:21 2018 +0100 (18 months ago)
changeset 67448dbb1f02e667d
parent 67447 c98c6eb3dd4c
child 67449 1caeb087d957
more documentation;
NEWS
src/Doc/Isar_Ref/Inner_Syntax.thy
src/Doc/Isar_Ref/Outer_Syntax.thy
     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
     2.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Tue Jan 16 11:30:03 2018 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Tue Jan 16 15:42:21 2018 +0100
     2.3 @@ -567,7 +567,6 @@
     2.4      @{syntax_def (inner) str_token} & = & \<^verbatim>\<open>''\<close> \<open>\<dots>\<close> \<^verbatim>\<open>''\<close> \\
     2.5      @{syntax_def (inner) string_token} & = & \<^verbatim>\<open>"\<close> \<open>\<dots>\<close> \<^verbatim>\<open>"\<close> \\
     2.6      @{syntax_def (inner) cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
     2.7 -    @{syntax_def (inner) comment_cartouche} & = & @{verbatim "\<comment> \<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
     2.8    \end{supertabular}
     2.9    \end{center}
    2.10  
    2.11 @@ -582,10 +581,8 @@
    2.12    (inner) float_const}, provide robust access to the respective tokens: the
    2.13    syntax tree holds a syntactic constant instead of a free variable.
    2.14  
    2.15 -  A @{syntax (inner) comment_cartouche} resembles the outer syntax notation
    2.16 -  for marginal @{syntax_ref comment} (\secref{sec:comments}), but is
    2.17 -  syntactically more restrictive: only the symbol-form with \<^verbatim>\<open>\<comment>\<close> and text
    2.18 -  cartouche is supported.
    2.19 +  Formal document comments (\secref{sec:comments}) may be also used within the
    2.20 +  inner syntax.
    2.21  \<close>
    2.22  
    2.23  
     3.1 --- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue Jan 16 11:30:03 2018 +0100
     3.2 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue Jan 16 15:42:21 2018 +0100
     3.3 @@ -230,21 +230,48 @@
     3.4  \<close>
     3.5  
     3.6  
     3.7 -subsection \<open>Comments \label{sec:comments}\<close>
     3.8 +subsection \<open>Document text\<close>
     3.9  
    3.10  text \<open>
    3.11 -  Large chunks of plain @{syntax text} are usually given @{syntax verbatim},
    3.12 -  i.e.\ enclosed in \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>, or as @{syntax cartouche} \<open>\<open>\<dots>\<close>\<close>. For
    3.13 -  convenience, any of the smaller text units conforming to @{syntax name} are
    3.14 -  admitted as well. A marginal @{syntax comment} is of the form \<^verbatim>\<open>--\<close>~@{syntax
    3.15 -  text} or \<^verbatim>\<open>\<comment>\<close>~@{syntax text}. Any number of these may occur within
    3.16 -  Isabelle/Isar commands.
    3.17 +  A chunk of document @{syntax text} is usually given as @{syntax cartouche}
    3.18 +  \<open>\<open>\<dots>\<close>\<close> or @{syntax verbatim}, i.e.\ enclosed in \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>. For
    3.19 +  convenience, any of the smaller text unit that conforms to @{syntax name} is
    3.20 +  admitted as well.
    3.21  
    3.22    @{rail \<open>
    3.23      @{syntax_def text}: @{syntax embedded} | @{syntax verbatim}
    3.24 -    ;
    3.25 -    @{syntax_def comment}: ('--' | @'\<comment>') @{syntax text}
    3.26    \<close>}
    3.27 +
    3.28 +  Typical uses are document markup commands, like \<^theory_text>\<open>chapter\<close>, \<^theory_text>\<open>section\<close> etc.
    3.29 +  (\secref{sec:markup}).
    3.30 +\<close>
    3.31 +
    3.32 +
    3.33 +subsection \<open>Document comments \label{sec:comments}\<close>
    3.34 +
    3.35 +text \<open>
    3.36 +  Formal comments are an integral part of the document, but are logically void
    3.37 +  and removed from the resulting theory or term content. The output of
    3.38 +  document preparation (\chref{ch:document-prep}) supports various styles,
    3.39 +  according to the following kinds of comments.
    3.40 +
    3.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
    3.42 +    single space between the comment symbol and the argument cartouche. The
    3.43 +    given argument is typeset as regular text, with formal antiquotations
    3.44 +    (\secref{sec:antiq}).
    3.45 +
    3.46 +    \<^item> Canceled text of the form \<^verbatim>\<open>\<^cancel>\<close>\<open>\<open>text\<close>\<close> (no white space between the
    3.47 +    control symbol and the argument cartouche). The argument is typeset as
    3.48 +    formal Isabelle source and overlaid with a ``strike-through'' pattern,
    3.49 +    e.g. \<^theory_text>\<open>\<^cancel>\<open>bad\<close>\<close>.
    3.50 +
    3.51 +    \<^item> Raw {\LaTeX} source of the form \<^verbatim>\<open>\<^latex>\<close>\<open>\<open>argument\<close>\<close> (no white space
    3.52 +    between the control symbol and the argument cartouche). This allows to
    3.53 +    augment the generated {\TeX} source arbitrarily, without any sanity
    3.54 +    checks!
    3.55 +
    3.56 +  These formal comments work uniformly in outer syntax, inner syntax (term
    3.57 +  language), Isabelle/ML, and some other embedded languages of Isabelle.
    3.58  \<close>
    3.59  
    3.60