doc-src/Locales/Locales/document/isabelle.sty
changeset 18962 d6ecc5828b14
parent 17536 1b7c2f7df2e6
child 22649 6cf96b9f7b9e
equal deleted inserted replaced
18961:9000bb9e6718 18962:d6ecc5828b14
     8 
     8 
     9 % isabelle environments
     9 % isabelle environments
    10 
    10 
    11 \newcommand{\isabellecontext}{UNKNOWN}
    11 \newcommand{\isabellecontext}{UNKNOWN}
    12 
    12 
    13 \newcommand{\isastyle}{\small\tt\slshape}
    13 \newcommand{\isastyle}{\UNDEF}
    14 \newcommand{\isastyleminor}{\small\tt\slshape}
    14 \newcommand{\isastyleminor}{\UNDEF}
    15 \newcommand{\isastylescript}{\footnotesize\tt\slshape}
    15 \newcommand{\isastylescript}{\UNDEF}
    16 \newcommand{\isastyletext}{\normalsize\rm}
    16 \newcommand{\isastyletext}{\normalsize\rm}
    17 \newcommand{\isastyletxt}{\rm}
    17 \newcommand{\isastyletxt}{\rm}
    18 \newcommand{\isastylecmt}{\rm}
    18 \newcommand{\isastylecmt}{\rm}
    19 
    19 
    20 %symbol markup -- \emph achieves decent spacing via italic corrections
    20 %symbol markup -- \emph achieves decent spacing via italic corrections
    50 \newcommand{\isaindent}[1]{\hphantom{#1}}
    50 \newcommand{\isaindent}[1]{\hphantom{#1}}
    51 \newcommand{\isanewline}{\mbox{}\par\mbox{}}
    51 \newcommand{\isanewline}{\mbox{}\par\mbox{}}
    52 \newcommand{\isasep}{}
    52 \newcommand{\isasep}{}
    53 \newcommand{\isadigit}[1]{#1}
    53 \newcommand{\isadigit}[1]{#1}
    54 
    54 
    55 \chardef\isacharbang=`\!
    55 \newcommand{\isachardefaults}{%
    56 \chardef\isachardoublequote=`\"
    56 \chardef\isacharbang=`\!%
    57 \chardef\isachardoublequoteopen=`\"
    57 \chardef\isachardoublequote=`\"%
    58 \chardef\isachardoublequoteclose=`\"
    58 \chardef\isachardoublequoteopen=`\"%
    59 \chardef\isacharhash=`\#
    59 \chardef\isachardoublequoteclose=`\"%
    60 \chardef\isachardollar=`\$
    60 \chardef\isacharhash=`\#%
    61 \chardef\isacharpercent=`\%
    61 \chardef\isachardollar=`\$%
    62 \chardef\isacharampersand=`\&
    62 \chardef\isacharpercent=`\%%
    63 \chardef\isacharprime=`\'
    63 \chardef\isacharampersand=`\&%
    64 \chardef\isacharparenleft=`\(
    64 \chardef\isacharprime=`\'%
    65 \chardef\isacharparenright=`\)
    65 \chardef\isacharparenleft=`\(%
    66 \chardef\isacharasterisk=`\*
    66 \chardef\isacharparenright=`\)%
    67 \chardef\isacharplus=`\+
    67 \chardef\isacharasterisk=`\*%
    68 \chardef\isacharcomma=`\,
    68 \chardef\isacharplus=`\+%
    69 \chardef\isacharminus=`\-
    69 \chardef\isacharcomma=`\,%
    70 \chardef\isachardot=`\.
    70 \chardef\isacharminus=`\-%
    71 \chardef\isacharslash=`\/
    71 \chardef\isachardot=`\.%
    72 \chardef\isacharcolon=`\:
    72 \chardef\isacharslash=`\/%
    73 \chardef\isacharsemicolon=`\;
    73 \chardef\isacharcolon=`\:%
    74 \chardef\isacharless=`\<
    74 \chardef\isacharsemicolon=`\;%
    75 \chardef\isacharequal=`\=
    75 \chardef\isacharless=`\<%
    76 \chardef\isachargreater=`\>
    76 \chardef\isacharequal=`\=%
    77 \chardef\isacharquery=`\?
    77 \chardef\isachargreater=`\>%
    78 \chardef\isacharat=`\@
    78 \chardef\isacharquery=`\?%
    79 \chardef\isacharbrackleft=`\[
    79 \chardef\isacharat=`\@%
    80 \chardef\isacharbackslash=`\\
    80 \chardef\isacharbrackleft=`\[%
    81 \chardef\isacharbrackright=`\]
    81 \chardef\isacharbackslash=`\\%
    82 \chardef\isacharcircum=`\^
    82 \chardef\isacharbrackright=`\]%
    83 \chardef\isacharunderscore=`\_
    83 \chardef\isacharcircum=`\^%
    84 \chardef\isacharbackquote=`\`
    84 \chardef\isacharunderscore=`\_%
    85 \chardef\isacharbackquoteopen=`\`
    85 \def\isacharunderscorekeyword{\_}%
    86 \chardef\isacharbackquoteclose=`\`
    86 \chardef\isacharbackquote=`\`%
    87 \chardef\isacharbraceleft=`\{
    87 \chardef\isacharbackquoteopen=`\`%
    88 \chardef\isacharbar=`\|
    88 \chardef\isacharbackquoteclose=`\`%
    89 \chardef\isacharbraceright=`\}
    89 \chardef\isacharbraceleft=`\{%
    90 \chardef\isachartilde=`\~
    90 \chardef\isacharbar=`\|%
    91 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}
    91 \chardef\isacharbraceright=`\}%
    92 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}
    92 \chardef\isachartilde=`\~%
       
    93 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
       
    94 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
       
    95 }
    93 
    96 
    94 
    97 
    95 % keyword and section markup
    98 % keyword and section markup
    96 
    99 
    97 \newcommand{\isakeywordcharunderscore}{\_}
       
    98 \newcommand{\isakeyword}[1]
   100 \newcommand{\isakeyword}[1]
    99 {\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
   101 {\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
   100 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
   102 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
   101 \newcommand{\isacommand}[1]{\isakeyword{#1}}
   103 \newcommand{\isacommand}[1]{\isakeyword{#1}}
   102 
   104 
   103 \newcommand{\isamarkupheader}[1]{\section{#1}}
   105 \newcommand{\isamarkupheader}[1]{\section{#1}}
   104 \newcommand{\isamarkupchapter}[1]{\chapter{#1}}
   106 \newcommand{\isamarkupchapter}[1]{\chapter{#1}}
   116 \newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
   118 \newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
   117 \newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
   119 \newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
   118 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
   120 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
   119 
   121 
   120 
   122 
   121 % alternative styles
   123 % styles
   122 
   124 
   123 \newcommand{\isabellestyle}{}
       
   124 \def\isabellestyle#1{\csname isabellestyle#1\endcsname}
   125 \def\isabellestyle#1{\csname isabellestyle#1\endcsname}
       
   126 
       
   127 \newcommand{\isabellestyledefault}{%
       
   128 \renewcommand{\isastyle}{\small\tt\slshape}%
       
   129 \renewcommand{\isastyleminor}{\small\tt\slshape}%
       
   130 \renewcommand{\isastylescript}{\footnotesize\tt\slshape}%
       
   131 \isachardefaults%
       
   132 }
       
   133 \isabellestyledefault
   125 
   134 
   126 \newcommand{\isabellestylett}{%
   135 \newcommand{\isabellestylett}{%
   127 \renewcommand{\isastyle}{\small\tt}%
   136 \renewcommand{\isastyle}{\small\tt}%
   128 \renewcommand{\isastyleminor}{\small\tt}%
   137 \renewcommand{\isastyleminor}{\small\tt}%
   129 \renewcommand{\isastylescript}{\footnotesize\tt}%
   138 \renewcommand{\isastylescript}{\footnotesize\tt}%
   130 }
   139 \isachardefaults%
       
   140 }
       
   141 
   131 \newcommand{\isabellestyleit}{%
   142 \newcommand{\isabellestyleit}{%
   132 \renewcommand{\isastyle}{\small\it}%
   143 \renewcommand{\isastyle}{\small\it}%
   133 \renewcommand{\isastyleminor}{\it}%
   144 \renewcommand{\isastyleminor}{\it}%
   134 \renewcommand{\isastylescript}{\footnotesize\it}%
   145 \renewcommand{\isastylescript}{\footnotesize\it}%
   135 \renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
   146 \renewcommand{\isacharunderscorekeyword}{\mbox{-}}%
   136 \renewcommand{\isacharbang}{\isamath{!}}%
   147 \renewcommand{\isacharbang}{\isamath{!}}%
   137 \renewcommand{\isachardoublequote}{}%
   148 \renewcommand{\isachardoublequote}{}%
   138 \renewcommand{\isachardoublequoteopen}{}%
   149 \renewcommand{\isachardoublequoteopen}{}%
   139 \renewcommand{\isachardoublequoteclose}{}%
   150 \renewcommand{\isachardoublequoteclose}{}%
   140 \renewcommand{\isacharhash}{\isamath{\#}}%
   151 \renewcommand{\isacharhash}{\isamath{\#}}%