lib/texinputs/isabelle.sty
author wenzelm
Wed Nov 07 21:42:16 2018 +0100 (9 months ago)
changeset 69255 800b1ce96fce
parent 67571 f858fe5531ac
child 70142 7efe226c50e4
permissions -rw-r--r--
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
     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 \newcommand{\setisabellecontext}[1]{\def\isabellecontext{#1}}
    11 
    12 \newcommand{\isastyle}{\UNDEF}
    13 \newcommand{\isastylett}{\UNDEF}
    14 \newcommand{\isastyleminor}{\UNDEF}
    15 \newcommand{\isastyleminortt}{\UNDEF}
    16 \newcommand{\isastylescript}{\UNDEF}
    17 \newcommand{\isastyletext}{\normalsize\normalfont\rmfamily}
    18 \newcommand{\isastyletxt}{\normalfont\rmfamily}
    19 \newcommand{\isastylecmt}{\normalfont\rmfamily}
    20 
    21 \newcommand{\isaspacing}{%
    22   \sfcode 42 1000 % .
    23   \sfcode 63 1000 % ?
    24   \sfcode 33 1000 % !
    25   \sfcode 58 1000 % :
    26   \sfcode 59 1000 % ;
    27   \sfcode 44 1000 % ,
    28 }
    29 
    30 %symbol markup -- \emph achieves decent spacing via italic corrections
    31 \newcommand{\isamath}[1]{\emph{$#1$}}
    32 \newcommand{\isatext}[1]{\emph{#1}}
    33 \DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}}
    34 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    35 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    36 \DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript}
    37 \DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
    38 \DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
    39 \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
    40 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
    41 
    42 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
    43 
    44 \newdimen\isa@parindent\newdimen\isa@parskip
    45 
    46 \newenvironment{isabellebody}{%
    47 \isamarkuptrue\par%
    48 \isa@parindent\parindent\parindent0pt%
    49 \isa@parskip\parskip\parskip0pt%
    50 \isaspacing\isastyle}{\par}
    51 
    52 \newenvironment{isabellebodytt}{%
    53 \isamarkuptrue\par%
    54 \isa@parindent\parindent\parindent0pt%
    55 \isa@parskip\parskip\parskip0pt%
    56 \isaspacing\isastylett}{\par}
    57 
    58 \newenvironment{isabelle}
    59 {\begin{trivlist}\begin{isabellebody}\item\relax}
    60 {\end{isabellebody}\end{trivlist}}
    61 
    62 \newenvironment{isabellett}
    63 {\begin{trivlist}\begin{isabellebodytt}\item\relax}
    64 {\end{isabellebodytt}\end{trivlist}}
    65 
    66 \newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}}
    67 \newcommand{\isatt}[1]{\emph{\isaspacing\isastyleminortt #1}}
    68 
    69 \newcommand{\isaindent}[1]{\hphantom{#1}}
    70 \newcommand{\isanewline}{\mbox{}\par\mbox{}}
    71 \newcommand{\isasep}{}
    72 \newcommand{\isadigit}[1]{#1}
    73 
    74 \newcommand{\isachardefaults}{%
    75 \def\isacharbell{\isamath{\bigbox}}%requires stmaryrd
    76 \chardef\isacharbang=`\!%
    77 \chardef\isachardoublequote=`\"%
    78 \chardef\isachardoublequoteopen=`\"%
    79 \chardef\isachardoublequoteclose=`\"%
    80 \chardef\isacharhash=`\#%
    81 \chardef\isachardollar=`\$%
    82 \chardef\isacharpercent=`\%%
    83 \chardef\isacharampersand=`\&%
    84 \chardef\isacharprime=`\'%
    85 \chardef\isacharparenleft=`\(%
    86 \chardef\isacharparenright=`\)%
    87 \chardef\isacharasterisk=`\*%
    88 \chardef\isacharplus=`\+%
    89 \chardef\isacharcomma=`\,%
    90 \chardef\isacharminus=`\-%
    91 \chardef\isachardot=`\.%
    92 \chardef\isacharslash=`\/%
    93 \chardef\isacharcolon=`\:%
    94 \chardef\isacharsemicolon=`\;%
    95 \chardef\isacharless=`\<%
    96 \chardef\isacharequal=`\=%
    97 \chardef\isachargreater=`\>%
    98 \chardef\isacharquery=`\?%
    99 \chardef\isacharat=`\@%
   100 \chardef\isacharbrackleft=`\[%
   101 \chardef\isacharbackslash=`\\%
   102 \chardef\isacharbrackright=`\]%
   103 \chardef\isacharcircum=`\^%
   104 \chardef\isacharunderscore=`\_%
   105 \def\isacharunderscorekeyword{\_}%
   106 \chardef\isacharbackquote=`\`%
   107 \chardef\isacharbackquoteopen=`\`%
   108 \chardef\isacharbackquoteclose=`\`%
   109 \chardef\isacharbraceleft=`\{%
   110 \chardef\isacharbar=`\|%
   111 \chardef\isacharbraceright=`\}%
   112 \chardef\isachartilde=`\~%
   113 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
   114 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
   115 \def\isacartoucheopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
   116 \def\isacartoucheclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
   117 }
   118 
   119 
   120 % keyword and section markup
   121 
   122 \newcommand{\isakeyword}[1]
   123 {\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
   124 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
   125 \newcommand{\isacommand}[1]{\isakeyword{#1}}
   126 
   127 \newcommand{\isakeywordcontrol}[1]
   128 {\emph{\normalfont\bfseries\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}}
   129 
   130 \newcommand{\isamarkupheader}[1]{\section{#1}}
   131 \newcommand{\isamarkupchapter}[1]{\chapter{#1}}
   132 \newcommand{\isamarkupsection}[1]{\section{#1}}
   133 \newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
   134 \newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
   135 \newcommand{\isamarkupparagraph}[1]{\paragraph{#1}}
   136 \newcommand{\isamarkupsubparagraph}[1]{\subparagraph{#1}}
   137 
   138 \newif\ifisamarkup
   139 \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
   140 \newcommand{\isaendpar}{\par\medskip}
   141 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
   142 \newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
   143 \newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
   144 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
   145 
   146 
   147 % styles
   148 
   149 \def\isabellestyle#1{\csname isabellestyle#1\endcsname}
   150 
   151 \newcommand{\isabellestyledefault}{%
   152 \def\isastyle{\small\normalfont\ttfamily\slshape}%
   153 \def\isastylett{\small\normalfont\ttfamily}%
   154 \def\isastyleminor{\small\normalfont\ttfamily\slshape}%
   155 \def\isastyleminortt{\small\normalfont\ttfamily}%
   156 \def\isastylescript{\footnotesize\normalfont\ttfamily\slshape}%
   157 \isachardefaults%
   158 }
   159 \isabellestyledefault
   160 
   161 \newcommand{\isabellestylett}{%
   162 \def\isastyle{\small\normalfont\ttfamily}%
   163 \def\isastylett{\small\normalfont\ttfamily}%
   164 \def\isastyleminor{\small\normalfont\ttfamily}%
   165 \def\isastyleminortt{\small\normalfont\ttfamily}%
   166 \def\isastylescript{\footnotesize\normalfont\ttfamily}%
   167 \isachardefaults%
   168 }
   169 
   170 \newcommand{\isabellestyleit}{%
   171 \def\isastyle{\small\normalfont\itshape}%
   172 \def\isastylett{\small\normalfont\ttfamily}%
   173 \def\isastyleminor{\normalfont\itshape}%
   174 \def\isastyleminortt{\normalfont\ttfamily}%
   175 \def\isastylescript{\footnotesize\normalfont\itshape}%
   176 \isachardefaults%
   177 \def\isacharunderscorekeyword{\mbox{-}}%
   178 \def\isacharbang{\isamath{!}}%
   179 \def\isachardoublequote{}%
   180 \def\isachardoublequoteopen{}%
   181 \def\isachardoublequoteclose{}%
   182 \def\isacharhash{\isamath{\#}}%
   183 \def\isachardollar{\isamath{\$}}%
   184 \def\isacharpercent{\isamath{\%}}%
   185 \def\isacharampersand{\isamath{\&}}%
   186 \def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}%
   187 \def\isacharparenleft{\isamath{(}}%
   188 \def\isacharparenright{\isamath{)}}%
   189 \def\isacharasterisk{\isamath{*}}%
   190 \def\isacharplus{\isamath{+}}%
   191 \def\isacharcomma{\isamath{\mathord,}}%
   192 \def\isacharminus{\isamath{-}}%
   193 \def\isachardot{\isamath{\mathord.}}%
   194 \def\isacharslash{\isamath{/}}%
   195 \def\isacharcolon{\isamath{\mathord:}}%
   196 \def\isacharsemicolon{\isamath{\mathord;}}%
   197 \def\isacharless{\isamath{<}}%
   198 \def\isacharequal{\isamath{=}}%
   199 \def\isachargreater{\isamath{>}}%
   200 \def\isacharat{\isamath{@}}%
   201 \def\isacharbrackleft{\isamath{[}}%
   202 \def\isacharbackslash{\isamath{\backslash}}%
   203 \def\isacharbrackright{\isamath{]}}%
   204 \def\isacharunderscore{\mbox{-}}%
   205 \def\isacharbraceleft{\isamath{\{}}%
   206 \def\isacharbar{\isamath{\mid}}%
   207 \def\isacharbraceright{\isamath{\}}}%
   208 \def\isachartilde{\isamath{{}\sp{\sim}}}%
   209 \def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
   210 \def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
   211 \def\isacharverbatimopen{\isamath{\langle\!\langle}}%
   212 \def\isacharverbatimclose{\isamath{\rangle\!\rangle}}%
   213 }
   214 
   215 \newcommand{\isabellestyleliteral}{%
   216 \isabellestyleit%
   217 \def\isacharunderscore{\_}%
   218 \def\isacharunderscorekeyword{\_}%
   219 \chardef\isacharbackquoteopen=`\`%
   220 \chardef\isacharbackquoteclose=`\`%
   221 }
   222 
   223 \newcommand{\isabellestyleliteralunderscore}{%
   224 \isabellestyleliteral%
   225 \def\isacharunderscore{\textunderscore}%
   226 \def\isacharunderscorekeyword{\textunderscore}%
   227 }
   228 
   229 \newcommand{\isabellestylesl}{%
   230 \isabellestyleit%
   231 \def\isastyle{\small\normalfont\slshape}%
   232 \def\isastylett{\small\normalfont\ttfamily}%
   233 \def\isastyleminor{\normalfont\slshape}%
   234 \def\isastyleminortt{\normalfont\ttfamily}%
   235 \def\isastylescript{\footnotesize\normalfont\slshape}%
   236 }
   237 
   238 
   239 % cancel text
   240 
   241 \usepackage[normalem]{ulem}
   242 \newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}}
   243 
   244 
   245 % tagged regions
   246 
   247 %plain TeX version of comment package -- much faster!
   248 \let\isafmtname\fmtname\def\fmtname{plain}
   249 \usepackage{comment}
   250 \let\fmtname\isafmtname
   251 
   252 \newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
   253 
   254 \newcommand{\isakeeptag}[1]%
   255 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
   256 \newcommand{\isadroptag}[1]%
   257 {\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
   258 \newcommand{\isafoldtag}[1]%
   259 {\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
   260 
   261 \isakeeptag{document}
   262 \isakeeptag{theory}
   263 \isakeeptag{proof}
   264 \isakeeptag{ML}
   265 \isakeeptag{visible}
   266 \isadroptag{invisible}
   267 \isakeeptag{important}
   268 \isakeeptag{unimportant}
   269 
   270 \IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}