Merge
authorpaulson <lp15@cam.ac.uk>
Mon Dec 07 16:48:10 2015 +0000 (2015-12-07 ago)
changeset 61807965769fe2b63
parent 61806 d2e62ae01cd8
parent 61805 5d2ade78e002
child 61808 fc1556774cfe
Merge
NEWS
     1.1 --- a/NEWS	Mon Dec 07 16:44:26 2015 +0000
     1.2 +++ b/NEWS	Mon Dec 07 16:48:10 2015 +0000
     1.3 @@ -48,18 +48,27 @@
     1.4  * The main Isabelle executable is managed as single-instance Desktop
     1.5  application uniformly on all platforms: Linux, Windows, Mac OS X.
     1.6  
     1.7 -* The text overview column (status of errors, warnings etc.) is updated
     1.8 -asynchronously, leading to much better editor reactivity. Moreover, the
     1.9 -full document node content is taken into account.
    1.10 -
    1.11 -* The State panel manages explicit proof state output. The jEdit action
    1.12 -"isabelle.update-state" (shortcut S+ENTER) triggers manual update
    1.13 -according to cursor position.
    1.14 +* The State panel manages explicit proof state output, with dynamic
    1.15 +auto-update according to cursor movement. Alternatively, the jEdit
    1.16 +action "isabelle.update-state" (shortcut S+ENTER) triggers manual
    1.17 +update.
    1.18  
    1.19  * The Output panel no longer shows proof state output by default, to
    1.20  avoid GUI overcrowding. INCOMPATIBILITY, use the State panel instead or
    1.21  enable option "editor_output_state".
    1.22  
    1.23 +* The text overview column (status of errors, warnings etc.) is updated
    1.24 +asynchronously, leading to much better editor reactivity. Moreover, the
    1.25 +full document node content is taken into account. The width of the
    1.26 +column is scaled according to the main text area font, for improved
    1.27 +visibility.
    1.28 +
    1.29 +* The main text area no longer changes its color hue in outdated
    1.30 +situations. The text overview column takes over the role to indicate
    1.31 +unfinished edits in the PIDE pipeline. This avoids flashing text display
    1.32 +due to ad-hoc updates by auxiliary GUI components, such as the State
    1.33 +panel.
    1.34 +
    1.35  * Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls
    1.36  emphasized text style; the effect is visible in document output, not in
    1.37  the editor.
    1.38 @@ -588,8 +597,8 @@
    1.39  * Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals, Cauchy's
    1.40  integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light
    1.41  
    1.42 -* Multivariate_Analysis: Added topological concepts such as connected components
    1.43 -and the inside or outside of a set.
    1.44 +* Multivariate_Analysis: Added topological concepts such as connected components,
    1.45 +homotopic paths and the inside or outside of a set.
    1.46  
    1.47  * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef'
    1.48  command. Minor INCOMPATIBILITY, use 'function' instead.
     2.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Dec 07 16:44:26 2015 +0000
     2.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Dec 07 16:48:10 2015 +0000
     2.3 @@ -189,7 +189,7 @@
     2.4        proof
     2.5          show "g \<subseteq> graph H' h'"
     2.6          proof -
     2.7 -          have  "graph H h \<subseteq> graph H' h'"
     2.8 +          have "graph H h \<subseteq> graph H' h'"
     2.9            proof (rule graph_extI)
    2.10              fix t assume t: "t \<in> H"
    2.11              from E HE t have "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
     3.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Mon Dec 07 16:44:26 2015 +0000
     3.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Dec 07 16:48:10 2015 +0000
     3.3 @@ -1824,14 +1824,20 @@
     3.4    shows "f * inverse f = 1"
     3.5    by (metis mult.commute inverse_mult_eq_1 f0)
     3.6  
     3.7 +(* FIXME: The last part of this proof should go through by simp once we have a proper
     3.8 +   theorem collection for simplifying division on rings *)
     3.9  lemma fps_divide_deriv:
    3.10 -  fixes a :: "'a::field fps"
    3.11 -  assumes a0: "b$0 \<noteq> 0"
    3.12 -  shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b\<^sup>2"
    3.13 -  using fps_inverse_deriv[OF a0] a0
    3.14 -  by (simp add: fps_divide_unit field_simps
    3.15 -    power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
    3.16 -
    3.17 +  assumes "b dvd (a :: 'a :: field fps)"
    3.18 +  shows   "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b^2"
    3.19 +proof -
    3.20 +  have eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b div c" for a b c :: "'a :: field fps"
    3.21 +    by (drule sym) (simp add: mult.assoc)
    3.22 +  from assms have "a = a / b * b" by simp
    3.23 +  also have "fps_deriv (a / b * b) = fps_deriv (a / b) * b + a / b * fps_deriv b" by simp
    3.24 +  finally have "fps_deriv (a / b) * b^2 = fps_deriv a * b - a * fps_deriv b" using assms
    3.25 +    by (simp add: power2_eq_square algebra_simps)
    3.26 +  thus ?thesis by (cases "b = 0") (auto simp: eq_divide_imp)
    3.27 +qed
    3.28  
    3.29  lemma fps_inverse_gp': "inverse (Abs_fps (\<lambda>n. 1::'a::field)) = 1 - X"
    3.30    by (simp add: fps_inverse_gp fps_eq_iff X_def)
     4.1 --- a/src/Tools/jEdit/src/isabelle.scala	Mon Dec 07 16:44:26 2015 +0000
     4.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Mon Dec 07 16:48:10 2015 +0000
     4.3 @@ -207,7 +207,7 @@
     4.4    /* update state */
     4.5  
     4.6    def update_state(view: View): Unit =
     4.7 -    state_dockable(view).foreach(_.update())
     4.8 +    state_dockable(view).foreach(_.update_request())
     4.9  
    4.10  
    4.11    /* ML statistics */
     5.1 --- a/src/Tools/jEdit/src/state_dockable.scala	Mon Dec 07 16:44:26 2015 +0000
     5.2 +++ b/src/Tools/jEdit/src/state_dockable.scala	Mon Dec 07 16:48:10 2015 +0000
     5.3 @@ -57,9 +57,8 @@
     5.4  
     5.5    /* update */
     5.6  
     5.7 -  private var do_update = true
     5.8 -
     5.9 -  private def maybe_update(): Unit = GUI_Thread.require { if (do_update) update() }
    5.10 +  def update_request(): Unit =
    5.11 +    GUI_Thread.require { print_state.apply_query(Nil) }
    5.12  
    5.13    def update()
    5.14    {
    5.15 @@ -69,24 +68,32 @@
    5.16        case Some(snapshot) =>
    5.17          (PIDE.editor.current_command(view, snapshot), print_state.get_location) match {
    5.18            case (Some(command1), Some(command2)) if command1.id == command2.id =>
    5.19 -          case _ => print_state.apply_query(Nil)
    5.20 +          case _ => update_request()
    5.21          }
    5.22        case None =>
    5.23      }
    5.24    }
    5.25  
    5.26  
    5.27 +  /* auto update */
    5.28 +
    5.29 +  private var auto_update_enabled = true
    5.30 +
    5.31 +  private def auto_update(): Unit =
    5.32 +    GUI_Thread.require { if (auto_update_enabled) update() }
    5.33 +
    5.34 +
    5.35    /* controls */
    5.36  
    5.37    private val auto_update_button = new CheckBox("Auto update") {
    5.38      tooltip = "Indicate automatic update following cursor movement"
    5.39 -    reactions += { case ButtonClicked(_) => do_update = this.selected; maybe_update() }
    5.40 -    selected = do_update
    5.41 +    reactions += { case ButtonClicked(_) => auto_update_enabled = this.selected; auto_update() }
    5.42 +    selected = auto_update_enabled
    5.43    }
    5.44  
    5.45    private val update_button = new Button("<html><b>Update</b></html>") {
    5.46      tooltip = "Update display according to the command at cursor position"
    5.47 -    reactions += { case ButtonClicked(_) => print_state.apply_query(Nil) }
    5.48 +    reactions += { case ButtonClicked(_) => update_request() }
    5.49    }
    5.50  
    5.51    private val locate_button = new Button("Locate") {
    5.52 @@ -112,10 +119,10 @@
    5.53          GUI_Thread.later { handle_resize() }
    5.54  
    5.55        case changed: Session.Commands_Changed =>
    5.56 -        if (changed.assignment) GUI_Thread.later { maybe_update() }
    5.57 +        if (changed.assignment) GUI_Thread.later { auto_update() }
    5.58  
    5.59        case Session.Caret_Focus =>
    5.60 -        GUI_Thread.later { maybe_update() }
    5.61 +        GUI_Thread.later { auto_update() }
    5.62      }
    5.63  
    5.64    override def init()
    5.65 @@ -125,7 +132,7 @@
    5.66      PIDE.session.caret_focus += main
    5.67      handle_resize()
    5.68      print_state.activate()
    5.69 -    maybe_update()
    5.70 +    auto_update()
    5.71    }
    5.72  
    5.73    override def exit()