equal
deleted
inserted
replaced
82 fun boolean "" = true |
82 fun boolean "" = true |
83 | boolean "true" = true |
83 | boolean "true" = true |
84 | boolean "false" = false |
84 | boolean "false" = false |
85 | boolean s = error ("Bad boolean value: " ^ quote s); |
85 | boolean s = error ("Bad boolean value: " ^ quote s); |
86 |
86 |
87 val _ = Thy_Output.add_option "gray" |
87 val _ = Thy_Output.add_option @{binding "gray"} |
88 (Thy_Output.add_wrapper o Library.setmp_CRITICAL gray o boolean) |
88 (Thy_Output.add_wrapper o Library.setmp_CRITICAL gray o boolean) |
89 val _ = Thy_Output.add_option "linenos" |
89 val _ = Thy_Output.add_option @{binding "linenos"} |
90 (Thy_Output.add_wrapper o Library.setmp_CRITICAL linenos o boolean) |
90 (Thy_Output.add_wrapper o Library.setmp_CRITICAL linenos o boolean) |
91 |
91 |
92 end |
92 end |