# HG changeset patch
# User wenzelm
# Date 862923893 -7200
# Node ID b890bae4273e622a94bde1db2d512ddc2a9bcedb
# Parent  24ed05500380fe1ffcfe5681fb06281e20e61b23
*** empty log message ***

diff -r 24ed05500380 -r b890bae4273e NEWS
--- a/NEWS	Tue May 06 14:36:37 1997 +0200
+++ b/NEWS	Tue May 06 15:04:53 1997 +0200
@@ -21,21 +21,23 @@
 
 *** Syntax ***
 
+* supports alternative (named) syntax tables (parser and pretty
+printer); internal interface is provided by add_modesyntax(_i);
+
 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
 be used in conjunction with the Isabelle symbol font; uses the
 "symbols" syntax table;
 
 * added token_translation interface (may translate name tokens in
 arbitrary ways, dependent on their type (free, bound, tfree, ...) and
-the current print_mode);
+the current print_mode); IMPORTANT: user print translation functions
+are responsible for marking newly introduced bounds
+(Syntax.mark_boundT);
 
 * token translations for modes "xterm" and "xterm_color" that display
 names in bold, underline etc. or colors (which requires a color
 version of xterm);
 
-* supports alternative (named) syntax tables (parser and pretty
-printer); internal interface is provided by add_modesyntax(_i);
-
 * infixes may now be declared with names independent of their syntax;
 
 * added typed_print_translation (like print_translation, but may