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 @{binding "gray"} |
87 val gray_setup = 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 @{binding "linenos"} |
89 val linenos_setup = 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 val setup = |
|
93 gray_setup #> |
|
94 linenos_setup |
|
95 |
92 end |
96 end |