82 \renewcommand{\isatagTutorialML}{\begin{vanishML}\begin{graybox}} |
82 \renewcommand{\isatagTutorialML}{\begin{vanishML}\begin{graybox}} |
83 \renewcommand{\endisatagTutorialML}{\end{graybox}\end{vanishML}} |
83 \renewcommand{\endisatagTutorialML}{\end{graybox}\end{vanishML}} |
84 |
84 |
85 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
85 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
86 % for code that has line numbers |
86 % for code that has line numbers |
87 \isakeeptag{linenumbers} |
87 \isakeeptag{linenos} |
88 \renewcommand{\isataglinenumbers}{\begin{vanishML}\begin{graybox}\resetlinenumber\internallinenumbers} |
88 \renewcommand{\isataglinenos}{\begingroup\resetlinenumber\internallinenumbers} |
89 \renewcommand{\endisataglinenumbers}{\par\end{graybox}\end{vanishML}} |
89 \renewcommand{\endisataglinenos}{\par\nolinenumbers\endgroup} |
|
90 |
|
91 % should only be used in ML code |
|
92 \isakeeptag{linenosgray} |
|
93 \renewcommand{\isataglinenosgray}{\begin{vanishML}\begin{graybox}\resetlinenumber\internallinenumbers} |
|
94 \renewcommand{\endisataglinenosgray}{\par\nolinenumbers\end{graybox}\end{vanishML}} |
90 |
95 |
91 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
92 \renewenvironment{isabelle} |
97 \renewenvironment{isabelle} |
93 {\begin{trivlist}\begin{isabellebody}\small\item\relax} |
98 {\begin{trivlist}\begin{isabellebody}\small\item\relax} |
94 {\end{isabellebody}\end{trivlist}} |
99 {\end{isabellebody}\end{trivlist}} |