equal
deleted
inserted
replaced
95 \chardef\isacharbar=`\|% |
95 \chardef\isacharbar=`\|% |
96 \chardef\isacharbraceright=`\}% |
96 \chardef\isacharbraceright=`\}% |
97 \chardef\isachartilde=`\~% |
97 \chardef\isachartilde=`\~% |
98 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}% |
98 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}% |
99 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}% |
99 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}% |
|
100 \def\isacartoucheopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}% |
|
101 \def\isacartoucheclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}% |
100 } |
102 } |
101 |
103 |
102 |
104 |
103 % keyword and section markup |
105 % keyword and section markup |
104 |
106 |
193 \def\isacharunderscorekeyword{\_}% |
195 \def\isacharunderscorekeyword{\_}% |
194 \chardef\isacharbackquoteopen=`\`% |
196 \chardef\isacharbackquoteopen=`\`% |
195 \chardef\isacharbackquoteclose=`\`% |
197 \chardef\isacharbackquoteclose=`\`% |
196 } |
198 } |
197 |
199 |
|
200 \newcommand{\isabellestyleliteralunderscore}{% |
|
201 \isabellestyleliteral% |
|
202 \def\isacharunderscore{\textunderscore}% |
|
203 \def\isacharunderscorekeyword{\textunderscore}% |
|
204 } |
|
205 |
198 \newcommand{\isabellestylesl}{% |
206 \newcommand{\isabellestylesl}{% |
199 \isabellestyleit% |
207 \isabellestyleit% |
200 \def\isastyle{\small\sl}% |
208 \def\isastyle{\small\sl}% |
201 \def\isastyleminor{\sl}% |
209 \def\isastyleminor{\sl}% |
202 \def\isastylescript{\footnotesize\sl}% |
210 \def\isastylescript{\footnotesize\sl}% |