# HG changeset patch # User paulson # Date 1449506890 0 # Node ID 965769fe2b636e8fd0b9a070a9fa64423e40a487 # Parent d2e62ae01cd896866fbbb12048dc24cef550328a# Parent 5d2ade78e0026d35d061879ab386cbc82a9b4fea Merge diff -r d2e62ae01cd8 -r 965769fe2b63 NEWS --- 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. diff -r d2e62ae01cd8 -r 965769fe2b63 src/HOL/Hahn_Banach/Hahn_Banach.thy --- 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 \ graph H' h'" proof - - have "graph H h \ graph H' h'" + have "graph H h \ graph H' h'" proof (rule graph_extI) fix t assume t: "t \ H" from E HE t have "(SOME (y, a). t = y + a \ x' \ y \ H) = (t, 0)" diff -r d2e62ae01cd8 -r 965769fe2b63 src/HOL/Library/Formal_Power_Series.thy --- 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 \ 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 \ 0 \ a * c = b \ 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 (\n. 1::'a::field)) = 1 - X" by (simp add: fps_inverse_gp fps_eq_iff X_def) diff -r d2e62ae01cd8 -r 965769fe2b63 src/Tools/jEdit/src/isabelle.scala --- 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 */ diff -r d2e62ae01cd8 -r 965769fe2b63 src/Tools/jEdit/src/state_dockable.scala --- 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("Update") { 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()