diff -r 141751cab5b2 -r dfbd535cd1fd ProgTutorial/document/root.tex
--- a/ProgTutorial/document/root.tex	Wed Oct 26 13:19:09 2011 +0100
+++ b/ProgTutorial/document/root.tex	Thu Oct 27 18:11:52 2011 +0100
@@ -109,11 +109,15 @@
 \renewcommand{\isataglinenos}{\begin{linenos}}
 \renewcommand{\endisataglinenos}{\end{linenos}}
 
-% should only be used in ML code
+% should be used in ML code
 \isakeeptag{linenosgray}
 \renewcommand{\isataglinenosgray}{\begin{vanishML}\begin{graybox}\begin{linenos}}
 \renewcommand{\endisataglinenosgray}{\end{linenos}\end{graybox}\end{vanishML}}
 
+\isakeeptag{graylinenos}
+\renewcommand{\isataggraylinenos}{\begin{graybox}\begin{linenos}}
+\renewcommand{\endisataggraylinenos}{\end{linenos}\end{graybox}}
+
 \isakeeptag{gray}
 \renewcommand{\isataggray}{\begin{graybox}}
 \renewcommand{\endisataggray}{\end{graybox}}