equal
deleted
inserted
replaced
77 | boolean "true" = true |
77 | boolean "true" = true |
78 | boolean "false" = false |
78 | boolean "false" = false |
79 | boolean s = error ("Bad boolean value: " ^ quote s); |
79 | boolean s = error ("Bad boolean value: " ^ quote s); |
80 |
80 |
81 val _ = ThyOutput.add_options |
81 val _ = ThyOutput.add_options |
82 [("gray", Library.setmp gray o boolean), |
82 [("gray", Library.setmp_CRITICAL gray o boolean), |
83 ("linenos", Library.setmp linenos o boolean)] |
83 ("linenos", Library.setmp_CRITICAL linenos o boolean)] |
84 |
84 |
85 end |
85 end |