equal
deleted
inserted
replaced
133 not require additional LaTeX packages (depending on comments in |
133 not require additional LaTeX packages (depending on comments in |
134 isabellesym.sty) are displayed properly, everything else is left |
134 isabellesym.sty) are displayed properly, everything else is left |
135 verbatim. We use isatool display and isatool print as front ends; |
135 verbatim. We use isatool display and isatool print as front ends; |
136 these are subject to the DVI_VIEWER and PRINT_COMMAND settings, |
136 these are subject to the DVI_VIEWER and PRINT_COMMAND settings, |
137 respectively. |
137 respectively. |
|
138 |
|
139 * Document preparation: Proof scripts as well as some other commands |
|
140 such as ML or parse/print_translation can now be hidden in the document. |
|
141 Hiding can be enabled either via the option '-H true' of isatool usedir |
|
142 or by setting the reference variable IsarOutput.hide_commands. Additional |
|
143 commands to be hidden may be declared using IsarOutput.add_hidden_commands. |
138 |
144 |
139 * ML: output via the Isabelle channels of writeln/warning/error |
145 * ML: output via the Isabelle channels of writeln/warning/error |
140 etc. is now passed through Output.output, with a hook for arbitrary |
146 etc. is now passed through Output.output, with a hook for arbitrary |
141 transformations depending on the print_mode (cf. Output.add_mode -- |
147 transformations depending on the print_mode (cf. Output.add_mode -- |
142 the first active mode that provides a output function wins). |
148 the first active mode that provides a output function wins). |