46 running ML program. |
46 running ML program. |
47 |
47 |
48 * The main Isabelle executable is managed as single-instance Desktop |
48 * The main Isabelle executable is managed as single-instance Desktop |
49 application uniformly on all platforms: Linux, Windows, Mac OS X. |
49 application uniformly on all platforms: Linux, Windows, Mac OS X. |
50 |
50 |
51 * The text overview column (status of errors, warnings etc.) is updated |
51 * The State panel manages explicit proof state output, with dynamic |
52 asynchronously, leading to much better editor reactivity. Moreover, the |
52 auto-update according to cursor movement. Alternatively, the jEdit |
53 full document node content is taken into account. |
53 action "isabelle.update-state" (shortcut S+ENTER) triggers manual |
54 |
54 update. |
55 * The State panel manages explicit proof state output. The jEdit action |
|
56 "isabelle.update-state" (shortcut S+ENTER) triggers manual update |
|
57 according to cursor position. |
|
58 |
55 |
59 * The Output panel no longer shows proof state output by default, to |
56 * The Output panel no longer shows proof state output by default, to |
60 avoid GUI overcrowding. INCOMPATIBILITY, use the State panel instead or |
57 avoid GUI overcrowding. INCOMPATIBILITY, use the State panel instead or |
61 enable option "editor_output_state". |
58 enable option "editor_output_state". |
|
59 |
|
60 * The text overview column (status of errors, warnings etc.) is updated |
|
61 asynchronously, leading to much better editor reactivity. Moreover, the |
|
62 full document node content is taken into account. The width of the |
|
63 column is scaled according to the main text area font, for improved |
|
64 visibility. |
|
65 |
|
66 * The main text area no longer changes its color hue in outdated |
|
67 situations. The text overview column takes over the role to indicate |
|
68 unfinished edits in the PIDE pipeline. This avoids flashing text display |
|
69 due to ad-hoc updates by auxiliary GUI components, such as the State |
|
70 panel. |
62 |
71 |
63 * Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls |
72 * Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls |
64 emphasized text style; the effect is visible in document output, not in |
73 emphasized text style; the effect is visible in document output, not in |
65 the editor. |
74 the editor. |
66 |
75 |
586 orders. |
595 orders. |
587 |
596 |
588 * Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals, Cauchy's |
597 * Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals, Cauchy's |
589 integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light |
598 integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light |
590 |
599 |
591 * Multivariate_Analysis: Added topological concepts such as connected components |
600 * Multivariate_Analysis: Added topological concepts such as connected components, |
592 and the inside or outside of a set. |
601 homotopic paths and the inside or outside of a set. |
593 |
602 |
594 * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef' |
603 * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef' |
595 command. Minor INCOMPATIBILITY, use 'function' instead. |
604 command. Minor INCOMPATIBILITY, use 'function' instead. |
596 |
605 |
597 * Inductive definitions ('inductive', 'coinductive', etc.) expose |
606 * Inductive definitions ('inductive', 'coinductive', etc.) expose |