# HG changeset patch
# User wenzelm
# Date 971632235 -7200
# Node ID 2a726de6e12426c07e71327f8748cd27d9e73b30
# Parent  eb28637c72ced8a18b7aa698e7aa6064ebed285a
proper symbol markup with \isamath, \isatext;
support sub/super scripts:

diff -r eb28637c72ce -r 2a726de6e124 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Fri Oct 13 18:32:08 2000 +0200
+++ b/lib/texinputs/isabelle.sty	Sun Oct 15 19:50:35 2000 +0200
@@ -14,10 +14,18 @@
 
 \newcommand{\isastyle}{\small\tt\slshape}
 \newcommand{\isastyleminor}{\small\tt\slshape}
+\newcommand{\isastylescript}{\footnotesize\tt\slshape}
 \newcommand{\isastyletext}{\normalsize\rm}
 \newcommand{\isastyletxt}{\rm}
 \newcommand{\isastylecmt}{\rm}
 
+%symbol markup -- \emph achieves decent spacing via italic corrections
+\newcommand{\isamath}[1]{\emph{$#1$}}
+\newcommand{\isatext}[1]{\emph{#1}}
+\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
+\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}_{#1}$}}
+\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}^{#1}$}}
+
 \newdimen\isa@parindent\newdimen\isa@parskip
 
 \newenvironment{isabellebody}{%
@@ -99,43 +107,46 @@
 \newcommand{\isabellestylett}{%
 \renewcommand{\isastyle}{\small\tt}%
 \renewcommand{\isastyleminor}{\small\tt}%
+\renewcommand{\isastylescript}{\footnotesize\tt}%
 }
 \newcommand{\isabellestyleit}{%
 \renewcommand{\isastyle}{\small\it}%
 \renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastylescript}{\footnotesize\it}%
 \renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
-\renewcommand{\isacharbang}{\emph{$!$}}%
+\renewcommand{\isacharbang}{\isamath{!}}%
 \renewcommand{\isachardoublequote}{}%
-\renewcommand{\isacharhash}{\emph{$\#$}}%
-\renewcommand{\isachardollar}{\emph{$\$$}}%
-\renewcommand{\isacharpercent}{\emph{$\%$}}%
-\renewcommand{\isacharampersand}{\emph{$\&$}}%
-\renewcommand{\isacharprime}{$\mskip2mu{'}\mskip-2mu$}%
-\renewcommand{\isacharparenleft}{\emph{$($}}%
-\renewcommand{\isacharparenright}{\emph{$)$}}%
-\renewcommand{\isacharasterisk}{\emph{$*$}}%
-\renewcommand{\isacharplus}{\emph{$+$}}%
-\renewcommand{\isacharcomma}{\emph{$\mathord,$}}%
-\renewcommand{\isacharminus}{\emph{$-$}}%
-\renewcommand{\isachardot}{\emph{$\mathord.$}}%
-\renewcommand{\isacharslash}{\emph{$/$}}%
-\renewcommand{\isacharcolon}{\emph{$\mathord:$}}%
-\renewcommand{\isacharsemicolon}{\emph{$\mathord;$}}%
-\renewcommand{\isacharless}{\emph{$<$}}%
-\renewcommand{\isacharequal}{\emph{$=$}}%
-\renewcommand{\isachargreater}{\emph{$>$}}%
-\renewcommand{\isacharat}{\emph{$@$}}%
-\renewcommand{\isacharbrackleft}{\emph{$[$}}%
-\renewcommand{\isacharbrackright}{\emph{$]$}}%
+\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{\isacharbrackright}{\isamath{]}}%
 \renewcommand{\isacharunderscore}{\mbox{-}}%
-\renewcommand{\isacharbraceleft}{\emph{$\{$}}%
-\renewcommand{\isacharbar}{\emph{$\mid$}}%
-\renewcommand{\isacharbraceright}{\emph{$\}$}}%
-\renewcommand{\isachartilde}{\emph{${}^\sim$}}%
+\renewcommand{\isacharbraceleft}{\isamath{\{}}%
+\renewcommand{\isacharbar}{\isamath{\mid}}%
+\renewcommand{\isacharbraceright}{\isamath{\}}}%
+\renewcommand{\isachartilde}{\isamath{{}^\sim}}%
 }
 
 \newcommand{\isabellestylesl}{%
 \isabellestyleit%
 \renewcommand{\isastyle}{\small\sl}%
 \renewcommand{\isastyleminor}{\sl}%
+\renewcommand{\isastylescript}{\footnotesize\sl}%
 }
diff -r eb28637c72ce -r 2a726de6e124 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Fri Oct 13 18:32:08 2000 +0200
+++ b/lib/texinputs/isabellesym.sty	Sun Oct 15 19:50:35 2000 +0200
@@ -14,13 +14,6 @@
 %\usepackage[only,bigsqcap]{stmaryrd}
 %\usepackage{wasysym}
 
-% Note: \emph is important for proper spacing in fake math mode, it
-% automatically inserts italic corrections around symbols wherever
-% appropriate.
-
-\newcommand{\isamath}[1]{\emph{$#1$}}
-\newcommand{\isatext}[1]{\emph{#1}}
-
 
 % symbol definitions