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)]