--- a/src/HOL/Analysis/Conformal_Mappings.thy Fri Aug 11 23:38:33 2017 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Sat Aug 12 09:19:48 2017 +0200
@@ -3141,6 +3141,160 @@
ultimately show ?thesis using \<open>n>0\<close> unfolding P_def by auto
qed
+lemma zorder_eqI:
+ assumes "open s" "z \<in> s" "g holomorphic_on s" "g z \<noteq> 0" "n > 0"
+ assumes "\<And>w. w \<in> s \<Longrightarrow> f w = g w * (w - z) ^ n"
+ shows "zorder f z = n"
+proof -
+ have "continuous_on s g" by (rule holomorphic_on_imp_continuous_on) fact
+ moreover have "open (-{0::complex})" by auto
+ ultimately have "open ((g -` (-{0})) \<inter> s)"
+ unfolding continuous_on_open_vimage[OF \<open>open s\<close>] by blast
+ moreover from assms have "z \<in> (g -` (-{0})) \<inter> s" by auto
+ ultimately obtain r where r: "r > 0" "cball z r \<subseteq> (g -` (-{0})) \<inter> s"
+ unfolding open_contains_cball by blast
+
+ have "n > 0 \<and> r > 0 \<and> g holomorphic_on cball z r \<and>
+ (\<forall>w\<in>cball z r. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0)" (is "?P g r n")
+ using r assms(3,5,6) by auto
+ hence ex: "\<exists>g r. ?P g r n" by blast
+ have unique: "\<exists>!n. \<exists>g r. ?P g r n"
+ proof (rule holomorphic_factor_zero_Ex1)
+ from r have "(\<lambda>w. g w * (w - z) ^ n) holomorphic_on ball z r"
+ by (intro holomorphic_intros holomorphic_on_subset[OF assms(3)]) auto
+ also have "?this \<longleftrightarrow> f holomorphic_on ball z r"
+ using r assms by (intro holomorphic_cong refl) (auto simp: cball_def subset_iff)
+ finally show \<dots> .
+ next
+ let ?w = "z + of_real r / 2"
+ have "?w \<in> ball z r"
+ using r by (auto simp: dist_norm)
+ moreover from this and r have "g ?w \<noteq> 0" and "?w \<in> s"
+ by (auto simp: cball_def ball_def subset_iff)
+ with assms have "f ?w \<noteq> 0" using \<open>r > 0\<close> by auto
+ ultimately show "\<exists>w\<in>ball z r. f w \<noteq> 0" by blast
+ qed (insert assms r, auto)
+ from unique and ex have "(THE n. \<exists>g r. ?P g r n) = n"
+ by (rule the1_equality)
+ also have "(THE n. \<exists>g r. ?P g r n) = zorder f z"
+ by (simp add: zorder_def mult.commute)
+ finally show ?thesis .
+qed
+
+lemma simple_zeroI:
+ assumes "open s" "z \<in> s" "g holomorphic_on s" "g z \<noteq> 0"
+ assumes "\<And>w. w \<in> s \<Longrightarrow> f w = g w * (w - z)"
+ shows "zorder f z = 1"
+ using assms(1-4) by (rule zorder_eqI) (use assms(5) in auto)
+
+lemma higher_deriv_power:
+ shows "(deriv ^^ j) (\<lambda>w. (w - z) ^ n) w =
+ pochhammer (of_nat (Suc n - j)) j * (w - z) ^ (n - j)"
+proof (induction j arbitrary: w)
+ case 0
+ thus ?case by auto
+next
+ case (Suc j w)
+ have "(deriv ^^ Suc j) (\<lambda>w. (w - z) ^ n) w = deriv ((deriv ^^ j) (\<lambda>w. (w - z) ^ n)) w"
+ by simp
+ also have "(deriv ^^ j) (\<lambda>w. (w - z) ^ n) =
+ (\<lambda>w. pochhammer (of_nat (Suc n - j)) j * (w - z) ^ (n - j))"
+ using Suc by (intro Suc.IH ext)
+ also {
+ have "(\<dots> has_field_derivative of_nat (n - j) *
+ pochhammer (of_nat (Suc n - j)) j * (w - z) ^ (n - Suc j)) (at w)"
+ using Suc.prems by (auto intro!: derivative_eq_intros)
+ also have "of_nat (n - j) * pochhammer (of_nat (Suc n - j)) j =
+ pochhammer (of_nat (Suc n - Suc j)) (Suc j)"
+ by (cases "Suc j \<le> n", subst pochhammer_rec)
+ (insert Suc.prems, simp_all add: algebra_simps Suc_diff_le pochhammer_0_left)
+ finally have "deriv (\<lambda>w. pochhammer (of_nat (Suc n - j)) j * (w - z) ^ (n - j)) w =
+ \<dots> * (w - z) ^ (n - Suc j)"
+ by (rule DERIV_imp_deriv)
+ }
+ finally show ?case .
+qed
+
+lemma zorder_eqI':
+ assumes "open s" "connected s" "z \<in> s" "f holomorphic_on s"
+ assumes zero: "\<And>i. i < n' \<Longrightarrow> (deriv ^^ i) f z = 0"
+ assumes nz: "(deriv ^^ n') f z \<noteq> 0" and n: "n' > 0"
+ shows "zorder f z = n'"
+proof -
+ {
+ assume *: "\<And>w. w \<in> s \<Longrightarrow> f w = 0"
+ hence "eventually (\<lambda>u. u \<in> s) (nhds z)"
+ using assms by (intro eventually_nhds_in_open) auto
+ hence "eventually (\<lambda>u. f u = 0) (nhds z)"
+ by eventually_elim (simp_all add: *)
+ hence "(deriv ^^ n') f z = (deriv ^^ n') (\<lambda>_. 0) z"
+ by (intro higher_deriv_cong_ev) auto
+ also have "(deriv ^^ n') (\<lambda>_. 0) z = 0"
+ by (induction n') simp_all
+ finally have False using nz by contradiction
+ }
+ hence nz': "\<exists>w\<in>s. f w \<noteq> 0" by blast
+
+ from zero[of 0] and n have [simp]: "f z = 0" by simp
+
+ define n g where "n = zorder f z" and "g = zer_poly f z"
+ from zorder_exist[OF assms(1-4) \<open>f z = 0\<close> nz']
+ obtain r where r: "n > 0" "r > 0" "cball z r \<subseteq> s" "g holomorphic_on cball z r"
+ "\<forall>w\<in>cball z r. f w = g w * (w - z) ^ n \<and> g w \<noteq> 0"
+ unfolding n_def g_def by blast
+
+ define A where "A = (\<lambda>i. of_nat (i choose n) * fact n * (deriv ^^ (i - n)) g z)"
+ {
+ fix i :: nat
+ have "eventually (\<lambda>w. w \<in> ball z r) (nhds z)"
+ using r by (intro eventually_nhds_in_open) auto
+ hence "eventually (\<lambda>w. f w = (w - z) ^ n * g w) (nhds z)"
+ by eventually_elim (use r in auto)
+ hence "(deriv ^^ i) f z = (deriv ^^ i) (\<lambda>w. (w - z) ^ n * g w) z"
+ by (intro higher_deriv_cong_ev) auto
+ also have "\<dots> = (\<Sum>j=0..i. of_nat (i choose j) *
+ (deriv ^^ j) (\<lambda>w. (w - z) ^ n) z * (deriv ^^ (i - j)) g z)"
+ using r by (intro higher_deriv_mult[of _ "ball z r"]) (auto intro!: holomorphic_intros)
+ also have "\<dots> = (\<Sum>j=0..i. if j = n then of_nat (i choose n) * fact n * (deriv ^^ (i - n)) g z
+ else 0)"
+ proof (intro sum.cong refl, goal_cases)
+ case (1 j)
+ have "(deriv ^^ j) (\<lambda>w. (w - z) ^ n) z =
+ pochhammer (of_nat (Suc n - j)) j * 0 ^ (n - j)"
+ by (subst higher_deriv_power) auto
+ also have "\<dots> = (if j = n then fact j else 0)"
+ by (auto simp: not_less pochhammer_0_left pochhammer_fact)
+ also have "of_nat (i choose j) * \<dots> * (deriv ^^ (i - j)) g z =
+ (if j = n then of_nat (i choose n) * fact n * (deriv ^^ (i - n)) g z else 0)"
+ by simp
+ finally show ?case .
+ qed
+ also have "\<dots> = (if i \<ge> n then A i else 0)"
+ by (auto simp: A_def)
+ finally have "(deriv ^^ i) f z = \<dots>" .
+ } note * = this
+
+ from *[of n] and r have "(deriv ^^ n) f z \<noteq> 0"
+ by (simp add: A_def)
+ with zero[of n] have "n \<ge> n'" by (cases "n \<ge> n'") auto
+ with nz show "n = n'"
+ by (auto simp: * split: if_splits)
+qed
+
+lemma simple_zeroI':
+ assumes "open s" "connected s" "z \<in> s"
+ assumes "\<And>z. z \<in> s \<Longrightarrow> (f has_field_derivative f' z) (at z)"
+ assumes "f z = 0" "f' z \<noteq> 0"
+ shows "zorder f z = 1"
+proof -
+ have "deriv f z = f' z" if "z \<in> s" for z
+ using that by (intro DERIV_imp_deriv assms) auto
+ moreover from assms have "f holomorphic_on s"
+ by (subst holomorphic_on_open) auto
+ ultimately show ?thesis using assms
+ by (intro zorder_eqI'[of s]) auto
+qed
+
lemma porder_exist:
fixes f::"complex \<Rightarrow> complex" and z::complex
defines "n \<equiv> porder f z" and "h \<equiv> pol_poly f z"
--- a/src/HOL/Analysis/Derivative.thy Fri Aug 11 23:38:33 2017 +0200
+++ b/src/HOL/Analysis/Derivative.thy Sat Aug 12 09:19:48 2017 +0200
@@ -2421,6 +2421,22 @@
thus ?thesis by (simp add: deriv_def assms)
qed
+lemma higher_deriv_cong_ev:
+ assumes "eventually (\<lambda>x. f x = g x) (nhds x)" "x = y"
+ shows "(deriv ^^ n) f x = (deriv ^^ n) g y"
+proof -
+ from assms(1) have "eventually (\<lambda>x. (deriv ^^ n) f x = (deriv ^^ n) g x) (nhds x)"
+ proof (induction n arbitrary: f g)
+ case (Suc n)
+ from Suc.prems have "eventually (\<lambda>y. eventually (\<lambda>z. f z = g z) (nhds y)) (nhds x)"
+ by (simp add: eventually_eventually)
+ hence "eventually (\<lambda>x. deriv f x = deriv g x) (nhds x)"
+ by eventually_elim (rule deriv_cong_ev, simp_all)
+ thus ?case by (auto intro!: deriv_cong_ev Suc simp: funpow_Suc_right simp del: funpow.simps)
+ qed auto
+ from eventually_nhds_x_imp_x[OF this] assms(2) show ?thesis by simp
+qed
+
lemma real_derivative_chain:
fixes x :: real
shows "f differentiable at x \<Longrightarrow> g differentiable at (f x)
--- a/src/HOL/Analysis/Winding_Numbers.thy Fri Aug 11 23:38:33 2017 +0200
+++ b/src/HOL/Analysis/Winding_Numbers.thy Sat Aug 12 09:19:48 2017 +0200
@@ -779,5 +779,152 @@
using simple_closed_path_winding_number_cases
by fastforce
+
+subsection \<open>Winding number for rectangular paths\<close>
+
+(* TODO: Move *)
+lemma closed_segmentI:
+ "u \<in> {0..1} \<Longrightarrow> z = (1 - u) *\<^sub>R a + u *\<^sub>R b \<Longrightarrow> z \<in> closed_segment a b"
+ by (auto simp: closed_segment_def)
+
+lemma in_cbox_complex_iff:
+ "x \<in> cbox a b \<longleftrightarrow> Re x \<in> {Re a..Re b} \<and> Im x \<in> {Im a..Im b}"
+ by (cases x; cases a; cases b) (auto simp: cbox_Complex_eq)
+
+lemma box_Complex_eq:
+ "box (Complex a c) (Complex b d) = (\<lambda>(x,y). Complex x y) ` (box a b \<times> box c d)"
+ by (auto simp: box_def Basis_complex_def image_iff complex_eq_iff)
+
+lemma in_box_complex_iff:
+ "x \<in> box a b \<longleftrightarrow> Re x \<in> {Re a<..<Re b} \<and> Im x \<in> {Im a<..<Im b}"
+ by (cases x; cases a; cases b) (auto simp: box_Complex_eq)
+(* END TODO *)
+
+lemma closed_segment_same_Re:
+ assumes "Re a = Re b"
+ shows "closed_segment a b = {z. Re z = Re a \<and> Im z \<in> closed_segment (Im a) (Im b)}"
+proof safe
+ fix z assume "z \<in> closed_segment a b"
+ then obtain u where u: "u \<in> {0..1}" "z = a + of_real u * (b - a)"
+ by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
+ from assms show "Re z = Re a" by (auto simp: u)
+ from u(1) show "Im z \<in> closed_segment (Im a) (Im b)"
+ by (intro closed_segmentI[of u]) (auto simp: u algebra_simps)
+next
+ fix z assume [simp]: "Re z = Re a" and "Im z \<in> closed_segment (Im a) (Im b)"
+ then obtain u where u: "u \<in> {0..1}" "Im z = Im a + of_real u * (Im b - Im a)"
+ by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
+ from u(1) show "z \<in> closed_segment a b" using assms
+ by (intro closed_segmentI[of u]) (auto simp: u algebra_simps scaleR_conv_of_real complex_eq_iff)
+qed
+
+lemma closed_segment_same_Im:
+ assumes "Im a = Im b"
+ shows "closed_segment a b = {z. Im z = Im a \<and> Re z \<in> closed_segment (Re a) (Re b)}"
+proof safe
+ fix z assume "z \<in> closed_segment a b"
+ then obtain u where u: "u \<in> {0..1}" "z = a + of_real u * (b - a)"
+ by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
+ from assms show "Im z = Im a" by (auto simp: u)
+ from u(1) show "Re z \<in> closed_segment (Re a) (Re b)"
+ by (intro closed_segmentI[of u]) (auto simp: u algebra_simps)
+next
+ fix z assume [simp]: "Im z = Im a" and "Re z \<in> closed_segment (Re a) (Re b)"
+ then obtain u where u: "u \<in> {0..1}" "Re z = Re a + of_real u * (Re b - Re a)"
+ by (auto simp: closed_segment_def scaleR_conv_of_real algebra_simps)
+ from u(1) show "z \<in> closed_segment a b" using assms
+ by (intro closed_segmentI[of u]) (auto simp: u algebra_simps scaleR_conv_of_real complex_eq_iff)
+qed
+
+
+definition rectpath where
+ "rectpath a1 a3 = (let a2 = Complex (Re a3) (Im a1); a4 = Complex (Re a1) (Im a3)
+ in linepath a1 a2 +++ linepath a2 a3 +++ linepath a3 a4 +++ linepath a4 a1)"
+
+lemma path_rectpath [simp, intro]: "path (rectpath a b)"
+ by (simp add: Let_def rectpath_def)
+
+lemma valid_path_rectpath [simp, intro]: "valid_path (rectpath a b)"
+ by (simp add: Let_def rectpath_def)
+
+lemma pathstart_rectpath [simp]: "pathstart (rectpath a1 a3) = a1"
+ by (simp add: rectpath_def Let_def)
+
+lemma pathfinish_rectpath [simp]: "pathfinish (rectpath a1 a3) = a1"
+ by (simp add: rectpath_def Let_def)
+
+lemma simple_path_rectpath [simp, intro]:
+ assumes "Re a1 \<noteq> Re a3" "Im a1 \<noteq> Im a3"
+ shows "simple_path (rectpath a1 a3)"
+ unfolding rectpath_def Let_def using assms
+ by (intro simple_path_join_loop arc_join arc_linepath)
+ (auto simp: complex_eq_iff path_image_join closed_segment_same_Re closed_segment_same_Im)
+
+lemma path_image_rectpath:
+ assumes "Re a1 \<le> Re a3" "Im a1 \<le> Im a3"
+ shows "path_image (rectpath a1 a3) =
+ {z. Re z \<in> {Re a1, Re a3} \<and> Im z \<in> {Im a1..Im a3}} \<union>
+ {z. Im z \<in> {Im a1, Im a3} \<and> Re z \<in> {Re a1..Re a3}}" (is "?lhs = ?rhs")
+proof -
+ define a2 a4 where "a2 = Complex (Re a3) (Im a1)" and "a4 = Complex (Re a1) (Im a3)"
+ have "?lhs = closed_segment a1 a2 \<union> closed_segment a2 a3 \<union>
+ closed_segment a4 a3 \<union> closed_segment a1 a4"
+ by (simp_all add: rectpath_def Let_def path_image_join closed_segment_commute
+ a2_def a4_def Un_assoc)
+ also have "\<dots> = ?rhs" using assms
+ by (auto simp: rectpath_def Let_def path_image_join a2_def a4_def
+ closed_segment_same_Re closed_segment_same_Im closed_segment_eq_real_ivl)
+ finally show ?thesis .
+qed
+
+lemma path_image_rectpath_subset_cbox:
+ assumes "Re a \<le> Re b" "Im a \<le> Im b"
+ shows "path_image (rectpath a b) \<subseteq> cbox a b"
+ using assms by (auto simp: path_image_rectpath in_cbox_complex_iff)
+
+lemma path_image_rectpath_inter_box:
+ assumes "Re a \<le> Re b" "Im a \<le> Im b"
+ shows "path_image (rectpath a b) \<inter> box a b = {}"
+ using assms by (auto simp: path_image_rectpath in_box_complex_iff)
+
+lemma path_image_rectpath_cbox_minus_box:
+ assumes "Re a \<le> Re b" "Im a \<le> Im b"
+ shows "path_image (rectpath a b) = cbox a b - box a b"
+ using assms by (auto simp: path_image_rectpath in_cbox_complex_iff
+ in_box_complex_iff)
+
+lemma winding_number_rectpath:
+ assumes "z \<in> box a1 a3"
+ shows "winding_number (rectpath a1 a3) z = 1"
+proof -
+ from assms have less: "Re a1 < Re a3" "Im a1 < Im a3"
+ by (auto simp: in_box_complex_iff)
+ define a2 a4 where "a2 = Complex (Re a3) (Im a1)" and "a4 = Complex (Re a1) (Im a3)"
+ let ?l1 = "linepath a1 a2" and ?l2 = "linepath a2 a3"
+ and ?l3 = "linepath a3 a4" and ?l4 = "linepath a4 a1"
+ from assms and less have "z \<notin> path_image (rectpath a1 a3)"
+ by (auto simp: path_image_rectpath_cbox_minus_box)
+ also have "path_image (rectpath a1 a3) =
+ path_image ?l1 \<union> path_image ?l2 \<union> path_image ?l3 \<union> path_image ?l4"
+ by (simp add: rectpath_def Let_def path_image_join Un_assoc a2_def a4_def)
+ finally have "z \<notin> \<dots>" .
+ moreover have "\<forall>l\<in>{?l1,?l2,?l3,?l4}. Re (winding_number l z) > 0"
+ unfolding ball_simps HOL.simp_thms a2_def a4_def
+ by (intro conjI; (rule winding_number_linepath_pos_lt;
+ (insert assms, auto simp: a2_def a4_def in_box_complex_iff mult_neg_neg))+)
+ ultimately have "Re (winding_number (rectpath a1 a3) z) > 0"
+ by (simp add: winding_number_join path_image_join rectpath_def Let_def a2_def a4_def)
+ thus "winding_number (rectpath a1 a3) z = 1" using assms less
+ by (intro simple_closed_path_winding_number_pos simple_path_rectpath)
+ (auto simp: path_image_rectpath_cbox_minus_box)
+qed
+
+lemma winding_number_rectpath_outside:
+ assumes "Re a1 \<le> Re a3" "Im a1 \<le> Im a3"
+ assumes "z \<notin> cbox a1 a3"
+ shows "winding_number (rectpath a1 a3) z = 0"
+ using assms by (intro winding_number_zero_outside[OF _ _ _ assms(3)]
+ path_image_rectpath_subset_cbox) simp_all
+
end
--- a/src/HOL/Factorial.thy Fri Aug 11 23:38:33 2017 +0200
+++ b/src/HOL/Factorial.thy Sat Aug 12 09:19:48 2017 +0200
@@ -264,6 +264,10 @@
pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a]
by (auto simp add: not_le[symmetric])
+lemma pochhammer_0_left:
+ "pochhammer 0 n = (if n = 0 then 1 else 0)"
+ by (induction n) (simp_all add: pochhammer_rec)
+
lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (\<exists>k < n. a = - of_nat k)"
by (auto simp add: pochhammer_prod eq_neg_iff_add_eq_0)
--- a/src/HOL/Library/Finite_Map.thy Fri Aug 11 23:38:33 2017 +0200
+++ b/src/HOL/Library/Finite_Map.thy Sat Aug 12 09:19:48 2017 +0200
@@ -605,6 +605,13 @@
apply transfer'
using set_of_map_inj unfolding inj_def by auto
+lemma fset_of_fmap_iff[simp]: "(a, b) |\<in>| fset_of_fmap m \<longleftrightarrow> fmlookup m a = Some b"
+by transfer' (auto simp: set_of_map_def)
+
+lemma fset_of_fmap_iff'[simp]: "(a, b) \<in> fset (fset_of_fmap m) \<longleftrightarrow> fmlookup m a = Some b"
+by transfer' (auto simp: set_of_map_def)
+
+
lift_definition fmap_of_list :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) fmap"
is map_of
parametric map_of_transfer
@@ -900,6 +907,47 @@
lemma fmmap_subset[intro]: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmmap f m \<subseteq>\<^sub>f fmmap f n"
by transfer' (auto simp: map_le_def)
+lemma fmmap_fset_of_fmap: "fset_of_fmap (fmmap f m) = (\<lambda>(k, v). (k, f v)) |`| fset_of_fmap m"
+including fset.lifting
+by transfer' (auto simp: set_of_map_def)
+
+
+subsection \<open>@{const size} setup\<close>
+
+definition size_fmap :: "('a \<Rightarrow> nat) \<Rightarrow> ('b \<Rightarrow> nat) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> nat" where
+[simp]: "size_fmap f g m = size_fset (\<lambda>(a, b). f a + g b) (fset_of_fmap m)"
+
+instantiation fmap :: (type, type) size begin
+
+definition size_fmap where
+size_fmap_overloaded_def: "size_fmap = Finite_Map.size_fmap (\<lambda>_. 0) (\<lambda>_. 0)"
+
+instance ..
+
+end
+
+lemma size_fmap_overloaded_simps[simp]: "size x = size (fset_of_fmap x)"
+unfolding size_fmap_overloaded_def
+by simp
+
+lemma fmap_size_o_map: "inj h \<Longrightarrow> size_fmap f g \<circ> fmmap h = size_fmap f (g \<circ> h)"
+ unfolding size_fmap_def
+ apply (auto simp: fun_eq_iff fmmap_fset_of_fmap)
+ apply (subst sum.reindex)
+ subgoal for m
+ using prod.inj_map[unfolded map_prod_def, of "\<lambda>x. x" h]
+ unfolding inj_on_def
+ by auto
+ subgoal
+ by (rule sum.cong) (auto split: prod.splits)
+ done
+
+setup \<open>
+BNF_LFP_Size.register_size_global @{type_name fmap} @{const_name size_fmap}
+ @{thm size_fmap_overloaded_def} @{thms size_fmap_def size_fmap_overloaded_simps}
+ @{thms fmap_size_o_map}
+\<close>
+
subsection \<open>Additional operations\<close>
--- a/src/Tools/VSCode/extension/package.json Fri Aug 11 23:38:33 2017 +0200
+++ b/src/Tools/VSCode/extension/package.json Sat Aug 12 09:19:48 2017 +0200
@@ -10,7 +10,7 @@
"document preparation"
],
"icon": "isabelle.png",
- "version": "0.22.0",
+ "version": "0.23.0",
"publisher": "makarius",
"license": "MIT",
"repository": {
--- a/src/Tools/VSCode/extension/src/extension.ts Fri Aug 11 23:38:33 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts Sat Aug 12 09:19:48 2017 +0200
@@ -129,7 +129,8 @@
commands.registerCommand("isabelle.state", uri => state_panel.init(uri)),
commands.registerCommand("_isabelle.state-locate", state_panel.locate),
commands.registerCommand("_isabelle.state-update", state_panel.update),
- commands.registerCommand("_isabelle.state-auto-update", state_panel.auto_update))
+ commands.registerCommand("_isabelle.state-auto-update", state_panel.auto_update),
+ workspace.onDidCloseTextDocument(document => state_panel.exit_uri(document.uri)))
language_client.onReady().then(() => state_panel.setup(context, language_client))
--- a/src/Tools/VSCode/extension/src/state_panel.ts Fri Aug 11 23:38:33 2017 +0200
+++ b/src/Tools/VSCode/extension/src/state_panel.ts Sat Aug 12 09:19:48 2017 +0200
@@ -67,6 +67,12 @@
if (language_client) language_client.sendNotification(protocol.state_exit_type, { id: id })
}
+export function exit_uri(uri: Uri)
+{
+ const id = decode_state(uri)
+ if (id) exit(id)
+}
+
export function locate(id: number)
{
if (language_client) language_client.sendNotification(protocol.state_locate_type, { id: id })
--- a/src/Tools/VSCode/src/state_panel.scala Fri Aug 11 23:38:33 2017 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala Sat Aug 12 09:19:48 2017 +0200
@@ -57,10 +57,12 @@
/* query operation */
+ private val output_active = Synchronized(true)
+
private val print_state =
new Query_Operation(server.editor, (), "print_state", _ => (),
(snapshot, results, body) =>
- {
+ if (output_active.value) {
val text = server.resources.output_pretty_message(Pretty.separate(body))
val content =
HTML.output_document(
@@ -160,8 +162,9 @@
def exit()
{
- server.editor.send_wait_dispatcher { print_state.deactivate() }
+ output_active.change(_ => false)
server.session.commands_changed -= main
server.session.caret_focus -= main
+ server.editor.send_wait_dispatcher { print_state.deactivate() }
}
}