# HG changeset patch
# User wenzelm
# Date 1304262824 -7200
# Node ID f32500b4bc233c13c0597d950bbae85d3fdbd402
# Parent  96a55556639c36b0ae1fb677aec4e23a93a5622b
localized \isabellestyle;

diff -r 96a55556639c -r f32500b4bc23 NEWS
--- a/NEWS	Sun May 01 16:56:50 2011 +0200
+++ b/NEWS	Sun May 01 17:13:44 2011 +0200
@@ -83,6 +83,12 @@
 
 *** Document preparation ***
 
+* Localized \isabellestyle switch can be used within blocks or groups
+like this:
+
+  \isabellestyle{it}  %preferred default
+  {\isabellestylett @{text "typewriter stuff"}}
+
 * New term style "isub" as ad-hoc conversion of variables x1, y23 into
 subscripted form x\<^isub>1, y\<^isub>2\<^isub>3.
 
diff -r 96a55556639c -r f32500b4bc23 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Sun May 01 16:56:50 2011 +0200
+++ b/lib/texinputs/isabelle.sty	Sun May 01 17:13:44 2011 +0200
@@ -129,67 +129,68 @@
 \def\isabellestyle#1{\csname isabellestyle#1\endcsname}
 
 \newcommand{\isabellestyledefault}{%
-\renewcommand{\isastyle}{\small\tt\slshape}%
-\renewcommand{\isastyleminor}{\small\tt\slshape}%
-\renewcommand{\isastylescript}{\footnotesize\tt\slshape}%
+\def\isastyle{\small\tt\slshape}%
+\def\isastyleminor{\small\tt\slshape}%
+\def\isastylescript{\footnotesize\tt\slshape}%
 \isachardefaults%
 }
 \isabellestyledefault
 
 \newcommand{\isabellestylett}{%
-\renewcommand{\isastyle}{\small\tt}%
-\renewcommand{\isastyleminor}{\small\tt}%
-\renewcommand{\isastylescript}{\footnotesize\tt}%
+\def\isastyle{\small\tt}%
+\def\isastyleminor{\small\tt}%
+\def\isastylescript{\footnotesize\tt}%
 \isachardefaults%
 }
 
 \newcommand{\isabellestyleit}{%
-\renewcommand{\isastyle}{\small\it}%
-\renewcommand{\isastyleminor}{\it}%
-\renewcommand{\isastylescript}{\footnotesize\it}%
-\renewcommand{\isacharunderscorekeyword}{\mbox{-}}%
-\renewcommand{\isacharbang}{\isamath{!}}%
-\renewcommand{\isachardoublequote}{\isanil}%
-\renewcommand{\isachardoublequoteopen}{\isanil}%
-\renewcommand{\isachardoublequoteclose}{\isanil}%
-\renewcommand{\isacharhash}{\isamath{\#}}%
-\renewcommand{\isachardollar}{\isamath{\$}}%
-\renewcommand{\isacharpercent}{\isamath{\%}}%
-\renewcommand{\isacharampersand}{\isamath{\&}}%
-\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
-\renewcommand{\isacharparenleft}{\isamath{(}}%
-\renewcommand{\isacharparenright}{\isamath{)}}%
-\renewcommand{\isacharasterisk}{\isamath{*}}%
-\renewcommand{\isacharplus}{\isamath{+}}%
-\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
-\renewcommand{\isacharminus}{\isamath{-}}%
-\renewcommand{\isachardot}{\isamath{\mathord.}}%
-\renewcommand{\isacharslash}{\isamath{/}}%
-\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
-\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
-\renewcommand{\isacharless}{\isamath{<}}%
-\renewcommand{\isacharequal}{\isamath{=}}%
-\renewcommand{\isachargreater}{\isamath{>}}%
-\renewcommand{\isacharat}{\isamath{@}}%
-\renewcommand{\isacharbrackleft}{\isamath{[}}%
-\renewcommand{\isacharbackslash}{\isamath{\backslash}}%
-\renewcommand{\isacharbrackright}{\isamath{]}}%
-\renewcommand{\isacharunderscore}{\mbox{-}}%
-\renewcommand{\isacharbraceleft}{\isamath{\{}}%
-\renewcommand{\isacharbar}{\isamath{\mid}}%
-\renewcommand{\isacharbraceright}{\isamath{\}}}%
-\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
-\renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
-\renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
-\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
-\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
+\def\isastyle{\small\it}%
+\def\isastyleminor{\it}%
+\def\isastylescript{\footnotesize\it}%
+\isachardefaults%
+\def\isacharunderscorekeyword{\mbox{-}}%
+\def\isacharbang{\isamath{!}}%
+\def\isachardoublequote{\isanil}%
+\def\isachardoublequoteopen{\isanil}%
+\def\isachardoublequoteclose{\isanil}%
+\def\isacharhash{\isamath{\#}}%
+\def\isachardollar{\isamath{\$}}%
+\def\isacharpercent{\isamath{\%}}%
+\def\isacharampersand{\isamath{\&}}%
+\def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}%
+\def\isacharparenleft{\isamath{(}}%
+\def\isacharparenright{\isamath{)}}%
+\def\isacharasterisk{\isamath{*}}%
+\def\isacharplus{\isamath{+}}%
+\def\isacharcomma{\isamath{\mathord,}}%
+\def\isacharminus{\isamath{-}}%
+\def\isachardot{\isamath{\mathord.}}%
+\def\isacharslash{\isamath{/}}%
+\def\isacharcolon{\isamath{\mathord:}}%
+\def\isacharsemicolon{\isamath{\mathord;}}%
+\def\isacharless{\isamath{<}}%
+\def\isacharequal{\isamath{=}}%
+\def\isachargreater{\isamath{>}}%
+\def\isacharat{\isamath{@}}%
+\def\isacharbrackleft{\isamath{[}}%
+\def\isacharbackslash{\isamath{\backslash}}%
+\def\isacharbrackright{\isamath{]}}%
+\def\isacharunderscore{\mbox{-}}%
+\def\isacharbraceleft{\isamath{\{}}%
+\def\isacharbar{\isamath{\mid}}%
+\def\isacharbraceright{\isamath{\}}}%
+\def\isachartilde{\isamath{{}\sp{\sim}}}%
+\def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
+\def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
+\def\isacharverbatimopen{\isamath{\langle\!\langle}}%
+\def\isacharverbatimclose{\isamath{\rangle\!\rangle}}%
 }
 
 \newcommand{\isabellestylesl}{%
 \isabellestyleit%
-\renewcommand{\isastyle}{\small\sl}%
-\renewcommand{\isastyleminor}{\sl}%
-\renewcommand{\isastylescript}{\footnotesize\sl}%
+\def\isastyle{\small\sl}%
+\def\isastyleminor{\sl}%
+\def\isastylescript{\footnotesize\sl}%
 }