wneuper/isa: src/Tools/isac/Doc/isabelle.sty@168abe8dd1e3

     1 %%

     2 %% macros for Isabelle generated LaTeX output

     3 %%

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

     7 % isabelle environments

     9 \newcommand{\isabellecontext}{UNKNOWN}

    10 \newcommand{\setisabellecontext}[1]{\def\isabellecontext{#1}}

    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}

    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 }

    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}}

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

    44 \newdimen\isa@parindent\newdimen\isa@parskip

    46 \newenvironment{isabellebody}{%

    47 \isamarkuptrue\par%

    48 \isa@parindent\parindent\parindent0pt%

    49 \isa@parskip\parskip\parskip0pt%

    50 \isaspacing\isastyle}{\par}

    52 \newenvironment{isabellebodytt}{%

    53 \isamarkuptrue\par%

    54 \isa@parindent\parindent\parindent0pt%

    55 \isa@parskip\parskip\parskip0pt%

    56 \isaspacing\isastylett}{\par}

    58 \newenvironment{isabelle}

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

    60 {\end{isabellebody}\end{trivlist}}

    62 \newenvironment{isabellett}

    63 {\begin{trivlist}\begin{isabellebodytt}\item\relax}

    64 {\end{isabellebodytt}\end{trivlist}}

    66 \newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}}

    67 \newcommand{\isatt}[1]{\emph{\isaspacing\isastyleminortt #1}}

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

    70 \newcommand{\isanewline}{\mbox{}\par\mbox{}}

    71 \newcommand{\isasep}{}

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

    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 }

   120 % keyword and section markup

   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}}

   127 \newcommand{\isakeywordcontrol}[1]

   128 {\emph{\normalfont\bfseries\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}}

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

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

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

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

   134 \newcommand{\isamarkupparagraph}[1]{\paragraph{#1}}

   135 \newcommand{\isamarkupsubparagraph}[1]{\subparagraph{#1}}

   137 \newif\ifisamarkup

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

   139 \newcommand{\isaendpar}{\par\medskip}

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

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

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

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

   146 % styles

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

   150 \newcommand{\isabellestyledefault}{%

   151 \def\isastyle{\small\normalfont\ttfamily\slshape}%

   152 \def\isastylett{\small\normalfont\ttfamily}%

   153 \def\isastyleminor{\small\normalfont\ttfamily\slshape}%

   154 \def\isastyleminortt{\small\normalfont\ttfamily}%

   155 \def\isastylescript{\footnotesize\normalfont\ttfamily\slshape}%

   156 \isachardefaults%

   157 }

   158 \isabellestyledefault

   160 \newcommand{\isabellestylett}{%

   161 \def\isastyle{\small\normalfont\ttfamily}%

   162 \def\isastylett{\small\normalfont\ttfamily}%

   163 \def\isastyleminor{\small\normalfont\ttfamily}%

   164 \def\isastyleminortt{\small\normalfont\ttfamily}%

   165 \def\isastylescript{\footnotesize\normalfont\ttfamily}%

   166 \isachardefaults%

   167 }

   169 \newcommand{\isabellestyleit}{%

   170 \def\isastyle{\small\normalfont\itshape}%

   171 \def\isastylett{\small\normalfont\ttfamily}%

   172 \def\isastyleminor{\normalfont\itshape}%

   173 \def\isastyleminortt{\normalfont\ttfamily}%

   174 \def\isastylescript{\footnotesize\normalfont\itshape}%

   175 \isachardefaults%

   176 \def\isacharunderscorekeyword{\mbox{-}}%

   177 \def\isacharbang{\isamath{!}}%

   178 \def\isachardoublequote{}%

   179 \def\isachardoublequoteopen{}%

   180 \def\isachardoublequoteclose{}%

   181 \def\isacharhash{\isamath{\#}}%

   182 \def\isachardollar{\isamath{\$}}%

   183 \def\isacharpercent{\isamath{\%}}%

   184 \def\isacharampersand{\isamath{\&}}%

   185 \def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}%

   186 \def\isacharparenleft{\isamath{(}}%

   187 \def\isacharparenright{\isamath{)}}%

   188 \def\isacharasterisk{\isamath{*}}%

   189 \def\isacharplus{\isamath{+}}%

   190 \def\isacharcomma{\isamath{\mathord,}}%

   191 \def\isacharminus{\isamath{-}}%

   192 \def\isachardot{\isamath{\mathord.}}%

   193 \def\isacharslash{\isamath{/}}%

   194 \def\isacharcolon{\isamath{\mathord:}}%

   195 \def\isacharsemicolon{\isamath{\mathord;}}%

   196 \def\isacharless{\isamath{<}}%

   197 \def\isacharequal{\isamath{=}}%

   198 \def\isachargreater{\isamath{>}}%

   199 \def\isacharat{\isamath{@}}%

   200 \def\isacharbrackleft{\isamath{[}}%

   201 \def\isacharbackslash{\isamath{\backslash}}%

   202 \def\isacharbrackright{\isamath{]}}%

   203 \def\isacharunderscore{\mbox{-}}%

   204 \def\isacharbraceleft{\isamath{\{}}%

   205 \def\isacharbar{\isamath{\mid}}%

   206 \def\isacharbraceright{\isamath{\}}}%

   207 \def\isachartilde{\isamath{{}\sp{\sim}}}%

   208 \def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%

   209 \def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%

   210 \def\isacharverbatimopen{\isamath{\langle\!\langle}}%

   211 \def\isacharverbatimclose{\isamath{\rangle\!\rangle}}%

   212 }

   214 \newcommand{\isabellestyleliteral}{%

   215 \isabellestyleit%

   216 \def\isacharunderscore{\_}%

   217 \def\isacharunderscorekeyword{\_}%

   218 \chardef\isacharbackquoteopen=`\`%

   219 \chardef\isacharbackquoteclose=`\`%

   220 }

   222 \newcommand{\isabellestyleliteralunderscore}{%

   223 \isabellestyleliteral%

   224 \def\isacharunderscore{\textunderscore}%

   225 \def\isacharunderscorekeyword{\textunderscore}%

   226 }

   228 \newcommand{\isabellestylesl}{%

   229 \isabellestyleit%

   230 \def\isastyle{\small\normalfont\slshape}%

   231 \def\isastylett{\small\normalfont\ttfamily}%

   232 \def\isastyleminor{\normalfont\slshape}%

   233 \def\isastyleminortt{\normalfont\ttfamily}%

   234 \def\isastylescript{\footnotesize\normalfont\slshape}%

   235 }

   238 % cancel text

   240 \usepackage[normalem]{ulem}

   241 \newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}}

   244 % tagged regions

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

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

   248 \usepackage{comment}

   249 \let\fmtname\isafmtname

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

   253 \newcommand{\isakeeptag}[1]%

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

   255 \newcommand{\isadroptag}[1]%

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

   257 \newcommand{\isafoldtag}[1]%

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

   260 \isakeeptag{document}

   261 \isakeeptag{theory}

   262 \isakeeptag{proof}

   263 \isakeeptag{ML}

   264 \isakeeptag{visible}

   265 \isadroptag{invisible}

   266 \isakeeptag{important}

   267 \isakeeptag{unimportant}

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

author	Walther Neuper <walther.neuper@jku.at>
	Wed, 11 Mar 2020 15:25:52 +0100
changeset 59827	168abe8dd1e3
permissions	-rw-r--r--