doc-src/IsarRef/Thy/document/Document_Preparation.tex
changeset 30397 b6212ae21656
parent 30172 afdf7808cfd0
child 32893 dbef0e6438ec
     1.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon Mar 09 21:23:40 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon Mar 09 21:25:33 2009 +0100
     1.3 @@ -335,59 +335,62 @@
     1.4  
     1.5    \begin{description}
     1.6  
     1.7 -  \item \isa{{\isachardoublequote}show{\isacharunderscore}types\ {\isacharequal}\ bool{\isachardoublequote}} and \isa{{\isachardoublequote}show{\isacharunderscore}sorts\ {\isacharequal}\ bool{\isachardoublequote}}
     1.8 -  control printing of explicit type and sort constraints.
     1.9 +  \item \indexdef{}{antiquotation option}{show\_types}\hypertarget{antiquotation option.show-types}{\hyperlink{antiquotation option.show-types}{\mbox{\isa{show{\isacharunderscore}types}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} and
    1.10 +  \indexdef{}{antiquotation option}{show\_sorts}\hypertarget{antiquotation option.show-sorts}{\hyperlink{antiquotation option.show-sorts}{\mbox{\isa{show{\isacharunderscore}sorts}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} control
    1.11 +  printing of explicit type and sort constraints.
    1.12  
    1.13 -  \item \isa{{\isachardoublequote}show{\isacharunderscore}structs\ {\isacharequal}\ bool{\isachardoublequote}} controls printing of implicit
    1.14 -  structures.
    1.15 +  \item \indexdef{}{antiquotation option}{show\_structs}\hypertarget{antiquotation option.show-structs}{\hyperlink{antiquotation option.show-structs}{\mbox{\isa{show{\isacharunderscore}structs}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
    1.16 +  controls printing of implicit structures.
    1.17  
    1.18 -  \item \isa{{\isachardoublequote}long{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}} forces names of types and
    1.19 -  constants etc.\ to be printed in their fully qualified internal
    1.20 -  form.
    1.21 +  \item \indexdef{}{antiquotation option}{long\_names}\hypertarget{antiquotation option.long-names}{\hyperlink{antiquotation option.long-names}{\mbox{\isa{long{\isacharunderscore}names}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} forces
    1.22 +  names of types and constants etc.\ to be printed in their fully
    1.23 +  qualified internal form.
    1.24  
    1.25 -  \item \isa{{\isachardoublequote}short{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}} forces names of types and
    1.26 -  constants etc.\ to be printed unqualified.  Note that internalizing
    1.27 -  the output again in the current context may well yield a different
    1.28 -  result.
    1.29 +  \item \indexdef{}{antiquotation option}{short\_names}\hypertarget{antiquotation option.short-names}{\hyperlink{antiquotation option.short-names}{\mbox{\isa{short{\isacharunderscore}names}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
    1.30 +  forces names of types and constants etc.\ to be printed unqualified.
    1.31 +  Note that internalizing the output again in the current context may
    1.32 +  well yield a different result.
    1.33  
    1.34 -  \item \isa{{\isachardoublequote}unique{\isacharunderscore}names\ {\isacharequal}\ bool{\isachardoublequote}} determines whether the printed
    1.35 -  version of qualified names should be made sufficiently long to avoid
    1.36 -  overlap with names declared further back.  Set to \isa{false} for
    1.37 -  more concise output.
    1.38 +  \item \indexdef{}{antiquotation option}{unique\_names}\hypertarget{antiquotation option.unique-names}{\hyperlink{antiquotation option.unique-names}{\mbox{\isa{unique{\isacharunderscore}names}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
    1.39 +  determines whether the printed version of qualified names should be
    1.40 +  made sufficiently long to avoid overlap with names declared further
    1.41 +  back.  Set to \isa{false} for more concise output.
    1.42  
    1.43 -  \item \isa{{\isachardoublequote}eta{\isacharunderscore}contract\ {\isacharequal}\ bool{\isachardoublequote}} prints terms in \isa{{\isasymeta}}-contracted form.
    1.44 +  \item \indexdef{}{antiquotation option}{eta\_contract}\hypertarget{antiquotation option.eta-contract}{\hyperlink{antiquotation option.eta-contract}{\mbox{\isa{eta{\isacharunderscore}contract}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}}
    1.45 +  prints terms in \isa{{\isasymeta}}-contracted form.
    1.46  
    1.47 -  \item \isa{{\isachardoublequote}display\ {\isacharequal}\ bool{\isachardoublequote}} indicates if the text is to be output
    1.48 -  as multi-line ``display material'', rather than a small piece of
    1.49 -  text without line breaks (which is the default).
    1.50 +  \item \indexdef{}{antiquotation option}{display}\hypertarget{antiquotation option.display}{\hyperlink{antiquotation option.display}{\mbox{\isa{display}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} indicates
    1.51 +  if the text is to be output as multi-line ``display material'',
    1.52 +  rather than a small piece of text without line breaks (which is the
    1.53 +  default).
    1.54  
    1.55    In this mode the embedded entities are printed in the same style as
    1.56    the main theory text.
    1.57  
    1.58 -  \item \isa{{\isachardoublequote}break\ {\isacharequal}\ bool{\isachardoublequote}} controls line breaks in non-display
    1.59 -  material.
    1.60 +  \item \indexdef{}{antiquotation option}{break}\hypertarget{antiquotation option.break}{\hyperlink{antiquotation option.break}{\mbox{\isa{break}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} controls
    1.61 +  line breaks in non-display material.
    1.62  
    1.63 -  \item \isa{{\isachardoublequote}quotes\ {\isacharequal}\ bool{\isachardoublequote}} indicates if the output should be
    1.64 -  enclosed in double quotes.
    1.65 +  \item \indexdef{}{antiquotation option}{quotes}\hypertarget{antiquotation option.quotes}{\hyperlink{antiquotation option.quotes}{\mbox{\isa{quotes}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} indicates
    1.66 +  if the output should be enclosed in double quotes.
    1.67  
    1.68 -  \item \isa{{\isachardoublequote}mode\ {\isacharequal}\ name{\isachardoublequote}} adds \isa{name} to the print mode to
    1.69 -  be used for presentation (see also \cite{isabelle-ref}).  Note that
    1.70 -  the standard setup for {\LaTeX} output is already present by
    1.71 -  default, including the modes \isa{latex} and \isa{xsymbols}.
    1.72 +  \item \indexdef{}{antiquotation option}{mode}\hypertarget{antiquotation option.mode}{\hyperlink{antiquotation option.mode}{\mbox{\isa{mode}}}}~\isa{{\isachardoublequote}{\isacharequal}\ name{\isachardoublequote}} adds \isa{name} to the print mode to be used for presentation.  Note that the
    1.73 +  standard setup for {\LaTeX} output is already present by default,
    1.74 +  including the modes \isa{latex} and \isa{xsymbols}.
    1.75  
    1.76 -  \item \isa{{\isachardoublequote}margin\ {\isacharequal}\ nat{\isachardoublequote}} and \isa{{\isachardoublequote}indent\ {\isacharequal}\ nat{\isachardoublequote}} change the
    1.77 -  margin or indentation for pretty printing of display material.
    1.78 -
    1.79 -  \item \isa{{\isachardoublequote}goals{\isacharunderscore}limit\ {\isacharequal}\ nat{\isachardoublequote}} determines the maximum number of
    1.80 -  goals to be printed (for goal-based antiquotation).
    1.81 +  \item \indexdef{}{antiquotation option}{margin}\hypertarget{antiquotation option.margin}{\hyperlink{antiquotation option.margin}{\mbox{\isa{margin}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}} and
    1.82 +  \indexdef{}{antiquotation option}{indent}\hypertarget{antiquotation option.indent}{\hyperlink{antiquotation option.indent}{\mbox{\isa{indent}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}} change the margin
    1.83 +  or indentation for pretty printing of display material.
    1.84  
    1.85 -  \item \isa{{\isachardoublequote}locale\ {\isacharequal}\ name{\isachardoublequote}} specifies an alternative locale
    1.86 -  context used for evaluating and printing the subsequent argument.
    1.87 +  \item \indexdef{}{antiquotation option}{goals\_limit}\hypertarget{antiquotation option.goals-limit}{\hyperlink{antiquotation option.goals-limit}{\mbox{\isa{goals{\isacharunderscore}limit}}}}~\isa{{\isachardoublequote}{\isacharequal}\ nat{\isachardoublequote}}
    1.88 +  determines the maximum number of goals to be printed (for goal-based
    1.89 +  antiquotation).
    1.90  
    1.91 -  \item \isa{{\isachardoublequote}source\ {\isacharequal}\ bool{\isachardoublequote}} prints the original source text of the
    1.92 -  antiquotation arguments, rather than its internal representation.
    1.93 -  Note that formal checking of \hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}, \hyperlink{antiquotation.term}{\mbox{\isa{term}}}, etc. is still enabled; use the \hyperlink{antiquotation.text}{\mbox{\isa{text}}}
    1.94 -  antiquotation for unchecked output.
    1.95 +  \item \indexdef{}{antiquotation option}{source}\hypertarget{antiquotation option.source}{\hyperlink{antiquotation option.source}{\mbox{\isa{source}}}}~\isa{{\isachardoublequote}{\isacharequal}\ bool{\isachardoublequote}} prints the
    1.96 +  original source text of the antiquotation arguments, rather than its
    1.97 +  internal representation.  Note that formal checking of
    1.98 +  \hyperlink{antiquotation.thm}{\mbox{\isa{thm}}}, \hyperlink{antiquotation.term}{\mbox{\isa{term}}}, etc. is still
    1.99 +  enabled; use the \hyperlink{antiquotation.text}{\mbox{\isa{text}}} antiquotation for unchecked
   1.100 +  output.
   1.101  
   1.102    Regular \isa{{\isachardoublequote}term{\isachardoublequote}} and \isa{{\isachardoublequote}typ{\isachardoublequote}} antiquotations with \isa{{\isachardoublequote}source\ {\isacharequal}\ false{\isachardoublequote}} involve a full round-trip from the original source
   1.103    to an internalized logical entity back to a source form, according
   1.104 @@ -395,9 +398,10 @@
   1.105    not under direct control of the author, it may even fluctuate a bit
   1.106    as the underlying theory is changed later on.
   1.107  
   1.108 -  In contrast, \isa{{\isachardoublequote}source\ {\isacharequal}\ true{\isachardoublequote}} admits direct printing of the
   1.109 -  given source text, with the desirable well-formedness check in the
   1.110 -  background, but without modification of the printed text.
   1.111 +  In contrast, \indexdef{}{antiquotation option}{source}\hypertarget{antiquotation option.source}{\hyperlink{antiquotation option.source}{\mbox{\isa{source}}}}~\isa{{\isachardoublequote}{\isacharequal}\ true{\isachardoublequote}}
   1.112 +  admits direct printing of the given source text, with the desirable
   1.113 +  well-formedness check in the background, but without modification of
   1.114 +  the printed text.
   1.115  
   1.116    \end{description}
   1.117