NEWS
changeset 50717 30bcdd5c8e78
parent 50716 e04c44dc11fc
child 50720 834847691d99
child 50730 883963f45ac9
equal deleted inserted replaced
50716:e04c44dc11fc 50717:30bcdd5c8e78
    58 same Rich_Text_Area as regular Isabelle/jEdit buffers.  Activation of
    58 same Rich_Text_Area as regular Isabelle/jEdit buffers.  Activation of
    59 tooltips leads to some window that supports the same recursively,
    59 tooltips leads to some window that supports the same recursively,
    60 which can lead to stacks of tooltips as the semantic document content
    60 which can lead to stacks of tooltips as the semantic document content
    61 is explored.  ESCAPE closes the whole stack, individual windows may be
    61 is explored.  ESCAPE closes the whole stack, individual windows may be
    62 closed separately, or detached to become independent jEdit dockables.
    62 closed separately, or detached to become independent jEdit dockables.
       
    63 
       
    64 * Improved support for commands that produce graph output: the text
       
    65 message contains a clickable area to open a new instance of the graph
       
    66 browser on demand.
    63 
    67 
    64 * More robust incremental parsing of outer syntax (partial comments,
    68 * More robust incremental parsing of outer syntax (partial comments,
    65 malformed symbols).  Changing the balance of open/close quotes and
    69 malformed symbols).  Changing the balance of open/close quotes and
    66 comment delimiters works more conveniently with unfinished situations
    70 comment delimiters works more conveniently with unfinished situations
    67 that frequently occur in user interaction.
    71 that frequently occur in user interaction.