--- a/NEWS Tue Apr 07 17:03:44 2020 +0200
+++ b/NEWS Tue Apr 07 17:03:57 2020 +0200
@@ -7,6 +7,11 @@
New in this Isabelle version
----------------------------
+*** System ***
+
+* The command-line tool "isabelle console" now supports interrupts
+properly (on Linux and macOS).
+
New in Isabelle2020 (April 2020)
--- a/src/HOL/Binomial.thy Tue Apr 07 17:03:44 2020 +0200
+++ b/src/HOL/Binomial.thy Tue Apr 07 17:03:57 2020 +0200
@@ -121,21 +121,35 @@
using binomial_Suc_Suc [of "n - 1" "k - 1"] by simp
lemma Suc_times_binomial_eq: "Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
- apply (induct n arbitrary: k)
- apply simp
- apply arith
- apply (case_tac k)
- apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0)
- done
+proof (induction n arbitrary: k)
+ case 0
+ then show ?case
+ by auto
+next
+ case (Suc n)
+ show ?case
+ proof (cases k)
+ case (Suc k')
+ then show ?thesis
+ using Suc.IH
+ by (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0)
+ qed auto
+qed
lemma binomial_le_pow2: "n choose k \<le> 2^n"
- apply (induct n arbitrary: k)
- apply (case_tac k)
- apply simp_all
- apply (case_tac k)
- apply auto
- apply (simp add: add_le_mono mult_2)
- done
+proof (induction n arbitrary: k)
+ case 0
+ then show ?case
+ using le_less less_le_trans by fastforce
+next
+ case (Suc n)
+ show ?case
+ proof (cases k)
+ case (Suc k')
+ then show ?thesis
+ using Suc.IH by (simp add: add_le_mono mult_2)
+ qed auto
+qed
text \<open>The absorption property.\<close>
lemma Suc_times_binomial: "Suc k * (Suc n choose Suc k) = Suc n * (n choose k)"
@@ -246,9 +260,7 @@
assumes kn: "k \<le> n"
shows "(of_nat (n choose k) :: 'a::field_char_0) = fact n / (fact k * fact (n - k))"
using binomial_fact_lemma[OF kn]
- apply (simp add: field_simps)
- apply (metis mult.commute of_nat_fact of_nat_mult)
- done
+ by (metis (mono_tags, lifting) fact_nonzero mult_eq_0_iff nonzero_mult_div_cancel_left of_nat_fact of_nat_mult)
lemma fact_binomial:
assumes "k \<le> n"
@@ -361,11 +373,11 @@
for a :: "'a::field_char_0"
proof (cases k)
case (Suc k')
+ then have "a gchoose k = pochhammer (a - of_nat k') (Suc k') / ((1 + of_nat k') * fact k')"
+ by (simp add: gbinomial_prod_rev pochhammer_prod_rev atLeastLessThanSuc_atLeastAtMost
+ prod.atLeast_Suc_atMost_Suc_shift of_nat_diff flip: power_mult_distrib prod.cl_ivl_Suc)
then show ?thesis
- apply (simp add: pochhammer_minus)
- apply (simp add: gbinomial_prod_rev pochhammer_prod_rev power_mult_distrib [symmetric] atLeastLessThanSuc_atLeastAtMost
- prod.atLeast_Suc_atMost_Suc_shift of_nat_diff del: prod.cl_ivl_Suc)
- done
+ by (simp add: pochhammer_minus Suc)
qed auto
lemma gbinomial_pochhammer': "a gchoose k = pochhammer (a - of_nat k + 1) k / fact k"
@@ -437,10 +449,8 @@
(is "?l = ?r")
proof -
have "?r = ((- 1) ^k * pochhammer (- a) k / fact k) * (of_nat k - (- a + of_nat k))"
- apply (simp only: gbinomial_pochhammer pochhammer_Suc right_diff_distrib power_Suc)
- apply (simp del: of_nat_Suc fact_Suc)
- apply (auto simp add: field_simps simp del: of_nat_Suc)
- done
+ unfolding gbinomial_pochhammer pochhammer_Suc right_diff_distrib power_Suc
+ by (auto simp add: field_simps simp del: of_nat_Suc)
also have "\<dots> = ?l"
by (simp add: field_simps gbinomial_pochhammer)
finally show ?thesis ..
@@ -459,17 +469,17 @@
next
case (Suc h)
have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{0..h}. a - of_nat i)"
- apply (rule prod.reindex_cong [where l = Suc])
- using Suc
- apply (auto simp add: image_Suc_atMost)
- done
+ proof (rule prod.reindex_cong)
+ show "{1..k} = Suc ` {0..h}"
+ using Suc by (auto simp add: image_Suc_atMost)
+ qed auto
have "fact (Suc k) * (a gchoose k + (a gchoose (Suc k))) =
(a gchoose Suc h) * (fact (Suc (Suc h))) +
(a gchoose Suc (Suc h)) * (fact (Suc (Suc h)))"
by (simp add: Suc field_simps del: fact_Suc)
also have "\<dots> =
(a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) + (\<Prod>i=0..Suc h. a - of_nat i)"
- apply (simp del: fact_Suc prod.op_ivl_Suc add: gbinomial_mult_fact field_simps mult.left_commute [of _ "2"])
+ apply (simp only: gbinomial_mult_fact field_simps mult.left_commute [of _ "2"])
apply (simp del: fact_Suc add: fact_Suc [of "Suc h"] field_simps gbinomial_mult_fact
mult.left_commute [of _ "2"] atLeastLessThanSuc_atLeastAtMost)
done
@@ -608,10 +618,8 @@
also have "(\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) +
pochhammer b (Suc n) =
(\<Sum>i=0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
- apply (subst sum.atLeast_Suc_atMost)
- apply simp
- apply (subst sum.shift_bounds_cl_Suc_ivl)
- apply (simp add: atLeast0AtMost)
+ apply (subst sum.atLeast_Suc_atMost, simp)
+ apply (simp add: sum.shift_bounds_cl_Suc_ivl atLeast0AtMost del: sum.cl_ivl_Suc)
done
also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
using Suc by (intro sum.mono_neutral_right) (auto simp: not_le binomial_eq_0)
@@ -641,12 +649,11 @@
using assms of_nat_0_le_iff order_trans by blast
have "(a / of_nat k :: 'a) ^ k = (\<Prod>i = 0..<k. a / of_nat k :: 'a)"
by simp
- also have "\<dots> \<le> a gchoose k" (* FIXME *)
- unfolding gbinomial_altdef_of_nat
- apply (safe intro!: prod_mono)
- apply simp_all
- prefer 2
- subgoal premises for i
+ also have "\<dots> \<le> a gchoose k"
+ proof -
+ have "\<And>i. i < k \<Longrightarrow> 0 \<le> a / of_nat k"
+ by (simp add: x zero_le_divide_iff)
+ moreover have "a / of_nat k \<le> (a - of_nat i) / of_nat (k - i)" if "i < k" for i
proof -
from assms have "a * of_nat i \<ge> of_nat (i * k)"
by (metis mult.commute mult_le_cancel_right of_nat_less_0_iff of_nat_mult)
@@ -655,12 +662,14 @@
then have "a * of_nat (k - i) \<le> (a - of_nat i) * of_nat k"
using \<open>i < k\<close> by (simp add: algebra_simps zero_less_mult_iff of_nat_diff)
then have "a * of_nat (k - i) \<le> (a - of_nat i) * (of_nat k :: 'a)"
- by (simp only: of_nat_mult[symmetric] of_nat_le_iff)
+ by blast
with assms show ?thesis
using \<open>i < k\<close> by (simp add: field_simps)
qed
- apply (simp add: x zero_le_divide_iff)
- done
+ ultimately show ?thesis
+ unfolding gbinomial_altdef_of_nat
+ by (intro prod_mono) auto
+ qed
finally show ?thesis .
qed
@@ -919,12 +928,16 @@
lemma gbinomial_partial_sum_poly_xpos:
"(\<Sum>k\<le>m. (of_nat m + a gchoose k) * x^k * y^(m-k)) =
- (\<Sum>k\<le>m. (of_nat k + a - 1 gchoose k) * x^k * (x + y)^(m-k))"
- apply (subst gbinomial_partial_sum_poly)
- apply (subst gbinomial_negated_upper)
- apply (intro sum.cong, rule refl)
- apply (simp add: power_mult_distrib [symmetric])
- done
+ (\<Sum>k\<le>m. (of_nat k + a - 1 gchoose k) * x^k * (x + y)^(m-k))" (is "?lhs = ?rhs")
+proof -
+ have "?lhs = (\<Sum>k\<le>m. (- a gchoose k) * (- x) ^ k * (x + y) ^ (m - k))"
+ by (simp add: gbinomial_partial_sum_poly)
+ also have "... = (\<Sum>k\<le>m. (-1) ^ k * (of_nat k - - a - 1 gchoose k) * (- x) ^ k * (x + y) ^ (m - k))"
+ by (metis (no_types, hide_lams) gbinomial_negated_upper)
+ also have "... = ?rhs"
+ by (intro sum.cong) (auto simp flip: power_mult_distrib)
+ finally show ?thesis .
+qed
lemma binomial_r_part_sum: "(\<Sum>k\<le>m. (2 * m + 1 choose k)) = 2 ^ (2 * m)"
proof -
@@ -1012,12 +1025,12 @@
by (subst binomial_fact_lemma [symmetric]) auto
lemma choose_dvd:
- "k \<le> n \<Longrightarrow> fact k * fact (n - k) dvd (fact n :: 'a::linordered_semidom)"
+ assumes "k \<le> n" shows "fact k * fact (n - k) dvd (fact n :: 'a::linordered_semidom)"
unfolding dvd_def
- apply (rule exI [where x="of_nat (n choose k)"])
- using binomial_fact_lemma [of k n, THEN arg_cong [where f = of_nat and 'b='a]]
- apply auto
- done
+proof
+ show "fact n = fact k * fact (n - k) * of_nat (n choose k)"
+ by (metis assms binomial_fact_lemma of_nat_fact of_nat_mult)
+qed
lemma fact_fact_dvd_fact:
"fact k * fact n dvd (fact (k + n) :: 'a::linordered_semidom)"
@@ -1030,11 +1043,14 @@
have "?lhs =
fact (m + r + k) div (fact (m + k) * fact (m + r - m)) * (fact (m + k) div (fact k * fact m))"
by (simp add: binomial_altdef_nat)
- also have "\<dots> = fact (m + r + k) div (fact r * (fact k * fact m))"
+ also have "... = fact (m + r + k) * fact (m + k) div
+ (fact (m + k) * fact (m + r - m) * (fact k * fact m))"
apply (subst div_mult_div_if_dvd)
- apply (auto simp: algebra_simps fact_fact_dvd_fact)
+ apply (auto simp: algebra_simps fact_fact_dvd_fact)
apply (metis add.assoc add.commute fact_fact_dvd_fact)
done
+ also have "\<dots> = fact (m + r + k) div (fact r * (fact k * fact m))"
+ by (auto simp: algebra_simps fact_fact_dvd_fact)
also have "\<dots> = (fact (m + r + k) * fact (m + r)) div (fact r * (fact k * fact m) * fact (m + r))"
apply (subst div_mult_div_if_dvd [symmetric])
apply (auto simp add: algebra_simps)
@@ -1042,9 +1058,7 @@
done
also have "\<dots> =
(fact (m + r + k) div (fact k * fact (m + r)) * (fact (m + r) div (fact r * fact m)))"
- apply (subst div_mult_div_if_dvd)
- apply (auto simp: fact_fact_dvd_fact algebra_simps)
- done
+ by (auto simp: div_mult_div_if_dvd fact_fact_dvd_fact algebra_simps)
finally show ?thesis
by (simp add: binomial_altdef_nat mult.commute)
qed
@@ -1163,17 +1177,13 @@
have 2: "xs \<noteq> [] \<Longrightarrow> sum_list(tl xs) = sum_list xs - hd xs" for xs :: "nat list"
by (auto simp add: neq_Nil_conv)
have f: "bij_betw ?f ?A ?A'"
- apply (rule bij_betw_byWitness[where f' = tl])
- using assms
- apply (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv)
- done
+ by (rule bij_betw_byWitness[where f' = tl]) (use assms in \<open>auto simp: 2 1 simp flip: length_0_conv\<close>)
have 3: "xs \<noteq> [] \<Longrightarrow> hd xs + (sum_list xs - hd xs) = sum_list xs" for xs :: "nat list"
by (metis 1 sum_list_simps(2) 2)
have g: "bij_betw ?g ?B ?B'"
apply (rule bij_betw_byWitness[where f' = "\<lambda>l. (hd l - 1) # tl l"])
using assms
- by (auto simp: 2 length_0_conv[symmetric] intro!: 3
- simp del: length_greater_0_conv length_0_conv)
+ by (auto simp: 2 simp flip: length_0_conv intro!: 3)
have fin: "finite {xs. size xs = M \<and> set xs \<subseteq> {0..<N}}" for M N :: nat
using finite_lists_length_eq[OF finite_atLeastLessThan] conj_commute by auto
have fin_A: "finite ?A" using fin[of _ "N+1"]
--- a/src/HOL/Real_Vector_Spaces.thy Tue Apr 07 17:03:44 2020 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Apr 07 17:03:57 2020 +0200
@@ -62,14 +62,10 @@
and span_raw_def: span = real_vector.span
and extend_basis_raw_def: extend_basis = real_vector.extend_basis
and dim_raw_def: dim = real_vector.dim
- apply unfold_locales
- apply (rule scaleR_add_right)
- apply (rule scaleR_add_left)
- apply (rule scaleR_scaleR)
- apply (rule scaleR_one)
- apply (force simp: linear_def)
- apply (force simp: linear_def real_scaleR_def[abs_def])
- done
+proof unfold_locales
+ show "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear" "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
+ by (force simp: linear_def real_scaleR_def[abs_def])+
+qed (use scaleR_add_right scaleR_add_left scaleR_scaleR scaleR_one in auto)
hide_const (open)\<comment> \<open>locale constants\<close>
real_vector.dependent
@@ -86,9 +82,10 @@
rewrites "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
and "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
defines construct_raw_def: construct = real_vector.construct
- apply unfold_locales
- unfolding linear_def real_scaleR_def
- by (rule refl)+
+proof unfold_locales
+ show "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
+ unfolding linear_def real_scaleR_def by auto
+qed (auto simp: linear_def)
hide_const (open)\<comment> \<open>locale constants\<close>
real_vector.construct
@@ -390,8 +387,7 @@
by (auto simp: Reals_def)
lemma Reals_minus_iff [simp]: "- a \<in> \<real> \<longleftrightarrow> a \<in> \<real>"
- apply (auto simp: Reals_def)
- by (metis add.inverse_inverse of_real_minus rangeI)
+ using Reals_minus by fastforce
lemma Reals_diff [simp]: "a \<in> \<real> \<Longrightarrow> b \<in> \<real> \<Longrightarrow> a - b \<in> \<real>"
by (metis Reals_add Reals_minus_iff add_uminus_conv_diff)
@@ -514,10 +510,8 @@
using that by (simp add: less_le_not_le pos_le_minus_divideR_eq pos_minus_divideR_le_eq)
lemma scaleR_image_atLeastAtMost: "c > 0 \<Longrightarrow> scaleR c ` {x..y} = {c *\<^sub>R x..c *\<^sub>R y}"
- apply (auto intro!: scaleR_left_mono)
- apply (rule_tac x = "inverse c *\<^sub>R xa" in image_eqI)
- apply (simp_all add: pos_le_divideR_eq[symmetric] scaleR_scaleR scaleR_one)
- done
+ apply (auto intro!: scaleR_left_mono simp: image_iff Bex_def)
+ by (meson local.eq_iff pos_divideR_le_eq pos_le_divideR_eq)
end
@@ -1273,13 +1267,12 @@
assume "open S"
then obtain f where "\<forall>x\<in>S. 0 < f x \<and> (\<forall>y. dist y x < f x \<longrightarrow> y \<in> S)"
unfolding open_dist bchoice_iff ..
- then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
+ then have *: "(\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x}) = S" (is "?S = S")
by (fastforce simp: dist_real_def)
- show "generate_topology (range lessThan \<union> range greaterThan) S"
- apply (subst *)
- apply (intro generate_topology_Union generate_topology.Int)
- apply (auto intro: generate_topology.Basis)
- done
+ moreover have "generate_topology (range lessThan \<union> range greaterThan) ?S"
+ by (force intro: generate_topology.Basis generate_topology_Union generate_topology.Int)
+ ultimately show "generate_topology (range lessThan \<union> range greaterThan) S"
+ by simp
next
fix S :: "real set"
assume "generate_topology (range lessThan \<union> range greaterThan) S"
@@ -1548,9 +1541,10 @@
by (simp add: diff_left diff_right)
lemma flip: "bounded_bilinear (\<lambda>x y. y ** x)"
- apply standard
- apply (simp_all add: add_right add_left scaleR_right scaleR_left)
- by (metis bounded mult.commute)
+proof
+ show "\<exists>K. \<forall>a b. norm (b ** a) \<le> norm a * norm b * K"
+ by (metis bounded mult.commute)
+qed (simp_all add: add_right add_left scaleR_right scaleR_left)
lemma comp1:
assumes "bounded_linear g"
@@ -1653,11 +1647,10 @@
qed
lemma bounded_bilinear_mult: "bounded_bilinear ((*) :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
- apply (rule bounded_bilinear.intro)
- apply (auto simp: algebra_simps)
- apply (rule_tac x=1 in exI)
- apply (simp add: norm_mult_ineq)
- done
+proof (rule bounded_bilinear.intro)
+ show "\<exists>K. \<forall>a b::'a. norm (a * b) \<le> norm a * norm b * K"
+ by (rule_tac x=1 in exI) (simp add: norm_mult_ineq)
+qed (auto simp: algebra_simps)
lemma bounded_linear_mult_left: "bounded_linear (\<lambda>x::'a::real_normed_algebra. x * y)"
using bounded_bilinear_mult
@@ -1678,10 +1671,10 @@
unfolding divide_inverse by (rule bounded_linear_mult_left)
lemma bounded_bilinear_scaleR: "bounded_bilinear scaleR"
- apply (rule bounded_bilinear.intro)
- apply (auto simp: algebra_simps)
- apply (rule_tac x=1 in exI, simp)
- done
+proof (rule bounded_bilinear.intro)
+ show "\<exists>K. \<forall>a b. norm (a *\<^sub>R b) \<le> norm a * norm b * K"
+ using less_eq_real_def by auto
+qed (auto simp: algebra_simps)
lemma bounded_linear_scaleR_left: "bounded_linear (\<lambda>r. scaleR r x)"
using bounded_bilinear_scaleR
@@ -1716,11 +1709,11 @@
instance real_normed_algebra_1 \<subseteq> perfect_space
proof
- show "\<not> open {x}" for x :: 'a
- apply (clarsimp simp: open_dist dist_norm)
- apply (rule_tac x = "x + of_real (e/2)" in exI)
- apply simp
- done
+ fix x::'a
+ have "\<And>e. 0 < e \<Longrightarrow> \<exists>y. norm (y - x) < e \<and> y \<noteq> x"
+ by (rule_tac x = "x + of_real (e/2)" in exI) auto
+ then show "\<not> open {x}"
+ by (clarsimp simp: open_dist dist_norm)
qed
@@ -1793,9 +1786,11 @@
qed
lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top"
- apply (clarsimp simp: filterlim_at_top)
- apply (rule_tac c="nat \<lceil>Z + 1\<rceil>" in eventually_sequentiallyI, linarith)
- done
+proof (clarsimp simp: filterlim_at_top)
+ fix Z
+ show "\<forall>\<^sub>F x in sequentially. Z \<le> real x"
+ by (meson eventually_sequentiallyI nat_ceiling_le_eq)
+qed
lemma filterlim_nat_sequentially: "filterlim nat sequentially at_top"
proof -
@@ -1814,17 +1809,20 @@
qed
lemma filterlim_sequentially_iff_filterlim_real:
- "filterlim f sequentially F \<longleftrightarrow> filterlim (\<lambda>x. real (f x)) at_top F"
- apply (rule iffI)
- subgoal using filterlim_compose filterlim_real_sequentially by blast
- subgoal premises prems
+ "filterlim f sequentially F \<longleftrightarrow> filterlim (\<lambda>x. real (f x)) at_top F" (is "?lhs = ?rhs")
+proof
+ assume ?lhs then show ?rhs
+ using filterlim_compose filterlim_real_sequentially by blast
+next
+ assume R: ?rhs
+ show ?lhs
proof -
have "filterlim (\<lambda>x. nat (floor (real (f x)))) sequentially F"
by (intro filterlim_compose[OF filterlim_nat_sequentially]
- filterlim_compose[OF filterlim_floor_sequentially] prems)
+ filterlim_compose[OF filterlim_floor_sequentially] R)
then show ?thesis by simp
qed
- done
+qed
subsubsection \<open>Limits of Sequences\<close>
@@ -1899,10 +1897,8 @@
shows "f \<midarrow>a\<rightarrow> l"
proof -
have "\<And>S. \<lbrakk>open S; l \<in> S; \<forall>\<^sub>F x in at a. g x \<in> S\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in at a. f x \<in> S"
- apply (clarsimp simp add: eventually_at)
- apply (rule_tac x="min d R" in exI)
- apply (auto simp: assms)
- done
+ apply (simp add: eventually_at)
+ by (metis assms(2) assms(3) dual_order.strict_trans linorder_neqE_linordered_idom)
then show ?thesis
using assms by (simp add: tendsto_def)
qed
@@ -2171,16 +2167,19 @@
have "dist (u n) l \<le> dist (u n) ((u \<circ> r) n) + dist ((u \<circ> r) n) l"
by (rule dist_triangle)
also have "\<dots> < e/2 + e/2"
- apply (intro add_strict_mono)
- using N1[of n "r n"] N2[of n] that unfolding comp_def
- by (auto simp: less_imp_le) (meson assms(2) less_imp_le order.trans seq_suble)
+ proof (intro add_strict_mono)
+ show "dist (u n) ((u \<circ> r) n) < e / 2"
+ using N1[of n "r n"] N2[of n] that unfolding comp_def
+ by (meson assms(2) le_trans max.bounded_iff strict_mono_imp_increasing)
+ show "dist ((u \<circ> r) n) l < e / 2"
+ using N2 that by auto
+ qed
finally show ?thesis by simp
qed
then show ?thesis unfolding eventually_sequentially by blast
qed
have "(\<lambda>n. dist (u n) l) \<longlonglongrightarrow> 0"
- apply (rule order_tendstoI)
- using * by auto (meson eventually_sequentiallyI less_le_trans zero_le_dist)
+ by (simp add: less_le_trans * order_tendstoI)
then show ?thesis using tendsto_dist_iff by auto
qed
--- a/src/HOL/Rings.thy Tue Apr 07 17:03:44 2020 +0200
+++ b/src/HOL/Rings.thy Tue Apr 07 17:03:57 2020 +0200
@@ -2255,21 +2255,39 @@
an assumption, but effectively four when the comparison is a goal.
\<close>
-lemma mult_less_cancel_right_disj: "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and> b < a"
- apply (cases "c = 0")
- apply (auto simp add: neq_iff mult_strict_right_mono mult_strict_right_mono_neg)
- apply (auto simp add: not_less not_le [symmetric, of "a*c"] not_le [symmetric, of a])
- apply (erule_tac [!] notE)
- apply (auto simp add: less_imp_le mult_right_mono mult_right_mono_neg)
- done
-
-lemma mult_less_cancel_left_disj: "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and> b < a"
- apply (cases "c = 0")
- apply (auto simp add: neq_iff mult_strict_left_mono mult_strict_left_mono_neg)
- apply (auto simp add: not_less not_le [symmetric, of "c * a"] not_le [symmetric, of a])
- apply (erule_tac [!] notE)
- apply (auto simp add: less_imp_le mult_left_mono mult_left_mono_neg)
- done
+lemma mult_less_cancel_right_disj: "a * c < b * c \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and> b < a"
+proof (cases "c = 0")
+ case False
+ show ?thesis (is "?lhs \<longleftrightarrow> ?rhs")
+ proof
+ assume ?lhs
+ then have "c < 0 \<Longrightarrow> b < a" "c > 0 \<Longrightarrow> b > a"
+ by (auto simp flip: not_le intro: mult_right_mono mult_right_mono_neg)
+ with False show ?rhs
+ by (auto simp add: neq_iff)
+ next
+ assume ?rhs
+ with False show ?lhs
+ by (auto simp add: mult_strict_right_mono mult_strict_right_mono_neg)
+ qed
+qed auto
+
+lemma mult_less_cancel_left_disj: "c * a < c * b \<longleftrightarrow> 0 < c \<and> a < b \<or> c < 0 \<and> b < a"
+proof (cases "c = 0")
+ case False
+ show ?thesis (is "?lhs \<longleftrightarrow> ?rhs")
+ proof
+ assume ?lhs
+ then have "c < 0 \<Longrightarrow> b < a" "c > 0 \<Longrightarrow> b > a"
+ by (auto simp flip: not_le intro: mult_left_mono mult_left_mono_neg)
+ with False show ?rhs
+ by (auto simp add: neq_iff)
+ next
+ assume ?rhs
+ with False show ?lhs
+ by (auto simp add: mult_strict_left_mono mult_strict_left_mono_neg)
+ qed
+qed auto
text \<open>
The ``conjunction of implication'' lemmas produce two cases when the
@@ -2368,29 +2386,29 @@
lemma add_diff_inverse: "\<not> a < b \<Longrightarrow> b + (a - b) = a"
by simp
-lemma add_le_imp_le_diff: "i + k \<le> n \<Longrightarrow> i \<le> n - k"
- apply (subst add_le_cancel_right [where c=k, symmetric])
- apply (frule le_add_diff_inverse2)
- apply (simp only: add.assoc [symmetric])
- using add_implies_diff
- apply fastforce
- done
+lemma add_le_imp_le_diff:
+ assumes "i + k \<le> n" shows "i \<le> n - k"
+proof -
+ have "n - (i + k) + i + k = n"
+ by (simp add: assms add.assoc)
+ with assms add_implies_diff have "i + k \<le> n - k + k"
+ by fastforce
+ then show ?thesis
+ by simp
+qed
lemma add_le_add_imp_diff_le:
assumes 1: "i + k \<le> n"
and 2: "n \<le> j + k"
shows "i + k \<le> n \<Longrightarrow> n \<le> j + k \<Longrightarrow> n - k \<le> j"
proof -
- have "n - (i + k) + (i + k) = n"
- using 1 by simp
+ have "n - (i + k) + i + k = n"
+ using 1 by (simp add: add.assoc)
moreover have "n - k = n - k - i + i"
using 1 by (simp add: add_le_imp_le_diff)
ultimately show ?thesis
- using 2
- apply (simp add: add.assoc [symmetric])
- apply (rule add_le_imp_le_diff [of _ k "j + k", simplified add_diff_cancel_right'])
- apply (simp add: add.commute diff_diff_add)
- done
+ using 2 add_le_imp_le_diff [of "n-k" k "j + k"]
+ by (simp add: add.commute diff_diff_add)
qed
lemma less_1_mult: "1 < m \<Longrightarrow> 1 < n \<Longrightarrow> 1 < m * n"
--- a/src/HOL/Set_Interval.thy Tue Apr 07 17:03:44 2020 +0200
+++ b/src/HOL/Set_Interval.thy Tue Apr 07 17:03:57 2020 +0200
@@ -812,10 +812,10 @@
greaterThanLessThan_def)
lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}"
-by (auto simp add: atLeastAtMost_def)
+ by auto
lemma atLeastAtMost_insertL: "m \<le> n \<Longrightarrow> insert m {Suc m..n} = {m ..n}"
-by auto
+ by auto
text \<open>The analogous result is useful on \<^typ>\<open>int\<close>:\<close>
(* here, because we don't have an own int section *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/delay.scala Tue Apr 07 17:03:57 2020 +0200
@@ -0,0 +1,66 @@
+/* Title: Pure/Concurrent/delay.scala
+ Author: Makarius
+
+Delayed events.
+*/
+
+package isabelle
+
+
+object Delay
+{
+ // delayed event after first invocation
+ def first(delay: => Time, log: Logger = No_Logger, gui: Boolean = false)(event: => Unit): Delay =
+ new Delay(true, delay, log, if (gui) GUI_Thread.later { event } else event )
+
+ // delayed event after last invocation
+ def last(delay: => Time, log: Logger = No_Logger, gui: Boolean = false)(event: => Unit): Delay =
+ new Delay(false, delay, log, if (gui) GUI_Thread.later { event } else event )
+}
+
+final class Delay private(first: Boolean, delay: => Time, log: Logger, event: => Unit)
+{
+ private var running: Option[Event_Timer.Request] = None
+
+ private def run: Unit =
+ {
+ val do_run = synchronized {
+ if (running.isDefined) { running = None; true } else false
+ }
+ if (do_run) {
+ try { event }
+ catch { case exn: Throwable if !Exn.is_interrupt(exn) => log(Exn.message(exn)); throw exn }
+ }
+ }
+
+ def invoke(): Unit = synchronized
+ {
+ val new_run =
+ running match {
+ case Some(request) => if (first) false else { request.cancel; true }
+ case None => true
+ }
+ if (new_run)
+ running = Some(Event_Timer.request(Time.now() + delay)(run))
+ }
+
+ def revoke(): Unit = synchronized
+ {
+ running match {
+ case Some(request) => request.cancel; running = None
+ case None =>
+ }
+ }
+
+ def postpone(alt_delay: Time): Unit = synchronized
+ {
+ running match {
+ case Some(request) =>
+ val alt_time = Time.now() + alt_delay
+ if (request.time < alt_time && request.cancel) {
+ running = Some(Event_Timer.request(alt_time)(run))
+ }
+ case None =>
+ }
+ }
+}
--- a/src/Pure/Concurrent/isabelle_thread.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.scala Tue Apr 07 17:03:57 2020 +0200
@@ -12,7 +12,19 @@
object Isabelle_Thread
{
- /* fork */
+ /* self-thread */
+
+ def self: Isabelle_Thread =
+ Thread.currentThread match {
+ case thread: Isabelle_Thread => thread
+ case thread => error("Isabelle-specific thread required: " + thread)
+ }
+
+ def check_self: Boolean =
+ Thread.currentThread.isInstanceOf[Isabelle_Thread]
+
+
+ /* create threads */
private val counter = Counter.make()
@@ -21,6 +33,18 @@
def current_thread_group: ThreadGroup = Thread.currentThread.getThreadGroup
+ def create(
+ main: Runnable,
+ name: String = "",
+ group: ThreadGroup = current_thread_group,
+ pri: Int = Thread.NORM_PRIORITY,
+ daemon: Boolean = false,
+ inherit_locals: Boolean = false): Isabelle_Thread =
+ {
+ new Isabelle_Thread(main, name = make_name(name = name), group = group,
+ pri = pri, daemon = daemon, inherit_locals = inherit_locals)
+ }
+
def fork(
name: String = "",
group: ThreadGroup = current_thread_group,
@@ -29,108 +53,71 @@
inherit_locals: Boolean = false,
uninterruptible: Boolean = false)(body: => Unit): Isabelle_Thread =
{
- val main =
- if (uninterruptible) new Runnable { override def run { Isabelle_Thread.uninterruptible { body } } }
- else new Runnable { override def run { body } }
+ val main: Runnable =
+ if (uninterruptible) { () => Isabelle_Thread.uninterruptible { body } }
+ else { () => body }
val thread =
- new Isabelle_Thread(main, name = make_name(name = name), group = group,
- pri = pri, daemon = daemon, inherit_locals = inherit_locals)
+ create(main, name = name, group = group, pri = pri,
+ daemon = daemon, inherit_locals = inherit_locals)
thread.start
thread
}
- /* self */
-
- def self: Isabelle_Thread =
- Thread.currentThread match {
- case thread: Isabelle_Thread => thread
- case _ => error("Isabelle-specific thread required")
- }
-
- def uninterruptible[A](body: => A): A = self.uninterruptible(body)
-
-
- /* pool */
+ /* thread pool */
lazy val pool: ThreadPoolExecutor =
- {
- val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
- val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
- val executor =
- new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
- executor.setThreadFactory(
- new Isabelle_Thread(_, name = make_name(base = "worker"), group = current_thread_group))
- executor
- }
+ {
+ val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
+ val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
+ val executor =
+ new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
+ executor.setThreadFactory(create(_, name = make_name(base = "worker"), group = current_thread_group))
+ executor
+ }
- /* delayed events */
-
- final class Delay private[Isabelle_Thread](
- first: Boolean, delay: => Time, log: Logger, event: => Unit)
- {
- private var running: Option[Event_Timer.Request] = None
+ /* interrupt handlers */
- private def run: Unit =
- {
- val do_run = synchronized {
- if (running.isDefined) { running = None; true } else false
- }
- if (do_run) {
- try { event }
- catch { case exn: Throwable if !Exn.is_interrupt(exn) => log(Exn.message(exn)); throw exn }
- }
- }
+ object Interrupt_Handler
+ {
+ def apply(handle: Isabelle_Thread => Unit, name: String = "handler"): Interrupt_Handler =
+ new Interrupt_Handler(handle, name)
+
+ val interruptible: Interrupt_Handler =
+ Interrupt_Handler(_.raise_interrupt, name = "interruptible")
- def invoke(): Unit = synchronized
- {
- val new_run =
- running match {
- case Some(request) => if (first) false else { request.cancel; true }
- case None => true
- }
- if (new_run)
- running = Some(Event_Timer.request(Time.now() + delay)(run))
- }
+ val uninterruptible: Interrupt_Handler =
+ Interrupt_Handler(_.postpone_interrupt, name = "uninterruptible")
+ }
- def revoke(): Unit = synchronized
- {
- running match {
- case Some(request) => request.cancel; running = None
- case None =>
- }
- }
-
- def postpone(alt_delay: Time): Unit = synchronized
- {
- running match {
- case Some(request) =>
- val alt_time = Time.now() + alt_delay
- if (request.time < alt_time && request.cancel) {
- running = Some(Event_Timer.request(alt_time)(run))
- }
- case None =>
- }
- }
+ class Interrupt_Handler private(handle: Isabelle_Thread => Unit, name: String)
+ extends Function[Isabelle_Thread, Unit]
+ {
+ def apply(thread: Isabelle_Thread) { handle(thread) }
+ override def toString: String = name
}
- // delayed event after first invocation
- def delay_first(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay =
- new Delay(true, delay, log, event)
+ def interrupt_handler[A](handler: Interrupt_Handler)(body: => A): A =
+ if (handler == null) body
+ else self.interrupt_handler(handler)(body)
+
+ def interrupt_handler[A](handle: Isabelle_Thread => Unit)(body: => A): A =
+ self.interrupt_handler(Interrupt_Handler(handle))(body)
- // delayed event after last invocation
- def delay_last(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay =
- new Delay(false, delay, log, event)
+ def interruptible[A](body: => A): A =
+ interrupt_handler(Interrupt_Handler.interruptible)(body)
+
+ def uninterruptible[A](body: => A): A =
+ interrupt_handler(Interrupt_Handler.uninterruptible)(body)
+
+ def try_uninterruptible[A](body: => A): A =
+ if (check_self) interrupt_handler(Interrupt_Handler.uninterruptible)(body)
+ else body
}
-class Isabelle_Thread private(
- main: Runnable,
- name: String = "",
- group: ThreadGroup = null,
- pri: Int = Thread.NORM_PRIORITY,
- daemon: Boolean = false,
- inherit_locals: Boolean = false)
+class Isabelle_Thread private(main: Runnable, name: String, group: ThreadGroup,
+ pri: Int, daemon: Boolean, inherit_locals: Boolean)
extends Thread(group, null, name, 0L, inherit_locals)
{
thread =>
@@ -140,30 +127,56 @@
override def run { main.run() }
- private var interruptible: Boolean = true
- private var interrupt_pending: Boolean = false
+ def is_self: Boolean = Thread.currentThread == thread
+
+
+ /* interrupt state */
+
+ // synchronized, with concurrent changes
+ private var interrupt_postponed: Boolean = false
- override def interrupt: Unit = synchronized
+ def clear_interrupt: Boolean = synchronized
{
- if (interruptible) super.interrupt()
- else { interrupt_pending = true }
+ val was_interrupted = isInterrupted || interrupt_postponed
+ Exn.Interrupt.dispose()
+ interrupt_postponed = false
+ was_interrupted
+ }
+
+ def raise_interrupt: Unit = synchronized
+ {
+ interrupt_postponed = false
+ super.interrupt()
}
- def uninterruptible[A](body: => A): A =
+ def postpone_interrupt: Unit = synchronized
{
- require(Thread.currentThread == thread)
+ interrupt_postponed = true
+ Exn.Interrupt.dispose()
+ }
+
+
+ /* interrupt handler */
+
+ // non-synchronized, only changed on self-thread
+ @volatile private var handler = Isabelle_Thread.Interrupt_Handler.interruptible
+
+ override def interrupt: Unit = handler(thread)
- val interruptible0 = synchronized { val b = interruptible; interruptible = false; b }
- try { body }
- finally {
- synchronized {
- interruptible = interruptible0
- if (interruptible && interrupt_pending) {
- interrupt_pending = false
- super.interrupt()
- }
+ def interrupt_handler[A](new_handler: Isabelle_Thread.Interrupt_Handler)(body: => A): A =
+ if (new_handler == null) body
+ else {
+ require(is_self)
+
+ val old_handler = handler
+ handler = new_handler
+ try {
+ if (clear_interrupt) interrupt
+ body
}
- Exn.Interrupt.expose()
+ finally {
+ handler = old_handler
+ if (clear_interrupt) interrupt
+ }
}
- }
}
--- a/src/Pure/GUI/gui_thread.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Pure/GUI/gui_thread.scala Tue Apr 07 17:03:57 2020 +0200
@@ -16,13 +16,13 @@
def assert[A](body: => A): A =
{
- Predef.assert(SwingUtilities.isEventDispatchThread())
+ Predef.assert(SwingUtilities.isEventDispatchThread)
body
}
def require[A](body: => A): A =
{
- Predef.require(SwingUtilities.isEventDispatchThread())
+ Predef.require(SwingUtilities.isEventDispatchThread)
body
}
@@ -31,36 +31,27 @@
def now[A](body: => A): A =
{
- if (SwingUtilities.isEventDispatchThread()) body
+ if (SwingUtilities.isEventDispatchThread) body
else {
- lazy val result = { assert { Exn.capture(body) } }
- SwingUtilities.invokeAndWait(new Runnable { def run = result })
+ lazy val result = assert { Exn.capture(body) }
+ SwingUtilities.invokeAndWait(() => result)
Exn.release(result)
}
}
def later(body: => Unit)
{
- if (SwingUtilities.isEventDispatchThread()) body
- else SwingUtilities.invokeLater(new Runnable { def run = body })
+ if (SwingUtilities.isEventDispatchThread) body
+ else SwingUtilities.invokeLater(() => body)
}
def future[A](body: => A): Future[A] =
{
- if (SwingUtilities.isEventDispatchThread()) Future.value(body)
+ if (SwingUtilities.isEventDispatchThread) Future.value(body)
else {
val promise = Future.promise[A]
later { promise.fulfill_result(Exn.capture(body)) }
promise
}
}
-
-
- /* delayed events */
-
- def delay_first(delay: => Time)(event: => Unit): Isabelle_Thread.Delay =
- Isabelle_Thread.delay_first(delay) { later { event } }
-
- def delay_last(delay: => Time)(event: => Unit): Isabelle_Thread.Delay =
- Isabelle_Thread.delay_last(delay) { later { event } }
}
--- a/src/Pure/General/exn.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Pure/General/exn.scala Tue Apr 07 17:03:57 2020 +0200
@@ -96,22 +96,10 @@
def apply(): Throwable = new InterruptedException
def unapply(exn: Throwable): Boolean = is_interrupt(exn)
+ def dispose() { Thread.interrupted }
def expose() { if (Thread.interrupted) throw apply() }
def impose() { Thread.currentThread.interrupt }
- def postpone[A](body: => A): Option[A] =
- {
- val interrupted = Thread.interrupted
- val result = capture { body }
- if (interrupted) impose()
- result match {
- case Res(x) => Some(x)
- case Exn(e) =>
- if (is_interrupt(e)) { impose(); None }
- else throw e
- }
- }
-
val return_code = 130
}
--- a/src/Pure/General/file_watcher.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Pure/General/file_watcher.scala Tue Apr 07 17:03:57 2020 +0200
@@ -84,7 +84,7 @@
/* changed directory entries */
- private val delay_changed = Isabelle_Thread.delay_last(delay)
+ private val delay_changed = Delay.last(delay)
{
val changed = state.change_result(st => (st.changed, st.copy(changed = Set.empty)))
handle(changed)
--- a/src/Pure/ML/ml_console.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Pure/ML/ml_console.scala Tue Apr 07 17:03:57 2020 +0200
@@ -74,16 +74,11 @@
else Some(Sessions.base_info(
options, logic, dirs = dirs, include_sessions = include_sessions).check_base))
- val tty_loop = new TTY_Loop(process.stdin, process.stdout, Some(process.interrupt _))
- val process_result = Future.thread[Int]("process_result") {
+ POSIX_Interrupt.handler { process.interrupt } {
+ new TTY_Loop(process.stdin, process.stdout).join
val rc = process.join
- tty_loop.cancel // FIXME does not quite work, cannot interrupt blocking read on System.in
- rc
+ if (rc != 0) sys.exit(rc)
}
- tty_loop.join
-
- val rc = process_result.join
- if (rc != 0) sys.exit(rc)
}
}
}
--- a/src/Pure/PIDE/headless.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Pure/PIDE/headless.scala Tue Apr 07 17:03:57 2020 +0200
@@ -304,12 +304,12 @@
val consumer =
{
val delay_nodes_status =
- Isabelle_Thread.delay_first(nodes_status_delay max Time.zero) {
+ Delay.first(nodes_status_delay max Time.zero) {
progress.nodes_status(use_theories_state.value.nodes_status)
}
val delay_commit_clean =
- Isabelle_Thread.delay_first(commit_cleanup_delay max Time.zero) {
+ Delay.first(commit_cleanup_delay max Time.zero) {
val clean_theories = use_theories_state.change_result(_.clean_theories)
if (clean_theories.nonEmpty) {
progress.echo("Removing " + clean_theories.length + " theories ...")
--- a/src/Pure/PIDE/session.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Pure/PIDE/session.scala Tue Apr 07 17:03:57 2020 +0200
@@ -268,7 +268,7 @@
nodes = Set.empty
commands = Set.empty
}
- private val delay_flush = Isabelle_Thread.delay_first(output_delay) { flush() }
+ private val delay_flush = Delay.first(output_delay) { flush() }
def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit =
synchronized {
@@ -313,7 +313,7 @@
private object consolidation
{
private val delay =
- Isabelle_Thread.delay_first(consolidate_delay) { manager.send(Consolidate_Execution) }
+ Delay.first(consolidate_delay) { manager.send(Consolidate_Execution) }
private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty)
private val state = Synchronized(init_state)
@@ -382,7 +382,7 @@
/* manager thread */
private val delay_prune =
- Isabelle_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
+ Delay.first(prune_delay) { manager.send(Prune_History) }
private val manager: Consumer_Thread[Any] =
{
--- a/src/Pure/System/bash.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Pure/System/bash.scala Tue Apr 07 17:03:57 2020 +0200
@@ -10,6 +10,8 @@
import java.io.{File => JFile, BufferedReader, InputStreamReader,
BufferedWriter, OutputStreamWriter}
+import scala.annotation.tailrec
+
object Bash
{
@@ -100,41 +102,36 @@
private val pid = stdout.readLine
- def interrupt()
- { Exn.Interrupt.postpone { Isabelle_System.kill("INT", pid) } }
-
- private def kill(signal: String): Boolean =
- Exn.Interrupt.postpone {
- Isabelle_System.kill(signal, pid)
- Isabelle_System.kill("0", pid)._2 == 0 } getOrElse true
-
- private def multi_kill(signal: String): Boolean =
+ @tailrec private def kill(signal: String, count: Int = 1): Boolean =
{
- var running = true
- var count = 10
- while (running && count > 0) {
- if (kill(signal)) {
- Exn.Interrupt.postpone {
- Time.seconds(0.1).sleep
- count -= 1
- }
+ count <= 0 ||
+ {
+ Isabelle_System.kill(signal, pid)
+ val running = Isabelle_System.kill("0", pid)._2 == 0
+ if (running) {
+ Time.seconds(0.1).sleep
+ kill(signal, count - 1)
}
- else running = false
+ else false
}
- running
}
- def terminate()
+ def terminate(): Unit = Isabelle_Thread.try_uninterruptible
{
- multi_kill("INT") && multi_kill("TERM") && kill("KILL")
+ kill("INT", count = 7) && kill("TERM", count = 3) && kill("KILL")
proc.destroy
do_cleanup()
}
+ def interrupt(): Unit = Isabelle_Thread.try_uninterruptible
+ {
+ Isabelle_System.kill("INT", pid)
+ }
+
// JVM shutdown hook
- private val shutdown_hook = new Thread { override def run = terminate() }
+ private val shutdown_hook = Isabelle_Thread.create(() => terminate())
try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
catch { case _: IllegalStateException => }
--- a/src/Pure/System/isabelle_process.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Pure/System/isabelle_process.scala Tue Apr 07 17:03:57 2020 +0200
@@ -76,4 +76,6 @@
session.stop()
result
}
+
+ def terminate { process.terminate }
}
--- a/src/Pure/System/isabelle_system.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Pure/System/isabelle_system.scala Tue Apr 07 17:03:57 2020 +0200
@@ -287,7 +287,7 @@
proc.getInputStream.close
proc.getErrorStream.close
proc.destroy
- Thread.interrupted
+ Exn.Interrupt.dispose()
}
(output, rc)
}
--- a/src/Pure/System/tty_loop.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Pure/System/tty_loop.scala Tue Apr 07 17:03:57 2020 +0200
@@ -10,13 +10,14 @@
import java.io.{IOException, Writer, Reader, InputStreamReader, BufferedReader}
-class TTY_Loop(writer: Writer, reader: Reader,
- writer_lock: AnyRef = new Object,
- interrupt: Option[() => Unit] = None)
+class TTY_Loop(
+ writer: Writer,
+ reader: Reader,
+ writer_lock: AnyRef = new Object)
{
- private val console_output = Future.thread[Unit]("console_output") {
+ private val console_output = Future.thread[Unit]("console_output", uninterruptible = true) {
try {
- var result = new StringBuilder(100)
+ val result = new StringBuilder(100)
var finished = false
while (!finished) {
var c = -1
@@ -40,32 +41,25 @@
catch { case e: IOException => case Exn.Interrupt() => }
}
- private val console_input = Future.thread[Unit]("console_input") {
+ private val console_input = Future.thread[Unit]("console_input", uninterruptible = true) {
val console_reader = new BufferedReader(new InputStreamReader(System.in))
- def body
- {
- try {
- var finished = false
- while (!finished) {
- console_reader.readLine() match {
- case null =>
- writer.close()
- finished = true
- case line =>
- writer_lock.synchronized {
- writer.write(line)
- writer.write("\n")
- writer.flush()
- }
- }
+ try {
+ var finished = false
+ while (!finished) {
+ console_reader.readLine() match {
+ case null =>
+ writer.close()
+ finished = true
+ case line =>
+ writer_lock.synchronized {
+ writer.write(line)
+ writer.write("\n")
+ writer.flush()
+ }
}
}
- catch { case e: IOException => case Exn.Interrupt() => }
}
- interrupt match {
- case None => body
- case Some(int) => POSIX_Interrupt.handler { int() } { body }
- }
+ catch { case e: IOException => case Exn.Interrupt() => }
}
def join { console_output.join; console_input.join }
--- a/src/Pure/Tools/build.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Pure/Tools/build.scala Tue Apr 07 17:03:57 2020 +0200
@@ -174,7 +174,7 @@
Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache)
private val future_result: Future[Process_Result] =
- Future.thread("build") {
+ Future.thread("build", uninterruptible = true) {
val parent = info.parent.getOrElse("")
val base = deps(parent)
val args_yxml =
@@ -321,14 +321,17 @@
cwd = info.dir.file, env = env)
val errors =
- Exn.capture { process.await_startup } match {
- case Exn.Res(_) =>
- session.protocol_command("build_session", args_yxml)
- build_session_errors.join
- case Exn.Exn(exn) => List(Exn.message(exn))
+ Isabelle_Thread.interrupt_handler(_ => process.terminate) {
+ Exn.capture { process.await_startup } match {
+ case Exn.Res(_) =>
+ session.protocol_command("build_session", args_yxml)
+ build_session_errors.join_result
+ case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn)))
+ }
}
- val process_result = process.await_shutdown
+ val process_result =
+ Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown }
val process_output =
stdout.toString :: messages.toList :::
command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
@@ -337,11 +340,16 @@
task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply)
val result = process_result.output(process_output)
- if (errors.isEmpty) result
- else {
- result.error_rc.output(
- errors.flatMap(s => split_lines(Output.error_message_text(s))) :::
- errors.map(Protocol.Error_Message_Marker.apply))
+
+ errors match {
+ case Exn.Res(Nil) => result
+ case Exn.Res(errs) =>
+ result.error_rc.output(
+ errs.flatMap(s => split_lines(Output.error_message_text(s))) :::
+ errs.map(Protocol.Error_Message_Marker.apply))
+ case Exn.Exn(Exn.Interrupt()) =>
+ if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result
+ case Exn.Exn(exn) => throw exn
}
}
else {
@@ -358,28 +366,30 @@
use_prelude = use_prelude, eval_main = eval_main,
cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
- process.result(
- progress_stdout =
- {
- case Protocol.Loading_Theory_Marker(theory) =>
- progress.theory(Progress.Theory(theory, session = session_name))
- case Protocol.Export.Marker((args, path)) =>
- val body =
- try { Bytes.read(path) }
- catch {
- case ERROR(msg) =>
- error("Failed to read export " + quote(args.compound_name) + "\n" + msg)
- }
- path.file.delete
- export_consumer(session_name, args, body)
- case _ =>
- },
- progress_limit =
- options.int("process_output_limit") match {
- case 0 => None
- case m => Some(m * 1000000L)
- },
- strict = false)
+ Isabelle_Thread.interrupt_handler(_ => process.terminate) {
+ process.result(
+ progress_stdout =
+ {
+ case Protocol.Loading_Theory_Marker(theory) =>
+ progress.theory(Progress.Theory(theory, session = session_name))
+ case Protocol.Export.Marker((args, path)) =>
+ val body =
+ try { Bytes.read(path) }
+ catch {
+ case ERROR(msg) =>
+ error("Failed to read export " + quote(args.compound_name) + "\n" + msg)
+ }
+ path.file.delete
+ export_consumer(session_name, args, body)
+ case _ =>
+ },
+ progress_limit =
+ options.int("process_output_limit") match {
+ case 0 => None
+ case m => Some(m * 1000000L)
+ },
+ strict = false)
+ }
}
}
--- a/src/Pure/Tools/debugger.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Pure/Tools/debugger.scala Tue Apr 07 17:03:57 2020 +0200
@@ -155,7 +155,7 @@
private val state = Synchronized(Debugger.State())
private val delay_update =
- Isabelle_Thread.delay_first(session.output_delay) {
+ Delay.first(session.output_delay) {
session.debugger_updates.post(Debugger.Update)
}
--- a/src/Pure/Tools/server.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Pure/Tools/server.scala Tue Apr 07 17:03:57 2020 +0200
@@ -173,12 +173,11 @@
private val out = new BufferedOutputStream(socket.getOutputStream)
private val out_lock: AnyRef = new Object
- def tty_loop(interrupt: Option[() => Unit] = None): TTY_Loop =
+ def tty_loop(): TTY_Loop =
new TTY_Loop(
new OutputStreamWriter(out),
new InputStreamReader(in),
- writer_lock = out_lock,
- interrupt = interrupt)
+ writer_lock = out_lock)
def read_password(password: String): Boolean =
try { Byte_Message.read_line(in).map(_.text) == Some(password) }
@@ -491,7 +490,7 @@
if (operation_list) {
for {
- server_info <- using(SQLite.open_database(Data.database))(list(_))
+ server_info <- using(SQLite.open_database(Data.database))(list)
if server_info.active
} Output.writeln(server_info.toString, stdout = true)
}
--- a/src/Pure/build-jars Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Pure/build-jars Tue Apr 07 17:03:57 2020 +0200
@@ -28,6 +28,7 @@
src/Pure/Admin/other_isabelle.scala
src/Pure/Concurrent/consumer_thread.scala
src/Pure/Concurrent/counter.scala
+ src/Pure/Concurrent/delay.scala
src/Pure/Concurrent/event_timer.scala
src/Pure/Concurrent/future.scala
src/Pure/Concurrent/isabelle_thread.scala
--- a/src/Tools/Graphview/tree_panel.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/Graphview/tree_panel.scala Tue Apr 07 17:03:57 2020 +0200
@@ -112,7 +112,7 @@
private val selection_field_foreground = selection_field.foreground
private val selection_delay =
- GUI_Thread.delay_last(graphview.options.seconds("editor_input_delay")) {
+ Delay.last(graphview.options.seconds("editor_input_delay"), gui = true) {
val (pattern, ok) =
selection_field.text match {
case null | "" => (None, true)
--- a/src/Tools/VSCode/src/server.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/VSCode/src/server.scala Tue Apr 07 17:03:57 2020 +0200
@@ -127,12 +127,12 @@
/* input from client or file-system */
- private val delay_input: Isabelle_Thread.Delay =
- Isabelle_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
+ private val delay_input: Delay =
+ Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger)
{ resources.flush_input(session, channel) }
- private val delay_load: Isabelle_Thread.Delay =
- Isabelle_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
+ private val delay_load: Delay =
+ Delay.last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
val (invoke_input, invoke_load) =
resources.resolve_dependencies(session, editor, file_watcher)
if (invoke_input) delay_input.invoke()
@@ -183,8 +183,8 @@
/* caret handling */
- private val delay_caret_update: Isabelle_Thread.Delay =
- Isabelle_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
+ private val delay_caret_update: Delay =
+ Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger)
{ session.caret_focus.post(Session.Caret_Focus) }
private def update_caret(caret: Option[(JFile, Line.Position)])
@@ -199,8 +199,8 @@
private lazy val preview_panel = new Preview_Panel(resources)
- private lazy val delay_preview: Isabelle_Thread.Delay =
- Isabelle_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
+ private lazy val delay_preview: Delay =
+ Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger)
{
if (preview_panel.flush(channel)) delay_preview.invoke()
}
@@ -214,8 +214,8 @@
/* output to client */
- private val delay_output: Isabelle_Thread.Delay =
- Isabelle_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
+ private val delay_output: Delay =
+ Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger)
{
if (resources.flush_output(channel)) delay_output.invoke()
}
--- a/src/Tools/jEdit/src/completion_popup.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Tue Apr 07 17:03:57 2020 +0200
@@ -373,7 +373,7 @@
}
private val input_delay =
- GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
+ Delay.last(PIDE.options.seconds("jedit_completion_delay"), gui = true) {
action()
}
@@ -530,7 +530,7 @@
}
private val process_delay =
- GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
+ Delay.last(PIDE.options.seconds("jedit_completion_delay"), gui = true) {
action()
}
--- a/src/Tools/jEdit/src/debugger_dockable.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Tue Apr 07 17:03:57 2020 +0200
@@ -362,7 +362,7 @@
/* resize */
private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/document_view.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Tue Apr 07 17:03:57 2020 +0200
@@ -184,7 +184,7 @@
/* caret handling */
private val delay_caret_update =
- GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
+ Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) {
session.caret_focus.post(Session.Caret_Focus)
JEdit_Lib.invalidate(text_area)
}
--- a/src/Tools/jEdit/src/font_info.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/font_info.scala Tue Apr 07 17:03:57 2020 +0200
@@ -56,7 +56,7 @@
// owned by GUI thread
private var steps = 0
- private val delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
+ private val delay = Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true)
{
change_size(size =>
{
--- a/src/Tools/jEdit/src/info_dockable.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala Tue Apr 07 17:03:57 2020 +0200
@@ -80,7 +80,7 @@
/* resize */
private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/jedit_editor.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Apr 07 17:03:57 2020 +0200
@@ -32,10 +32,10 @@
def purge() { flush_edits(purge = true) }
private val delay1_flush =
- GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
+ Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { flush() }
private val delay2_flush =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_generated_input_delay")) { flush() }
+ Delay.first(PIDE.options.seconds("editor_generated_input_delay"), gui = true) { flush() }
def invoke(): Unit = delay1_flush.invoke()
def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
--- a/src/Tools/jEdit/src/monitor_dockable.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Tue Apr 07 17:03:57 2020 +0200
@@ -59,10 +59,10 @@
}
private val input_delay =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_input_delay")) { update_chart }
+ Delay.first(PIDE.options.seconds("editor_input_delay"), gui = true) { update_chart }
private val update_delay =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { update_chart }
+ Delay.first(PIDE.options.seconds("editor_chart_delay"), gui = true) { update_chart }
/* controls */
--- a/src/Tools/jEdit/src/output_dockable.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Tue Apr 07 17:03:57 2020 +0200
@@ -151,7 +151,7 @@
/* resize */
private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/plugin.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Tue Apr 07 17:03:57 2020 +0200
@@ -107,7 +107,7 @@
/* theory files */
lazy val delay_init =
- GUI_Thread.delay_last(options.seconds("editor_load_delay"))
+ Delay.last(options.seconds("editor_load_delay"), gui = true)
{
init_models()
}
@@ -178,7 +178,7 @@
}
private lazy val delay_load =
- GUI_Thread.delay_last(options.seconds("editor_load_delay")) { delay_load_action() }
+ Delay.last(options.seconds("editor_load_delay"), gui = true) { delay_load_action() }
private def file_watcher_action(changed: Set[JFile]): Unit =
if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
--- a/src/Tools/jEdit/src/pretty_text_area.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Tue Apr 07 17:03:57 2020 +0200
@@ -191,7 +191,7 @@
Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search")
{
private val input_delay =
- GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
+ Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) {
search_action(this)
}
getDocument.addDocumentListener(new DocumentListener {
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Tue Apr 07 17:03:57 2020 +0200
@@ -77,7 +77,7 @@
private var active = true
private val pending_delay =
- GUI_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
+ Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) {
pending match {
case Some(body) => pending = None; body()
case None =>
@@ -99,7 +99,7 @@
}
private lazy val reactivate_delay =
- GUI_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
+ Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) {
active = true
}
@@ -113,7 +113,7 @@
/* dismiss */
- private lazy val focus_delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
+ private lazy val focus_delay = Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true)
{
dismiss_unfocused()
}
--- a/src/Tools/jEdit/src/query_dockable.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala Tue Apr 07 17:03:57 2020 +0200
@@ -320,7 +320,7 @@
}
private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/scala_console.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala Tue Apr 07 17:03:57 2020 +0200
@@ -152,7 +152,7 @@
}
finally {
running.change(_ => None)
- Thread.interrupted
+ Exn.Interrupt.dispose()
}
GUI_Thread.later {
if (err != null) err.commandDone()
--- a/src/Tools/jEdit/src/session_build.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/session_build.scala Tue Apr 07 17:03:57 2020 +0200
@@ -102,7 +102,7 @@
}
private val delay_exit =
- GUI_Thread.delay_first(Time.seconds(1.0))
+ Delay.first(Time.seconds(1.0), gui = true)
{
if (can_auto_close) conclude()
else {
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Apr 07 17:03:57 2020 +0200
@@ -144,7 +144,7 @@
/* resize */
private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Apr 07 17:03:57 2020 +0200
@@ -182,7 +182,7 @@
/* resize */
private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
peer.addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Tue Apr 07 17:03:57 2020 +0200
@@ -58,7 +58,7 @@
/* resize */
private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/state_dockable.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala Tue Apr 07 17:03:57 2020 +0200
@@ -40,7 +40,7 @@
/* resize */
private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/symbols_dockable.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Tue Apr 07 17:03:57 2020 +0200
@@ -28,7 +28,7 @@
private val abbrevs_panel = new Abbrevs_Panel
private val abbrevs_refresh_delay =
- GUI_Thread.delay_last(PIDE.options.seconds("editor_update_delay")) { abbrevs_panel.refresh }
+ Delay.last(PIDE.options.seconds("editor_update_delay"), gui = true) { abbrevs_panel.refresh }
private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button
{
@@ -129,7 +129,7 @@
val search_space = for ((sym, _) <- Symbol.codes) yield (sym, Word.lowercase(sym))
val search_delay =
- GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
+ Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) {
val search_words = Word.explode(Word.lowercase(search_field.text))
val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0
val results =
--- a/src/Tools/jEdit/src/syslog_dockable.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Tue Apr 07 17:03:57 2020 +0200
@@ -21,7 +21,7 @@
private val syslog = new TextArea()
- private def syslog_delay = GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay"))
+ private def syslog_delay = Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true)
{
val text = PIDE.session.syslog_content()
if (text != syslog.text) syslog.text = text
--- a/src/Tools/jEdit/src/text_overview.scala Tue Apr 07 17:03:44 2020 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala Tue Apr 07 17:03:57 2020 +0200
@@ -75,7 +75,7 @@
private var current_overview = Overview()
private val delay_repaint =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { repaint() }
override def paintComponent(gfx: Graphics)
{
@@ -116,7 +116,7 @@
def revoke(): Unit = { delay_refresh.revoke(); future_refresh.change(x => { x.cancel; x }) }
private val delay_refresh =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) {
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) {
if (!doc_view.rich_text_area.check_robust_body) invoke()
else {
JEdit_Lib.buffer_lock(buffer) {