51 |
51 |
52 * Document preparation: antiquotations now provide the option |
52 * Document preparation: antiquotations now provide the option |
53 'locale=NAME' to specify an alternative context used for evaluating |
53 'locale=NAME' to specify an alternative context used for evaluating |
54 and printing the subsequent argument, as in @{thm [locale=LC] |
54 and printing the subsequent argument, as in @{thm [locale=LC] |
55 fold_commute}, for example. |
55 fold_commute}, for example. |
|
56 |
|
57 * Document preparation: commands 'display_drafts' and 'print_drafts' |
|
58 perform simple output of raw sources. Only those symbols that do |
|
59 not require additional LaTeX packages (depending on comments in |
|
60 isabellesym.sty) are displayed properly, everything else is left |
|
61 verbatim. We use isatool display and isatool print as front ends; |
|
62 these are subject to the DVI_VIEWER and PRINT_COMMAND settings, |
|
63 respectively. |
56 |
64 |
57 * ML: output via the Isabelle channels of writeln/warning/error |
65 * ML: output via the Isabelle channels of writeln/warning/error |
58 etc. is now passed through Output.output, with a hook for arbitrary |
66 etc. is now passed through Output.output, with a hook for arbitrary |
59 transformations depending on the print_mode (cf. Output.add_mode -- |
67 transformations depending on the print_mode (cf. Output.add_mode -- |
60 the first active mode that provides a output function wins). |
68 the first active mode that provides a output function wins). |