lib/texinputs/isabelle.sty
author wenzelm
Thu Jun 09 17:46:25 2011 +0200 (2011-06-09)
changeset 43325 4384f4ae0574
parent 43321 0e79cd0b315f
child 43327 c835416237b3
permissions -rw-r--r--
some attempts at robust \isaspacing so that \isa{...} can be used in section headings etc. (need to avoid `\? for some reason);
     1 %%
     2 %% macros for Isabelle generated LaTeX output
     3 %%
     4 
     5 %%% Simple document preparation (based on theory token language and symbols)
     6 
     7 % isabelle environments
     8 
     9 \newcommand{\isabellecontext}{UNKNOWN}
    10 
    11 \newcommand{\isastyle}{\UNDEF}
    12 \newcommand{\isastyleminor}{\UNDEF}
    13 \newcommand{\isastylescript}{\UNDEF}
    14 \newcommand{\isastyletext}{\normalsize\rm}
    15 \newcommand{\isastyletxt}{\rm}
    16 \newcommand{\isastylecmt}{\rm}
    17 
    18 \newcommand{\isaspacing}{\sfcode`\.1000 \sfcode 63 1000 \sfcode`\!1000
    19   \sfcode`\:1000 \sfcode`\;1000 \sfcode`\,1000}
    20 
    21 %symbol markup -- \emph achieves decent spacing via italic corrections
    22 \newcommand{\isamath}[1]{\emph{$#1$}}
    23 \newcommand{\isatext}[1]{\emph{#1}}
    24 \DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}}
    25 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    26 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    27 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    28 \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    29 \DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript}
    30 \DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
    31 \DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
    32 \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
    33 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
    34 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
    35 
    36 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
    37 \newcommand{\isaantiqopen}{\isakeyword{\isacharbraceleft}}
    38 \newcommand{\isaantiqclose}{\isakeyword{\isacharbraceright}}
    39 
    40 \newdimen\isa@parindent\newdimen\isa@parskip
    41 
    42 \newenvironment{isabellebody}{%
    43 \isamarkuptrue\par%
    44 \isa@parindent\parindent\parindent0pt%
    45 \isa@parskip\parskip\parskip0pt%
    46 \isaspacing\isastyle}{\par}
    47 
    48 \newenvironment{isabelle}
    49 {\begin{trivlist}\begin{isabellebody}\item\relax}
    50 {\end{isabellebody}\end{trivlist}}
    51 
    52 \newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}}
    53 
    54 \newcommand{\isaindent}[1]{\hphantom{#1}}
    55 \newcommand{\isanewline}{\mbox{}\par\mbox{}}
    56 \newcommand{\isasep}{}
    57 \newcommand{\isadigit}[1]{#1}
    58 
    59 \newcommand{\isachardefaults}{%
    60 \chardef\isacharbang=`\!%
    61 \chardef\isachardoublequote=`\"%
    62 \chardef\isachardoublequoteopen=`\"%
    63 \chardef\isachardoublequoteclose=`\"%
    64 \chardef\isacharhash=`\#%
    65 \chardef\isachardollar=`\$%
    66 \chardef\isacharpercent=`\%%
    67 \chardef\isacharampersand=`\&%
    68 \chardef\isacharprime=`\'%
    69 \chardef\isacharparenleft=`\(%
    70 \chardef\isacharparenright=`\)%
    71 \chardef\isacharasterisk=`\*%
    72 \chardef\isacharplus=`\+%
    73 \chardef\isacharcomma=`\,%
    74 \chardef\isacharminus=`\-%
    75 \chardef\isachardot=`\.%
    76 \chardef\isacharslash=`\/%
    77 \chardef\isacharcolon=`\:%
    78 \chardef\isacharsemicolon=`\;%
    79 \chardef\isacharless=`\<%
    80 \chardef\isacharequal=`\=%
    81 \chardef\isachargreater=`\>%
    82 \chardef\isacharquery=`\?%
    83 \chardef\isacharat=`\@%
    84 \chardef\isacharbrackleft=`\[%
    85 \chardef\isacharbackslash=`\\%
    86 \chardef\isacharbrackright=`\]%
    87 \chardef\isacharcircum=`\^%
    88 \chardef\isacharunderscore=`\_%
    89 \def\isacharunderscorekeyword{\_}%
    90 \chardef\isacharbackquote=`\`%
    91 \chardef\isacharbackquoteopen=`\`%
    92 \chardef\isacharbackquoteclose=`\`%
    93 \chardef\isacharbraceleft=`\{%
    94 \chardef\isacharbar=`\|%
    95 \chardef\isacharbraceright=`\}%
    96 \chardef\isachartilde=`\~%
    97 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
    98 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
    99 }
   100 
   101 \newcommand{\isaliteral}[2]{#2}
   102 \newcommand{\isanil}{}
   103 
   104 
   105 % keyword and section markup
   106 
   107 \newcommand{\isakeyword}[1]
   108 {\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
   109 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
   110 \newcommand{\isacommand}[1]{\isakeyword{#1}}
   111 
   112 \newcommand{\isamarkupheader}[1]{\section{#1}}
   113 \newcommand{\isamarkupchapter}[1]{\chapter{#1}}
   114 \newcommand{\isamarkupsection}[1]{\section{#1}}
   115 \newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
   116 \newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
   117 \newcommand{\isamarkupsect}[1]{\section{#1}}
   118 \newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
   119 \newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
   120 
   121 \newif\ifisamarkup
   122 \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
   123 \newcommand{\isaendpar}{\par\medskip}
   124 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
   125 \newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
   126 \newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
   127 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
   128 
   129 
   130 % styles
   131 
   132 \def\isabellestyle#1{\csname isabellestyle#1\endcsname}
   133 
   134 \newcommand{\isabellestyledefault}{%
   135 \def\isastyle{\small\tt\slshape}%
   136 \def\isastyleminor{\small\tt\slshape}%
   137 \def\isastylescript{\footnotesize\tt\slshape}%
   138 \isachardefaults%
   139 }
   140 \isabellestyledefault
   141 
   142 \newcommand{\isabellestylett}{%
   143 \def\isastyle{\small\tt}%
   144 \def\isastyleminor{\small\tt}%
   145 \def\isastylescript{\footnotesize\tt}%
   146 \isachardefaults%
   147 }
   148 
   149 \newcommand{\isabellestyleit}{%
   150 \def\isastyle{\small\it}%
   151 \def\isastyleminor{\it}%
   152 \def\isastylescript{\footnotesize\it}%
   153 \isachardefaults%
   154 \def\isacharunderscorekeyword{\mbox{-}}%
   155 \def\isacharbang{\isamath{!}}%
   156 \def\isachardoublequote{\isanil}%
   157 \def\isachardoublequoteopen{\isanil}%
   158 \def\isachardoublequoteclose{\isanil}%
   159 \def\isacharhash{\isamath{\#}}%
   160 \def\isachardollar{\isamath{\$}}%
   161 \def\isacharpercent{\isamath{\%}}%
   162 \def\isacharampersand{\isamath{\&}}%
   163 \def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}%
   164 \def\isacharparenleft{\isamath{(}}%
   165 \def\isacharparenright{\isamath{)}}%
   166 \def\isacharasterisk{\isamath{*}}%
   167 \def\isacharplus{\isamath{+}}%
   168 \def\isacharcomma{\isamath{\mathord,}}%
   169 \def\isacharminus{\isamath{-}}%
   170 \def\isachardot{\isamath{\mathord.}}%
   171 \def\isacharslash{\isamath{/}}%
   172 \def\isacharcolon{\isamath{\mathord:}}%
   173 \def\isacharsemicolon{\isamath{\mathord;}}%
   174 \def\isacharless{\isamath{<}}%
   175 \def\isacharequal{\isamath{=}}%
   176 \def\isachargreater{\isamath{>}}%
   177 \def\isacharat{\isamath{@}}%
   178 \def\isacharbrackleft{\isamath{[}}%
   179 \def\isacharbackslash{\isamath{\backslash}}%
   180 \def\isacharbrackright{\isamath{]}}%
   181 \def\isacharunderscore{\mbox{-}}%
   182 \def\isacharbraceleft{\isamath{\{}}%
   183 \def\isacharbar{\isamath{\mid}}%
   184 \def\isacharbraceright{\isamath{\}}}%
   185 \def\isachartilde{\isamath{{}\sp{\sim}}}%
   186 \def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
   187 \def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
   188 \def\isacharverbatimopen{\isamath{\langle\!\langle}}%
   189 \def\isacharverbatimclose{\isamath{\rangle\!\rangle}}%
   190 }
   191 
   192 \newcommand{\isabellestyleitunderscore}{%
   193 \isabellestyleit%
   194 \def\isacharunderscore{\_}%
   195 \def\isacharunderscorekeyword{\_}%
   196 }
   197 
   198 \newcommand{\isabellestylesl}{%
   199 \isabellestyleit%
   200 \def\isastyle{\small\sl}%
   201 \def\isastyleminor{\sl}%
   202 \def\isastylescript{\footnotesize\sl}%
   203 }
   204 
   205 
   206 % tagged regions
   207 
   208 %plain TeX version of comment package -- much faster!
   209 \let\isafmtname\fmtname\def\fmtname{plain}
   210 \usepackage{comment}
   211 \let\fmtname\isafmtname
   212 
   213 \newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
   214 
   215 \newcommand{\isakeeptag}[1]%
   216 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
   217 \newcommand{\isadroptag}[1]%
   218 {\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
   219 \newcommand{\isafoldtag}[1]%
   220 {\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
   221 
   222 \isakeeptag{theory}
   223 \isakeeptag{proof}
   224 \isakeeptag{ML}
   225 \isakeeptag{visible}
   226 \isadroptag{invisible}
   227 
   228 \IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}