NEWS
changeset 49699 1301ed115729
parent 49647 21ae8500d261
child 49738 1e1611fd32df
equal deleted inserted replaced
49698:f68e237e8c10 49699:1301ed115729
    13     . more robust incremental parsing of outer syntax (partial
    13     . more robust incremental parsing of outer syntax (partial
    14       comments, malformed symbols);
    14       comments, malformed symbols);
    15     . smarter handling of tracing messages (via tracing_limit);
    15     . smarter handling of tracing messages (via tracing_limit);
    16     . more plugin options and preferences, based on Isabelle/Scala;
    16     . more plugin options and preferences, based on Isabelle/Scala;
    17     . uniform Java 7 platform on Linux, Mac OS X, Windows;
    17     . uniform Java 7 platform on Linux, Mac OS X, Windows;
       
    18 
       
    19 * Configuration option show_markup controls direct inlining of markup
       
    20 into the printed representation of formal entities --- notably type
       
    21 and sort constraints.  This enables Prover IDE users to retrieve that
       
    22 information via tooltips in the output window, for example.
    18 
    23 
    19 * Command 'ML_file' evaluates ML text from a file directly within the
    24 * Command 'ML_file' evaluates ML text from a file directly within the
    20 theory, without any predeclaration via 'uses' in the theory header.
    25 theory, without any predeclaration via 'uses' in the theory header.
    21 
    26 
    22 * Old command 'use' command and corresponding keyword 'uses' in the
    27 * Old command 'use' command and corresponding keyword 'uses' in the