equal
deleted
inserted
replaced
72 in the editor (hyperlinks, completion etc.). |
72 in the editor (hyperlinks, completion etc.). |
73 |
73 |
74 * Less waste of vertical space via negative line spacing (see Global |
74 * Less waste of vertical space via negative line spacing (see Global |
75 Options / Text Area). |
75 Options / Text Area). |
76 |
76 |
77 * Improved graphview panel (with optional output of PNG or PDF) |
77 * Improved graphview panel with optional output of PNG or PDF, for |
78 supersedes the old graph browser from 1996, but the latter remains |
78 display of 'thy_deps', 'locale_deps', 'class_deps' etc. |
79 available for some time as a fall-back. The old browser is still |
|
80 required for the massive graphs produced by 'thm_deps', for example. |
|
81 |
79 |
82 * Improved scheduling for asynchronous print commands (e.g. provers |
80 * Improved scheduling for asynchronous print commands (e.g. provers |
83 managed by the Sledgehammer panel) wrt. ongoing document processing. |
81 managed by the Sledgehammer panel) wrt. ongoing document processing. |
84 |
82 |
85 |
83 |