95   | boolean s = error ("Bad boolean value: " ^ quote s);

    95   | boolean s = error ("Bad boolean value: " ^ quote s);

    96 

    96 

    97 fun explicit "" = Default

    97 fun explicit "" = Default

    98   | explicit s  = Explicit s

    98   | explicit s  = Explicit s

    99 

    99 

   100 val _ = ThyOutput.add_options

   101 val _ = ThyOutput.add_options

   101  [("gray", Library.setmp gray o boolean),

   102  [("gray", Library.setmp gray o boolean),

   102   ("linenos", Library.setmp linenos o boolean),

   103   ("linenos", Library.setmp linenos o boolean),

   103   ("index", Library.setmp index o explicit)]

   104   ("index", Library.setmp index o explicit)]

   104 

   105