Option for hiding proof scripts in documents.
Tue, 11 Jan 2005 14:20:45 +0100
changeset 15436 d059da8434a5
parent 15435 ee392b6181a4
child 15437 e1b3f0ea0fb6
Option for hiding proof scripts in documents.
--- a/NEWS	Tue Jan 11 14:19:08 2005 +0100
+++ b/NEWS	Tue Jan 11 14:20:45 2005 +0100
@@ -136,6 +136,12 @@
   these are subject to the DVI_VIEWER and PRINT_COMMAND settings,
+* Document preparation: Proof scripts as well as some other commands
+  such as ML or parse/print_translation can now be hidden in the document.
+  Hiding can be enabled either via the option '-H true' of isatool usedir
+  or by setting the reference variable IsarOutput.hide_commands. Additional
+  commands to be hidden may be declared using IsarOutput.add_hidden_commands.
 * ML: output via the Isabelle channels of writeln/warning/error
   etc. is now passed through Output.output, with a hook for arbitrary
   transformations depending on the print_mode (cf. Output.add_mode --