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
 tools).
 
-\railalias{textraw}{text\_raw}
-\railterm{textraw}
-
 \begin{rail}
-  ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text' | textraw) text
+  ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') locale? text
+  ;
+  'text\_raw' text
   ;
 \end{rail}
 
@@ -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.
 \end{descr}
 
+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