wneuper/isa: doc-src/isabelle.sty@20e3616b2d9c

     1 %%

     2 %%

     3 %%

     4 %% macros for Isabelle generated LaTeX output

     5 %%

     7 %%% Simple document preparation (based on theory token language and symbols)

     9 % isabelle environments

    11 \newcommand{\isabellecontext}{UNKNOWN}

    13 \newcommand{\isastyle}{\UNDEF}

    14 \newcommand{\isastyleminor}{\UNDEF}

    15 \newcommand{\isastylescript}{\UNDEF}

    16 \newcommand{\isastyletext}{\normalsize\rm}

    17 \newcommand{\isastyletxt}{\rm}

    18 \newcommand{\isastylecmt}{\rm}

    20 %symbol markup -- \emph achieves decent spacing via italic corrections

    21 \newcommand{\isamath}[1]{\emph{$#1$}}

    22 \newcommand{\isatext}[1]{\emph{#1}}

    23 \DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}

    24 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}

    25 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}

    26 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}

    27 \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}

    28 \DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}

    29 \DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}

    30 \DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}

    31 \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}

    32 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}

    33 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}

    35 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}

    36 \newcommand{\isaantiqopen}{\isakeyword{\isacharbraceleft}}

    37 \newcommand{\isaantiqclose}{\isakeyword{\isacharbraceright}}

    39 \newdimen\isa@parindent\newdimen\isa@parskip

    41 \newenvironment{isabellebody}{%

    42 \isamarkuptrue\par%

    43 \isa@parindent\parindent\parindent0pt%

    44 \isa@parskip\parskip\parskip0pt%

    45 \isastyle}{\par}

    47 \newenvironment{isabelle}

    48 {\begin{trivlist}\begin{isabellebody}\item\relax}

    49 {\end{isabellebody}\end{trivlist}}

    51 \newcommand{\isa}[1]{\emph{\isastyleminor #1}}

    53 \newcommand{\isaindent}[1]{\hphantom{#1}}

    54 \newcommand{\isanewline}{\mbox{}\par\mbox{}}

    55 \newcommand{\isasep}{}

    56 \newcommand{\isadigit}[1]{#1}

    58 \newcommand{\isachardefaults}{%

    59 \chardef\isacharbang=`\!%

    60 \chardef\isachardoublequote=`\"%

    61 \chardef\isachardoublequoteopen=`\"%

    62 \chardef\isachardoublequoteclose=`\"%

    63 \chardef\isacharhash=`\#%

    64 \chardef\isachardollar=`\$%

    65 \chardef\isacharpercent=`\%%

    66 \chardef\isacharampersand=`\&%

    67 \chardef\isacharprime=`\'%

    68 \chardef\isacharparenleft=`\(%

    69 \chardef\isacharparenright=`\)%

    70 \chardef\isacharasterisk=`\*%

    71 \chardef\isacharplus=`\+%

    72 \chardef\isacharcomma=`\,%

    73 \chardef\isacharminus=`\-%

    74 \chardef\isachardot=`\.%

    75 \chardef\isacharslash=`\/%

    76 \chardef\isacharcolon=`\:%

    77 \chardef\isacharsemicolon=`\;%

    78 \chardef\isacharless=`\<%

    79 \chardef\isacharequal=`\=%

    80 \chardef\isachargreater=`\>%

    81 \chardef\isacharquery=`\?%

    82 \chardef\isacharat=`\@%

    83 \chardef\isacharbrackleft=`\[%

    84 \chardef\isacharbackslash=`\\%

    85 \chardef\isacharbrackright=`\]%

    86 \chardef\isacharcircum=`\^%

    87 \chardef\isacharunderscore=`\_%

    88 \def\isacharunderscorekeyword{\_}%

    89 \chardef\isacharbackquote=`\`%

    90 \chardef\isacharbackquoteopen=`\`%

    91 \chardef\isacharbackquoteclose=`\`%

    92 \chardef\isacharbraceleft=`\{%

    93 \chardef\isacharbar=`\|%

    94 \chardef\isacharbraceright=`\}%

    95 \chardef\isachartilde=`\~%

    96 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%

    97 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%

    98 }

   101 % keyword and section markup

   103 \newcommand{\isakeyword}[1]

   104 {\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%

   105 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}

   106 \newcommand{\isacommand}[1]{\isakeyword{#1}}

   108 \newcommand{\isamarkupheader}[1]{\section{#1}}

   109 \newcommand{\isamarkupchapter}[1]{\chapter{#1}}

   110 \newcommand{\isamarkupsection}[1]{\section{#1}}

   111 \newcommand{\isamarkupsubsection}[1]{\subsection{#1}}

   112 \newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}

   113 \newcommand{\isamarkupsect}[1]{\section{#1}}

   114 \newcommand{\isamarkupsubsect}[1]{\subsection{#1}}

   115 \newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}

   117 \newif\ifisamarkup

   118 \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}

   119 \newcommand{\isaendpar}{\par\medskip}

   120 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}

   121 \newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}

   122 \newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}

   123 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}

   126 % styles

   128 \def\isabellestyle#1{\csname isabellestyle#1\endcsname}

   130 \newcommand{\isabellestyledefault}{%

   131 \renewcommand{\isastyle}{\small\tt\slshape}%

   132 \renewcommand{\isastyleminor}{\small\tt\slshape}%

   133 \renewcommand{\isastylescript}{\footnotesize\tt\slshape}%

   134 \isachardefaults%

   135 }

   136 \isabellestyledefault

   138 \newcommand{\isabellestylett}{%

   139 \renewcommand{\isastyle}{\small\tt}%

   140 \renewcommand{\isastyleminor}{\small\tt}%

   141 \renewcommand{\isastylescript}{\footnotesize\tt}%

   142 \isachardefaults%

   143 }

   145 \newcommand{\isabellestyleit}{%

   146 \renewcommand{\isastyle}{\small\it}%

   147 \renewcommand{\isastyleminor}{\it}%

   148 \renewcommand{\isastylescript}{\footnotesize\it}%

   149 \renewcommand{\isacharunderscorekeyword}{\mbox{-}}%

   150 \renewcommand{\isacharbang}{\isamath{!}}%

   151 \renewcommand{\isachardoublequote}{}%

   152 \renewcommand{\isachardoublequoteopen}{}%

   153 \renewcommand{\isachardoublequoteclose}{}%

   154 \renewcommand{\isacharhash}{\isamath{\#}}%

   155 \renewcommand{\isachardollar}{\isamath{\$}}%

   156 \renewcommand{\isacharpercent}{\isamath{\%}}%

   157 \renewcommand{\isacharampersand}{\isamath{\&}}%

   158 \renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%

   159 \renewcommand{\isacharparenleft}{\isamath{(}}%

   160 \renewcommand{\isacharparenright}{\isamath{)}}%

   161 \renewcommand{\isacharasterisk}{\isamath{*}}%

   162 \renewcommand{\isacharplus}{\isamath{+}}%

   163 \renewcommand{\isacharcomma}{\isamath{\mathord,}}%

   164 \renewcommand{\isacharminus}{\isamath{-}}%

   165 \renewcommand{\isachardot}{\isamath{\mathord.}}%

   166 \renewcommand{\isacharslash}{\isamath{/}}%

   167 \renewcommand{\isacharcolon}{\isamath{\mathord:}}%

   168 \renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%

   169 \renewcommand{\isacharless}{\isamath{<}}%

   170 \renewcommand{\isacharequal}{\isamath{=}}%

   171 \renewcommand{\isachargreater}{\isamath{>}}%

   172 \renewcommand{\isacharat}{\isamath{@}}%

   173 \renewcommand{\isacharbrackleft}{\isamath{[}}%

   174 \renewcommand{\isacharbackslash}{\isamath{\backslash}}%

   175 \renewcommand{\isacharbrackright}{\isamath{]}}%

   176 \renewcommand{\isacharunderscore}{\mbox{-}}%

   177 \renewcommand{\isacharbraceleft}{\isamath{\{}}%

   178 \renewcommand{\isacharbar}{\isamath{\mid}}%

   179 \renewcommand{\isacharbraceright}{\isamath{\}}}%

   180 \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%

   181 \renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%

   182 \renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%

   183 \renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%

   184 \renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%

   185 }

   187 \newcommand{\isabellestylesl}{%

   188 \isabellestyleit%

   189 \renewcommand{\isastyle}{\small\sl}%

   190 \renewcommand{\isastyleminor}{\sl}%

   191 \renewcommand{\isastylescript}{\footnotesize\sl}%

   192 }

   195 % tagged regions

   197 %plain TeX version of comment package -- much faster!

   198 \let\isafmtname\fmtname\def\fmtname{plain}

   199 \usepackage{comment}

   200 \let\fmtname\isafmtname

   202 \newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}

   204 \newcommand{\isakeeptag}[1]%

   205 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}

   206 \newcommand{\isadroptag}[1]%

   207 {\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}

   208 \newcommand{\isafoldtag}[1]%

   209 {\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}

   211 \isakeeptag{theory}

   212 \isakeeptag{proof}

   213 \isakeeptag{ML}

   214 \isakeeptag{visible}

   215 \isadroptag{invisible}

   217 \IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 12 Aug 2010 15:03:34 +0200
branch	isac-from-Isabelle2009-2
changeset 37913	20e3616b2d9c
parent 27349	80273a002e37
child 39761	90a74f43174d
permissions	-rw-r--r--