equal
deleted
inserted
replaced
96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
96 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
97 % this hack is for getting rid of the ML {* ... *} |
97 % this hack is for getting rid of the ML {* ... *} |
98 % scaffolding around function definitions |
98 % scaffolding around function definitions |
99 \newenvironment{vanishML}{% |
99 \newenvironment{vanishML}{% |
100 \renewcommand{\isacommand}[1]{}% |
100 \renewcommand{\isacommand}[1]{}% |
101 \renewcommand{\isacharverbatimopen}{}% |
101 \renewcommand{\isacartoucheopen}{}% |
102 \renewcommand{\isacharverbatimclose}{}}{} |
102 \renewcommand{\isacartoucheclose}{}}{} |
103 |
103 |
104 \isakeeptag{grayML} |
104 \isakeeptag{grayML} |
105 \renewcommand{\isataggrayML}{\begin{vanishML}\begin{graybox}} |
105 \renewcommand{\isataggrayML}{\begin{vanishML}\begin{graybox}} |
106 \renewcommand{\endisataggrayML}{\end{graybox}\end{vanishML}} |
106 \renewcommand{\endisataggrayML}{\end{graybox}\end{vanishML}} |
107 |
107 |