NEWS
changeset 3116 b890bae4273e
parent 3107 492a3d5d2b17
child 3205 816a1f9fd620
--- 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