NEWS
changeset 15436 d059da8434a5
parent 15423 761a4f8e6ad6
child 15454 4b339d3907a0
equal deleted inserted replaced
15435:ee392b6181a4 15436:d059da8434a5
   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).