*** empty log message ***
authorwenzelm
Tue May 06 15:04:53 1997 +0200 (1997-05-06)
changeset 3116b890bae4273e
parent 3115 24ed05500380
child 3117 74c1b51c1cd9
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Tue May 06 14:36:37 1997 +0200
     1.2 +++ b/NEWS	Tue May 06 15:04:53 1997 +0200
     1.3 @@ -21,21 +21,23 @@
     1.4  
     1.5  *** Syntax ***
     1.6  
     1.7 +* supports alternative (named) syntax tables (parser and pretty
     1.8 +printer); internal interface is provided by add_modesyntax(_i);
     1.9 +
    1.10  * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
    1.11  be used in conjunction with the Isabelle symbol font; uses the
    1.12  "symbols" syntax table;
    1.13  
    1.14  * added token_translation interface (may translate name tokens in
    1.15  arbitrary ways, dependent on their type (free, bound, tfree, ...) and
    1.16 -the current print_mode);
    1.17 +the current print_mode); IMPORTANT: user print translation functions
    1.18 +are responsible for marking newly introduced bounds
    1.19 +(Syntax.mark_boundT);
    1.20  
    1.21  * token translations for modes "xterm" and "xterm_color" that display
    1.22  names in bold, underline etc. or colors (which requires a color
    1.23  version of xterm);
    1.24  
    1.25 -* supports alternative (named) syntax tables (parser and pretty
    1.26 -printer); internal interface is provided by add_modesyntax(_i);
    1.27 -
    1.28  * infixes may now be declared with names independent of their syntax;
    1.29  
    1.30  * added typed_print_translation (like print_translation, but may