--- a/NEWS Mon Dec 07 16:44:26 2015 +0000
+++ b/NEWS Mon Dec 07 16:48:10 2015 +0000
@@ -48,18 +48,27 @@
* The main Isabelle executable is managed as single-instance Desktop
application uniformly on all platforms: Linux, Windows, Mac OS X.
-* The text overview column (status of errors, warnings etc.) is updated
-asynchronously, leading to much better editor reactivity. Moreover, the
-full document node content is taken into account.
-
-* The State panel manages explicit proof state output. The jEdit action
-"isabelle.update-state" (shortcut S+ENTER) triggers manual update
-according to cursor position.
+* The State panel manages explicit proof state output, with dynamic
+auto-update according to cursor movement. Alternatively, the jEdit
+action "isabelle.update-state" (shortcut S+ENTER) triggers manual
+update.
* The Output panel no longer shows proof state output by default, to
avoid GUI overcrowding. INCOMPATIBILITY, use the State panel instead or
enable option "editor_output_state".
+* The text overview column (status of errors, warnings etc.) is updated
+asynchronously, leading to much better editor reactivity. Moreover, the
+full document node content is taken into account. The width of the
+column is scaled according to the main text area font, for improved
+visibility.
+
+* The main text area no longer changes its color hue in outdated
+situations. The text overview column takes over the role to indicate
+unfinished edits in the PIDE pipeline. This avoids flashing text display
+due to ad-hoc updates by auxiliary GUI components, such as the State
+panel.
+
* Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls
emphasized text style; the effect is visible in document output, not in
the editor.
@@ -588,8 +597,8 @@
* Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals, Cauchy's
integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light
-* Multivariate_Analysis: Added topological concepts such as connected components
-and the inside or outside of a set.
+* Multivariate_Analysis: Added topological concepts such as connected components,
+homotopic paths and the inside or outside of a set.
* Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef'
command. Minor INCOMPATIBILITY, use 'function' instead.
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Mon Dec 07 16:44:26 2015 +0000
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Mon Dec 07 16:48:10 2015 +0000
@@ -189,7 +189,7 @@
proof
show "g \<subseteq> graph H' h'"
proof -
- have "graph H h \<subseteq> graph H' h'"
+ have "graph H h \<subseteq> graph H' h'"
proof (rule graph_extI)
fix t assume t: "t \<in> H"
from E HE t have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
--- a/src/HOL/Library/Formal_Power_Series.thy Mon Dec 07 16:44:26 2015 +0000
+++ b/src/HOL/Library/Formal_Power_Series.thy Mon Dec 07 16:48:10 2015 +0000
@@ -1824,14 +1824,20 @@
shows "f * inverse f = 1"
by (metis mult.commute inverse_mult_eq_1 f0)
+(* FIXME: The last part of this proof should go through by simp once we have a proper
+ theorem collection for simplifying division on rings *)
lemma fps_divide_deriv:
- fixes a :: "'a::field fps"
- assumes a0: "b$0 \<noteq> 0"
- shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b\<^sup>2"
- using fps_inverse_deriv[OF a0] a0
- by (simp add: fps_divide_unit field_simps
- power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
-
+ assumes "b dvd (a :: 'a :: field fps)"
+ shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b^2"
+proof -
+ have eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b div c" for a b c :: "'a :: field fps"
+ by (drule sym) (simp add: mult.assoc)
+ from assms have "a = a / b * b" by simp
+ also have "fps_deriv (a / b * b) = fps_deriv (a / b) * b + a / b * fps_deriv b" by simp
+ finally have "fps_deriv (a / b) * b^2 = fps_deriv a * b - a * fps_deriv b" using assms
+ by (simp add: power2_eq_square algebra_simps)
+ thus ?thesis by (cases "b = 0") (auto simp: eq_divide_imp)
+qed
lemma fps_inverse_gp': "inverse (Abs_fps (\<lambda>n. 1::'a::field)) = 1 - X"
by (simp add: fps_inverse_gp fps_eq_iff X_def)
--- a/src/Tools/jEdit/src/isabelle.scala Mon Dec 07 16:44:26 2015 +0000
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Dec 07 16:48:10 2015 +0000
@@ -207,7 +207,7 @@
/* update state */
def update_state(view: View): Unit =
- state_dockable(view).foreach(_.update())
+ state_dockable(view).foreach(_.update_request())
/* ML statistics */
--- a/src/Tools/jEdit/src/state_dockable.scala Mon Dec 07 16:44:26 2015 +0000
+++ b/src/Tools/jEdit/src/state_dockable.scala Mon Dec 07 16:48:10 2015 +0000
@@ -57,9 +57,8 @@
/* update */
- private var do_update = true
-
- private def maybe_update(): Unit = GUI_Thread.require { if (do_update) update() }
+ def update_request(): Unit =
+ GUI_Thread.require { print_state.apply_query(Nil) }
def update()
{
@@ -69,24 +68,32 @@
case Some(snapshot) =>
(PIDE.editor.current_command(view, snapshot), print_state.get_location) match {
case (Some(command1), Some(command2)) if command1.id == command2.id =>
- case _ => print_state.apply_query(Nil)
+ case _ => update_request()
}
case None =>
}
}
+ /* auto update */
+
+ private var auto_update_enabled = true
+
+ private def auto_update(): Unit =
+ GUI_Thread.require { if (auto_update_enabled) update() }
+
+
/* controls */
private val auto_update_button = new CheckBox("Auto update") {
tooltip = "Indicate automatic update following cursor movement"
- reactions += { case ButtonClicked(_) => do_update = this.selected; maybe_update() }
- selected = do_update
+ reactions += { case ButtonClicked(_) => auto_update_enabled = this.selected; auto_update() }
+ selected = auto_update_enabled
}
private val update_button = new Button("<html><b>Update</b></html>") {
tooltip = "Update display according to the command at cursor position"
- reactions += { case ButtonClicked(_) => print_state.apply_query(Nil) }
+ reactions += { case ButtonClicked(_) => update_request() }
}
private val locate_button = new Button("Locate") {
@@ -112,10 +119,10 @@
GUI_Thread.later { handle_resize() }
case changed: Session.Commands_Changed =>
- if (changed.assignment) GUI_Thread.later { maybe_update() }
+ if (changed.assignment) GUI_Thread.later { auto_update() }
case Session.Caret_Focus =>
- GUI_Thread.later { maybe_update() }
+ GUI_Thread.later { auto_update() }
}
override def init()
@@ -125,7 +132,7 @@
PIDE.session.caret_focus += main
handle_resize()
print_state.activate()
- maybe_update()
+ auto_update()
}
override def exit()