--- a/ProgTutorial/output_tutorial.ML Tue Jun 28 08:44:34 2011 +0100
+++ b/ProgTutorial/output_tutorial.ML Tue Jun 28 09:22:00 2011 +0100
@@ -84,9 +84,13 @@
| boolean "false" = false
| boolean s = error ("Bad boolean value: " ^ quote s);
-val _ = Thy_Output.add_option @{binding "gray"}
+val gray_setup = Thy_Output.add_option @{binding "gray"}
(Thy_Output.add_wrapper o Library.setmp_CRITICAL gray o boolean)
-val _ = Thy_Output.add_option @{binding "linenos"}
+val linenos_setup = Thy_Output.add_option @{binding "linenos"}
(Thy_Output.add_wrapper o Library.setmp_CRITICAL linenos o boolean)
+val setup =
+ gray_setup #>
+ linenos_setup
+
end
\ No newline at end of file