Markup commands 'chapter' .. 'text' support optional locale specification;
Mon, 05 Sep 2005 17:38:15 +0200
changeset 17259 dda237f1d299
parent 17258 5e1a443fb298
child 17260 df7c3b1f390a
Markup commands 'chapter' .. 'text' support optional locale specification;
--- a/NEWS	Mon Sep 05 16:47:28 2005 +0200
+++ b/NEWS	Mon Sep 05 17:38:15 2005 +0200
@@ -93,6 +93,15 @@
 document practical applications.  The ML antiquotation prints
 type-checked ML expressions verbatim.
+* Markup commands 'chapter', 'section', 'subsection', 'subsubsection',
+and 'text' support optional locale specification '(in loc)', which
+specifies the default context for interpreting antiquotations.
+For example: 'text (in LC) {* @{thm fold_cummute}*}'.
+* Option 'locale=NAME' of antiquotations specifies an alternative
+context interpreting the subsequent argument.  For example: @{thm
+[locale=LC] fold_commute}.
 * Proper output of proof terms (@{prf ...} and @{full_prf ...}) within
 a proof context.
@@ -257,10 +266,6 @@
 statements with 'includes'.  INCOMPATIBILITY: produces a different
 theorem statement in rare situations.
-* Antiquotations provide the option 'locale=NAME' to specify an
-alternative context used for evaluating and printing the subsequent
-argument, as in @{thm [locale=LC] fold_commute}, for example.
 * Locale inspection command 'print_locale' omits notes elements.  Use
 'print_locale!' to have them included in the output.
--- a/doc-src/IsarRef/pure.tex	Mon Sep 05 16:47:28 2005 +0200
+++ b/doc-src/IsarRef/pure.tex	Mon Sep 05 17:38:15 2005 +0200
@@ -119,11 +119,10 @@
 \cite{isabelle-sys} for more information on Isabelle's document preparation
-  ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text' | textraw) text
+  ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') locale? text
+  ;
+  'text\_raw' text
@@ -131,13 +130,17 @@
 \item [$\isarkeyword{chapter}$, $\isarkeyword{section}$,
   $\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter
   and section headings.
-\item [$\TEXT$] specifies paragraphs of plain text, including references to
-  formal entities (see also \S\ref{sec:antiq} on ``antiquotations'').
+\item [$\TEXT$] specifies paragraphs of plain text.
 \item [$\isarkeyword{text_raw}$] inserts {\LaTeX} source into the output,
   without additional markup.  Thus the full range of document manipulations
   becomes available.
+The $text$ argument of these markup commands (except for
+$\isarkeyword{text_raw}$) may contain references to formal entities
+(``antiquotations'', see also \S\ref{sec:antiq}).  These are interpreted in
+the present theory context, or the specified $locale$.
 Any of these markup elements corresponds to a {\LaTeX} command with the name
 prefixed by \verb,\isamarkup,.  For the sectioning commands this is a plain
 macro with a single argument, e.g.\ \verb,\isamarkupchapter{,\dots\verb,}, for