# HG changeset patch
# User berghofe
# Date 1105449645 -3600
# Node ID d059da8434a55137d0f1057a43cc7ca451b0d121
# Parent  ee392b6181a46f05967aeef3ce19d7754318a501
Option for hiding proof scripts in documents.

diff -r ee392b6181a4 -r d059da8434a5 NEWS
--- 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,
   respectively.
 
+* 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 --