# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1234571045 0
# Node ID 796c6ea633b33e76580775a85a5c74ab9d369dcd
# Parent  c9ff326e3ce5698c1b13d9e30f7ce60d9f35b0e8
added an option for linenumbers to the chunk-antiquotation

diff -r c9ff326e3ce5 -r 796c6ea633b3 CookBook/Package/Ind_Interface.thy
--- a/CookBook/Package/Ind_Interface.thy	Sat Feb 14 00:11:50 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Sat Feb 14 00:24:05 2009 +0000
@@ -110,7 +110,7 @@
   railroad diagram in Figure~\ref{fig:railroad}. This diagram more or less
   translates directly into the parser
 
-   @{ML_chunk [display,gray] parser}
+   @{ML_chunk [display,gray,linenos] parser}
 
   which we also described in Section~\ref{sec:parsingspecs}
 
diff -r c9ff326e3ce5 -r 796c6ea633b3 CookBook/chunks.ML
--- a/CookBook/chunks.ML	Sat Feb 14 00:11:50 2009 +0000
+++ b/CookBook/chunks.ML	Sat Feb 14 00:24:05 2009 +0000
@@ -3,9 +3,10 @@
 struct
 
 (* rebuilding the output_list function from ThyOutput in order to *)
-(* enable the option [gray] *)
+(* enable the options [gray, linenos] *)
 
 val gray = ref false;
+val linenos = ref false
 
 fun boolean "" = true
   | boolean "true" = true
@@ -20,6 +21,7 @@
     map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent))
     #> space_implode "\\isasep\\isanewline%\n"
     #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) 
+    #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) 
     #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
  else
     map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
@@ -29,7 +31,8 @@
 fun output pretty src ctxt = output_list pretty src ctxt o single
 
 val _ = ThyOutput.add_options
- [("gray", Library.setmp gray o boolean)]
+ [("gray", Library.setmp gray o boolean),
+  ("linenos", Library.setmp linenos o boolean)]
 
 
 
diff -r c9ff326e3ce5 -r 796c6ea633b3 CookBook/document/root.tex
--- a/CookBook/document/root.tex	Sat Feb 14 00:11:50 2009 +0000
+++ b/CookBook/document/root.tex	Sat Feb 14 00:24:05 2009 +0000
@@ -84,14 +84,16 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % for code that has line numbers
+\newenvironment{linenos}{\resetlinenumber\internallinenumbers}{\nolinenumbers}
+
 \isakeeptag{linenos}
-\renewcommand{\isataglinenos}{\begingroup\resetlinenumber\internallinenumbers}
-\renewcommand{\endisataglinenos}{\par\nolinenumbers\endgroup}
+\renewcommand{\isataglinenos}{\begin{linenos}}
+\renewcommand{\endisataglinenos}{\par\end{linenos}}
 
 % should only be used in ML code
 \isakeeptag{linenosgray}
-\renewcommand{\isataglinenosgray}{\begin{vanishML}\begin{graybox}\resetlinenumber\internallinenumbers}
-\renewcommand{\endisataglinenosgray}{\par\nolinenumbers\end{graybox}\end{vanishML}}
+\renewcommand{\isataglinenosgray}{\begin{vanishML}\begin{graybox}\begin{linenos}}
+\renewcommand{\endisataglinenosgray}{\par\end{linenos}\end{graybox}\end{vanishML}}
 
 \isakeeptag{small}
 \renewcommand{\isatagsmall}{\begingroup\small}
diff -r c9ff326e3ce5 -r 796c6ea633b3 cookbook.pdf
Binary file cookbook.pdf has changed