--- a/NEWS Fri Dec 23 11:12:19 2022 +0000
+++ b/NEWS Sat Dec 24 15:35:43 2022 +0000
@@ -43,17 +43,26 @@
antisymp to be abbreviations. Lemmas antisym_def and antisymp_def are
explicitly provided for backward compatibility but their usage is
discouraged. Minor INCOMPATIBILITY.
+ - Added predicates trans_on and transp_on and redefined trans and transp to
+ be abbreviations. Lemmas trans_def and transp_def are explicitly provided
+ for backward compatibility but their usage is discouraged.
+ Minor INCOMPATIBILITY.
- Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
+ antisym_converse[simp] ~> antisym_on_converse[simp]
order.antisymp_ge[simp] ~> order.antisymp_on_ge[simp]
order.antisymp_le[simp] ~> order.antisymp_on_le[simp]
preorder.asymp_greater[simp] ~> preorder.asymp_on_greater[simp]
preorder.asymp_less[simp] ~> preorder.asymp_on_less[simp]
preorder.irreflp_greater[simp] ~> preorder.irreflp_on_greater[simp]
preorder.irreflp_less[simp] ~> preorder.irreflp_on_less[simp]
+ preorder.transp_ge[simp] ~> preorder.transp_on_ge[simp]
+ preorder.transp_gr[simp] ~> preorder.transp_on_greater[simp]
+ preorder.transp_le[simp] ~> preorder.transp_on_le[simp]
+ preorder.transp_less[simp] ~> preorder.transp_on_less[simp]
reflp_equality[simp] ~> reflp_on_equality[simp]
+ sym_converse[simp] ~> sym_on_converse[simp]
total_on_singleton
- sym_converse[simp] ~> sym_on_converse[simp]
- antisym_converse[simp] ~> antisym_on_converse[simp]
+ trans_converse[simp] ~> trans_on_converse[simp]
- Added lemmas.
antisym_onD
antisym_onI
@@ -111,17 +120,26 @@
totalI
totalp_on_converse[simp]
totalp_on_singleton[simp]
+ trans_onD
+ trans_onI
+ trans_on_subset
+ transp_onD
+ transp_onI
+ transp_on_conversep
+ transp_on_subset
+ transp_on_trans_on_eq[pred_set_conv]
* Theory "HOL.Transitive_Closure":
- Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
antisym_reflcl[simp] ~> antisym_on_reflcl[simp]
reflp_rtranclp[simp] ~> reflp_on_rtranclp[simp]
symp_symclp[simp] ~> symp_on_symclp[simp]
+ trans_reflclI[simp] ~> trans_on_reflcl[simp]
- Added lemmas.
antisymp_on_reflcp[simp]
reflclp_ident_if_reflp[simp]
reflp_on_reflclp[simp]
- transp_reflclp[simp]
+ transp_on_reflclp[simp]
* Theory "HOL.Wellfounded":
- Added lemmas.
@@ -132,6 +150,7 @@
refl_lex_prod[simp]
sym_lex_prod[simp]
sym_on_lex_prod[simp]
+ trans_on_lex_prod[simp]
wfP_if_convertible_to_nat
wfP_if_convertible_to_wfP
wf_if_convertible_to_wf
@@ -152,6 +171,8 @@
multp_cancel_add_mset
multp_cancel_max
multp_code_iff_mult
+ - Used transp_on in assumptions of lemmas bex_least_element and
+ bex_greatest_element. Minor INCOMPATIBILITIES.
- Added lemmas.
mult_mono_strong
multeqp_code_iff_reflclp_multp
--- a/src/Doc/System/Scala.thy Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Doc/System/Scala.thy Sat Dec 24 15:35:43 2022 +0000
@@ -152,7 +152,7 @@
\<^medskip>
The syntax of \<^path>\<open>etc/build.props\<close> follows a regular Java properties
- file\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/15/docs/api/java.base/java/util/Properties.html#load(java.io.Reader)\<close>\<close>,
+ file\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/Properties.html#load(java.io.Reader)\<close>\<close>,
but the encoding is \<^verbatim>\<open>UTF-8\<close>, instead of historic \<^verbatim>\<open>ISO 8859-1\<close> from the API
documentation.
--- a/src/HOL/Data_Structures/Sorted_Less.thy Fri Dec 23 11:12:19 2022 +0000
+++ b/src/HOL/Data_Structures/Sorted_Less.thy Sat Dec 24 15:35:43 2022 +0000
@@ -20,7 +20,7 @@
declare
sorted_wrt.simps(2)[simp del]
- sorted_wrt1[simp] sorted_wrt2[OF transp_less, simp]
+ sorted_wrt1[simp] sorted_wrt2[OF transp_on_less, simp]
lemma sorted_cons: "sorted (x#xs) \<Longrightarrow> sorted xs"
by(simp add: sorted_wrt_Cons)
--- a/src/HOL/Library/Complete_Partial_Order2.thy Fri Dec 23 11:12:19 2022 +0000
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Sat Dec 24 15:35:43 2022 +0000
@@ -432,7 +432,7 @@
context preorder begin
-declare transp_le[cont_intro]
+declare transp_on_le[cont_intro]
lemma monotone_const [simp, cont_intro]: "monotone ord (\<le>) (\<lambda>_. c)"
by(rule monotoneI) simp
@@ -441,7 +441,7 @@
lemma transp_le [cont_intro, simp]:
"class.preorder ord (mk_less ord) \<Longrightarrow> transp ord"
-by(rule preorder.transp_le)
+by(rule preorder.transp_on_le)
context partial_function_definitions begin
@@ -561,7 +561,7 @@
\<And>y. mcont lub ord Sup (\<le>) (\<lambda>x. f x y);
mcont lub ord lub' ord' (\<lambda>y. t y) \<rbrakk>
\<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f x (t x))"
-unfolding mcont_def by(blast intro: transp_le monotone2monotone cont_apply)
+unfolding mcont_def by(blast intro: transp_on_le monotone2monotone cont_apply)
lemma mcont2mcont:
"\<lbrakk>mcont lub' ord' Sup (\<le>) (\<lambda>x. f x); mcont lub ord lub' ord' (\<lambda>x. t x)\<rbrakk>
--- a/src/HOL/Library/Multiset.thy Fri Dec 23 11:12:19 2022 +0000
+++ b/src/HOL/Library/Multiset.thy Sat Dec 24 15:35:43 2022 +0000
@@ -1614,8 +1614,7 @@
qualified lemma
assumes
- (* FIXME: Replace by transp_on (set_mset M) R if it gets introduced. *)
- "\<forall>x \<in> set_mset M. \<forall>y \<in> set_mset M. \<forall>z \<in> set_mset M. R x y \<longrightarrow> R y z \<longrightarrow> R x z" and
+ "transp_on (set_mset M) R" and
"totalp_on (set_mset M) R" and
"M \<noteq> {#}"
shows
@@ -1629,12 +1628,10 @@
thus ?case ..
next
case (add x M)
- from add.prems(1) have transp_on_x_M_raw: "\<forall>y\<in>#M. \<forall>z\<in>#M. R x y \<and> R y z \<longrightarrow> R x z"
- by (metis insert_iff set_mset_add_mset_insert)
-
- from add.prems(1) have transp_on_R_M:
- "\<forall>x \<in> set_mset M. \<forall>y \<in> set_mset M. \<forall>z \<in> set_mset M. R x y \<longrightarrow> R y z \<longrightarrow> R x z"
- by (meson mset_subsetD multi_psub_of_add_self)
+ from add.prems(1) have
+ transp_on_x_M_raw: "\<forall>y\<in>#M. \<forall>z\<in>#M. R x y \<and> R y z \<longrightarrow> R x z" and
+ transp_on_R_M: "transp_on (set_mset M) R"
+ by (auto intro: transp_onI dest: transp_onD)
from add.prems(2) have
totalp_on_x_M_raw: "\<forall>y \<in># M. x \<noteq> y \<longrightarrow> R x y \<or> R y x" and
@@ -3458,7 +3455,7 @@
fix M N :: "'a multiset"
show "(M < N) = (M \<le> N \<and> \<not> N \<le> M)"
unfolding less_eq_multiset_def less_multiset_def
- by (metis irreflp_def irreflp_on_less irreflp_multp transpE transp_less transp_multp)
+ by (metis irreflp_def irreflp_on_less irreflp_multp transpE transp_on_less transp_multp)
next
fix M :: "'a multiset"
show "M \<le> M"
@@ -3468,14 +3465,14 @@
fix M1 M2 M3 :: "'a multiset"
show "M1 \<le> M2 \<Longrightarrow> M2 \<le> M3 \<Longrightarrow> M1 \<le> M3"
unfolding less_eq_multiset_def less_multiset_def
- using transp_multp[OF transp_less, THEN transpD]
+ using transp_multp[OF transp_on_less, THEN transpD]
by blast
next
fix M N :: "'a multiset"
show "M \<le> N \<Longrightarrow> N \<le> M \<Longrightarrow> M = N"
unfolding less_eq_multiset_def less_multiset_def
- using transp_multp[OF transp_less, THEN transpD]
- using irreflp_multp[OF transp_less irreflp_on_less, unfolded irreflp_def, rule_format]
+ using transp_multp[OF transp_on_less, THEN transpD]
+ using irreflp_multp[OF transp_on_less irreflp_on_less, unfolded irreflp_def, rule_format]
by blast
qed
--- a/src/HOL/List.thy Fri Dec 23 11:12:19 2022 +0000
+++ b/src/HOL/List.thy Sat Dec 24 15:35:43 2022 +0000
@@ -5535,7 +5535,7 @@
next
assume ?R
have "i < j \<Longrightarrow> j < length xs \<Longrightarrow> P (xs ! i) (xs ! j)" for i j
- by(induct i j rule: less_Suc_induct)(simp add: \<open>?R\<close>, meson assms transpE transp_less)
+ by(induct i j rule: less_Suc_induct)(simp add: \<open>?R\<close>, meson assms transpE transp_on_less)
thus ?L
by (simp add: sorted_wrt_iff_nth_less)
qed
--- a/src/HOL/Relation.thy Fri Dec 23 11:12:19 2022 +0000
+++ b/src/HOL/Relation.thy Sat Dec 24 15:35:43 2022 +0000
@@ -609,20 +609,46 @@
subsubsection \<open>Transitivity\<close>
-definition trans :: "'a rel \<Rightarrow> bool"
- where "trans r \<longleftrightarrow> (\<forall>x y z. (x, y) \<in> r \<longrightarrow> (y, z) \<in> r \<longrightarrow> (x, z) \<in> r)"
+definition trans_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" where
+ "trans_on A r \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>z \<in> A. (x, y) \<in> r \<longrightarrow> (y, z) \<in> r \<longrightarrow> (x, z) \<in> r)"
+
+abbreviation trans :: "'a rel \<Rightarrow> bool" where
+ "trans \<equiv> trans_on UNIV"
+
+definition transp_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "transp_on A R \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. \<forall>z \<in> A. R x y \<longrightarrow> R y z \<longrightarrow> R x z)"
+
+abbreviation transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+ "transp \<equiv> transp_on UNIV"
+
+lemma trans_def[no_atp]: "trans r \<longleftrightarrow> (\<forall>x y z. (x, y) \<in> r \<longrightarrow> (y, z) \<in> r \<longrightarrow> (x, z) \<in> r)"
+ by (simp add: trans_on_def)
-definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
- where "transp r \<longleftrightarrow> (\<forall>x y z. r x y \<longrightarrow> r y z \<longrightarrow> r x z)"
+lemma transp_def: "transp R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R y z \<longrightarrow> R x z)"
+ by (simp add: transp_on_def)
+
+text \<open>@{thm [source] trans_def} and @{thm [source] transp_def} are for backward compatibility.\<close>
+
+lemma transp_on_trans_on_eq[pred_set_conv]: "transp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans_on A r"
+ by (simp add: trans_on_def transp_on_def)
-lemma transp_trans_eq [pred_set_conv]: "transp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans r"
- by (simp add: trans_def transp_def)
+lemmas transp_trans_eq = transp_on_trans_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
+
+lemma trans_onI:
+ "(\<And>x y z. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow>
+ trans_on A r"
+ unfolding trans_on_def
+ by (intro ballI) iprover
lemma transI [intro?]: "(\<And>x y z. (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow> trans r"
- by (unfold trans_def) iprover
+ by (rule trans_onI)
-lemma transpI [intro?]: "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r"
- by (fact transI [to_pred])
+lemma transp_onI:
+ "(\<And>x y z. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z) \<Longrightarrow> transp_on A R"
+ by (rule trans_onI[to_pred])
+
+lemma transpI [intro?]: "(\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z) \<Longrightarrow> transp R"
+ by (rule transI[to_pred])
lemma transE:
assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r"
@@ -634,15 +660,25 @@
obtains "r x z"
using assms by (rule transE [to_pred])
-lemma transD [dest?]:
- assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r"
- shows "(x, z) \<in> r"
- using assms by (rule transE)
+lemma trans_onD:
+ "trans_on A r \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r"
+ unfolding trans_on_def
+ by (elim ballE) iprover+
+
+lemma transD[dest?]: "trans r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r"
+ by (simp add: trans_onD[of UNIV r x y z])
-lemma transpD [dest?]:
- assumes "transp r" and "r x y" and "r y z"
- shows "r x z"
- using assms by (rule transD [to_pred])
+lemma transp_onD: "transp_on A R \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> z \<in> A \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
+ by (rule trans_onD[to_pred])
+
+lemma transpD[dest?]: "transp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
+ by (rule transD[to_pred])
+
+lemma trans_on_subset: "trans_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> trans_on B r"
+ by (auto simp: trans_on_def)
+
+lemma transp_on_subset: "transp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> transp_on B R"
+ by (auto simp: transp_on_def)
lemma trans_Int: "trans r \<Longrightarrow> trans s \<Longrightarrow> trans (r \<inter> s)"
by (fast intro: transI elim: transE)
@@ -655,8 +691,13 @@
lemma transp_INF: "\<forall>x\<in>S. transp (r x) \<Longrightarrow> transp (\<Sqinter>(r ` S))"
by (fact trans_INTER [to_pred])
-
-lemma trans_join [code]: "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
+
+lemma trans_on_join [code]:
+ "trans_on A r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. x \<in> A \<longrightarrow> y1 \<in> A \<longrightarrow>
+ (\<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> z \<in> A \<longrightarrow> (x, z) \<in> r))"
+ by (auto simp: trans_on_def)
+
+lemma trans_join: "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
by (auto simp add: trans_def)
lemma transp_trans: "transp r \<longleftrightarrow> trans {(x, y). r x y}"
@@ -683,22 +724,26 @@
lemma asymp_on_iff_irreflp_on_if_transp: "transp R \<Longrightarrow> asymp_on A R \<longleftrightarrow> irreflp_on A R"
by (rule asym_on_iff_irrefl_on_if_trans[to_pred])
-context preorder
-begin
+lemma (in preorder) transp_on_le[simp]: "transp_on A (\<le>)"
+ by (auto intro: transp_onI order_trans)
+
+lemmas (in preorder) transp_le = transp_on_le[of UNIV]
-lemma transp_le[simp]: "transp (\<le>)"
-by(auto simp add: transp_def intro: order_trans)
+lemma (in preorder) transp_on_less[simp]: "transp_on A (<)"
+ by (auto intro: transp_onI less_trans)
+
+lemmas (in preorder) transp_less = transp_on_less[of UNIV]
-lemma transp_less[simp]: "transp (<)"
-by(auto simp add: transp_def intro: less_trans)
+lemma (in preorder) transp_on_ge[simp]: "transp_on A (\<ge>)"
+ by (auto intro: transp_onI order_trans)
+
+lemmas (in preorder) transp_ge = transp_on_ge[of UNIV]
-lemma transp_ge[simp]: "transp (\<ge>)"
-by(auto simp add: transp_def intro: order_trans)
+lemma (in preorder) transp_on_greater[simp]: "transp_on A (>)"
+ by (auto intro: transp_onI less_trans)
-lemma transp_gr[simp]: "transp (>)"
-by(auto simp add: transp_def intro: less_trans)
+lemmas (in preorder) transp_gr = transp_on_greater[of UNIV]
-end
subsubsection \<open>Totality\<close>
@@ -1140,8 +1185,11 @@
lemma antisymp_on_conversep [simp]: "antisymp_on A R\<inverse>\<inverse> = antisymp_on A R"
by (rule antisym_on_converse[to_pred])
-lemma trans_converse [simp]: "trans (converse r) = trans r"
- unfolding trans_def by blast
+lemma trans_on_converse [simp]: "trans_on A (r\<inverse>) = trans_on A r"
+ by (auto intro: trans_onI dest: trans_onD)
+
+lemma transp_on_conversep [simp]: "transp_on A R\<inverse>\<inverse> = transp_on A R"
+ by (rule trans_on_converse[to_pred])
lemma sym_conv_converse_eq: "sym r \<longleftrightarrow> r\<inverse> = r"
unfolding sym_def by fast
--- a/src/HOL/Tools/BNF/bnf_util.ML Fri Dec 23 11:12:19 2022 +0000
+++ b/src/HOL/Tools/BNF/bnf_util.ML Sat Dec 24 15:35:43 2022 +0000
@@ -400,7 +400,7 @@
Const (name, uncurry mk_pred2T (fastype_of R |> dest_pred2T) --> HOLogic.boolT) $ R;
val mk_reflp = mk_pred \<^const_abbrev>\<open>reflp\<close>;
val mk_symp = mk_pred \<^const_abbrev>\<open>symp\<close>;
-val mk_transp = mk_pred \<^const_name>\<open>transp\<close>;
+val mk_transp = mk_pred \<^const_abbrev>\<open>transp\<close>;
fun mk_trans thm1 thm2 = trans OF [thm1, thm2];
fun mk_sym thm = thm RS sym;
--- a/src/HOL/Transitive_Closure.thy Fri Dec 23 11:12:19 2022 +0000
+++ b/src/HOL/Transitive_Closure.thy Sat Dec 24 15:35:43 2022 +0000
@@ -82,11 +82,11 @@
lemma antisymp_on_reflcp[simp]: "antisymp_on A R\<^sup>=\<^sup>= \<longleftrightarrow> antisymp_on A R"
by (rule antisym_on_reflcl[to_pred])
-lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans (r\<^sup>=)"
- unfolding trans_def by blast
+lemma trans_on_reflcl[simp]: "trans_on A r \<Longrightarrow> trans_on A (r\<^sup>=)"
+ by (auto intro: trans_onI dest: trans_onD)
-lemma transp_reflclp[simp]: "transp R \<Longrightarrow> transp R\<^sup>=\<^sup>="
- unfolding transp_def by blast
+lemma transp_on_reflclp[simp]: "transp_on A R \<Longrightarrow> transp_on A R\<^sup>=\<^sup>="
+ by (rule trans_on_reflcl[to_pred])
lemma reflclp_idemp [simp]: "(P\<^sup>=\<^sup>=)\<^sup>=\<^sup>= = P\<^sup>=\<^sup>="
by blast
--- a/src/HOL/Wellfounded.thy Fri Dec 23 11:12:19 2022 +0000
+++ b/src/HOL/Wellfounded.thy Sat Dec 24 15:35:43 2022 +0000
@@ -875,9 +875,20 @@
"asym r\<^sub>A \<Longrightarrow> asym r\<^sub>B \<Longrightarrow> asym (r\<^sub>A <*lex*> r\<^sub>B)"
by (rule asym_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])
-text \<open>\<open><*lex*>\<close> preserves transitivity\<close>
-lemma trans_lex_prod [simp,intro!]: "trans R1 \<Longrightarrow> trans R2 \<Longrightarrow> trans (R1 <*lex*> R2)"
- unfolding trans_def lex_prod_def by blast
+lemma trans_on_lex_prod[simp]:
+ assumes "trans_on A r\<^sub>A" and "trans_on B r\<^sub>B"
+ shows "trans_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)"
+proof (rule trans_onI)
+ fix x y z
+ show "x \<in> A \<times> B \<Longrightarrow> y \<in> A \<times> B \<Longrightarrow> z \<in> A \<times> B \<Longrightarrow>
+ (x, y) \<in> r\<^sub>A <*lex*> r\<^sub>B \<Longrightarrow> (y, z) \<in> r\<^sub>A <*lex*> r\<^sub>B \<Longrightarrow> (x, z) \<in> r\<^sub>A <*lex*> r\<^sub>B"
+ using trans_onD[OF \<open>trans_on A r\<^sub>A\<close>, of "fst x" "fst y" "fst z"]
+ using trans_onD[OF \<open>trans_on B r\<^sub>B\<close>, of "snd x" "snd y" "snd z"]
+ by auto
+qed
+
+lemma trans_lex_prod [simp,intro!]: "trans r\<^sub>A \<Longrightarrow> trans r\<^sub>B \<Longrightarrow> trans (r\<^sub>A <*lex*> r\<^sub>B)"
+ by (rule trans_on_lex_prod[of UNIV _ UNIV, unfolded UNIV_Times_UNIV])
lemma total_on_lex_prod[simp]:
"total_on A r\<^sub>A \<Longrightarrow> total_on B r\<^sub>B \<Longrightarrow> total_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)"
--- a/src/Pure/PIDE/document.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Pure/PIDE/document.scala Sat Dec 24 15:35:43 2022 +0000
@@ -319,9 +319,10 @@
def update_commands(new_commands: Linear_Set[Command]): Node =
if (new_commands eq _commands.commands) this
- else
+ else {
new Node(get_blob, header, syntax, text_perspective, perspective,
Node.Commands(new_commands))
+ }
def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
_commands.iterator(i)
@@ -503,6 +504,36 @@
/* snapshot: persistent user-view of document state */
+ object Pending_Edits {
+ val empty: Pending_Edits = make(Nil)
+
+ def make(models: Iterable[Model]): Pending_Edits =
+ new Pending_Edits(
+ (for {
+ model <- models.iterator
+ edits = model.pending_edits if edits.nonEmpty
+ } yield model.node_name -> edits).toMap)
+ }
+
+ final class Pending_Edits(pending_edits: Map[Node.Name, List[Text.Edit]]) {
+ def is_stable: Boolean = pending_edits.isEmpty
+
+ def + (entry: (Document.Node.Name, List[Text.Edit])): Pending_Edits = {
+ val (name, es) = entry
+ if (es.isEmpty) this
+ else new Pending_Edits(pending_edits + (name -> (es ::: edits(name))))
+ }
+
+ def edits(name: Document.Node.Name): List[Text.Edit] =
+ pending_edits.getOrElse(name, Nil)
+
+ def reverse_edits(name: Document.Node.Name): List[Text.Edit] =
+ reverse_pending_edits.getOrElse(name, Nil)
+
+ private lazy val reverse_pending_edits =
+ (for ((name, es) <- pending_edits.iterator) yield (name, es.reverse)).toMap
+ }
+
object Snapshot {
val init: Snapshot = State.init.snapshot()
}
@@ -511,13 +542,17 @@
val state: State,
val version: Version,
val node_name: Node.Name,
- edits: List[Text.Edit],
+ pending_edits: Pending_Edits,
val snippet_command: Option[Command]
) {
override def toString: String =
"Snapshot(node = " + node_name.node + ", version = " + version.id +
(if (is_outdated) ", outdated" else "") + ")"
+ def switch(name: Node.Name): Snapshot =
+ if (name == node_name) this
+ else new Snapshot(state, version, name, pending_edits, None)
+
/* nodes */
@@ -538,16 +573,14 @@
}
- /* edits */
+ /* pending edits */
- def is_outdated: Boolean = edits.nonEmpty
-
- private lazy val reverse_edits = edits.reverse
+ def is_outdated: Boolean = !pending_edits.is_stable
def convert(offset: Text.Offset): Text.Offset =
- edits.foldLeft(offset) { case (i, edit) => edit.convert(i) }
+ pending_edits.edits(node_name).foldLeft(offset) { case (i, edit) => edit.convert(i) }
def revert(offset: Text.Offset): Text.Offset =
- reverse_edits.foldLeft(offset) { case (i, edit) => edit.revert(i) }
+ pending_edits.reverse_edits(node_name).foldLeft(offset) { case (i, edit) => edit.revert(i) }
def convert(range: Text.Range): Text.Range = range.map(convert)
def revert(range: Text.Range): Text.Range = range.map(revert)
@@ -752,7 +785,7 @@
trait Model {
def session: Session
def is_stable: Boolean
- def snapshot(): Snapshot
+ def pending_edits: List[Text.Edit]
def node_name: Node.Name
def is_theory: Boolean = node_name.is_theory
@@ -993,9 +1026,12 @@
val edited_nodes =
(for { (name, _) <- version.nodes.iterator if edited_set(name.node) } yield name).toList
- def upd(exec_id: Document_ID.Exec, st: Command.State)
- : Option[(Document_ID.Exec, Command.State)] =
+ def upd(
+ exec_id: Document_ID.Exec,
+ st: Command.State
+ ): Option[(Document_ID.Exec, Command.State)] = {
if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st)
+ }
val (changed_commands, new_execs) =
update.foldLeft((List.empty[Command], execs)) {
@@ -1071,13 +1107,15 @@
blobs1 += digest
}
- if (!commands1.isDefinedAt(command.id))
+ if (!commands1.isDefinedAt(command.id)) {
commands.get(command.id).foreach(st => commands1 += (command.id -> st))
+ }
- for (exec_id <- command_execs.getOrElse(command.id, Nil)) {
- if (!execs1.isDefinedAt(exec_id))
- execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
- }
+ for {
+ exec_id <- command_execs.getOrElse(command.id, Nil)
+ if !execs1.isDefinedAt(exec_id)
+ st <- execs.get(exec_id)
+ } execs1 += (exec_id -> st)
}
copy(
@@ -1196,26 +1234,19 @@
def snapshot(
node_name: Node.Name = Node.Name.empty,
- pending_edits: List[Text.Edit] = Nil,
+ pending_edits: Pending_Edits = Pending_Edits.empty,
snippet_command: Option[Command] = None
): Snapshot = {
val stable = recent_stable
val version = stable.version.get_finished
- val rev_pending_changes =
- for {
+ val pending_edits1 =
+ (for {
change <- history.undo_list.takeWhile(_ != stable)
- (name, edits) <- change.rev_edits
- if name == node_name
- } yield edits
+ (name, Node.Edits(es)) <- change.rev_edits
+ } yield (name -> es)).foldLeft(pending_edits)(_ + _)
- val edits =
- rev_pending_changes.foldLeft(pending_edits) {
- case (edits, Node.Edits(es)) => es ::: edits
- case (edits, _) => edits
- }
-
- new Snapshot(this, version, node_name, edits, snippet_command)
+ new Snapshot(this, version, node_name, pending_edits1, snippet_command)
}
def snippet(command: Command): Snapshot =
--- a/src/Pure/PIDE/resources.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Pure/PIDE/resources.scala Sat Dec 24 15:35:43 2022 +0000
@@ -458,18 +458,19 @@
/* resolve implicit theory dependencies */
def resolve_dependencies[A](
- models: Map[A, Document.Model],
- theories: List[(Document.Node.Name, Position.T)]
+ models: Iterable[Document.Model],
+ theories: List[Document.Node.Name]
): List[Document.Node.Name] = {
val model_theories =
- (for (model <- models.valuesIterator if model.is_theory)
+ (for (model <- models.iterator if model.is_theory)
yield (model.node_name, Position.none)).toList
- val thy_files1 = dependencies(model_theories ::: theories).theories
+ val thy_files1 =
+ dependencies(model_theories ::: theories.map((_, Position.none))).theories
val thy_files2 =
(for {
- model <- models.valuesIterator if !model.is_theory
+ model <- models.iterator if !model.is_theory
thy_name <- make_theory_name(model.node_name)
} yield thy_name).toList
--- a/src/Pure/PIDE/session.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Pure/PIDE/session.scala Sat Dec 24 15:35:43 2022 +0000
@@ -688,16 +688,17 @@
else Document.State.init
}
- def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
- pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
- get_state().snapshot(name, pending_edits)
+ def snapshot(
+ node_name: Document.Node.Name = Document.Node.Name.empty,
+ pending_edits: Document.Pending_Edits = Document.Pending_Edits.empty
+ ): Document.Snapshot = get_state().snapshot(node_name = node_name, pending_edits = pending_edits)
def recent_syntax(name: Document.Node.Name): Outer_Syntax =
get_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse
resources.session_base.overall_syntax
- def stable_tip_version[A](models: Map[A, Document.Model]): Option[Document.Version] =
- if (models.valuesIterator.forall(_.is_stable)) get_state().stable_tip_version
+ def stable_tip_version[A](models: Iterable[Document.Model]): Option[Document.Version] =
+ if (models.forall(model => model.pending_edits.isEmpty)) get_state().stable_tip_version
else None
@tailrec final def await_stable_snapshot(): Document.Snapshot = {
--- a/src/Pure/Thy/document_build.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Pure/Thy/document_build.scala Sat Dec 24 15:35:43 2022 +0000
@@ -132,6 +132,17 @@
List("isabelle.sty", "isabellesym.sty", "pdfsetup.sty", "railsetup.sty").
map(name => texinputs + Path.basic(name))
+ def running_script(title: String): String = "echo 'Running " + quote(title) + " ...'; "
+ def is_running_script(msg: String): Boolean =
+ msg.startsWith("Running \"") && msg.endsWith("\" ...")
+
+ sealed case class Document_Latex(name: Document.Node.Name, body: XML.Body) {
+ def content: File.Content_XML = File.content(Path.basic(tex_name(name)), body)
+ def file_pos: String = name.path.implode_symbolic
+ def write(latex_output: Latex.Output, dir: Path): Unit =
+ content.output(latex_output(_, file_pos = file_pos)).write(dir)
+ }
+
def context(
session_context: Export.Session_Context,
document_session: Option[Sessions.Base] = None,
@@ -185,19 +196,15 @@
def session_document_theories: List[Document.Node.Name] = base.proper_session_theories
def all_document_theories: List[Document.Node.Name] = base.all_document_theories
- lazy val document_latex: List[(File.Content_XML, String)] =
- for (name <- all_document_theories)
- yield {
- val path = Path.basic(tex_name(name))
- val content =
- if (document_selection(name)) {
- val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
- YXML.parse_body(entry.text)
- }
- else Nil
- val file_pos = name.path.implode_symbolic
- (File.content(path, content), file_pos)
- }
+ lazy val isabelle_logo: Option[File.Content] = {
+ document_logo.map(logo_name =>
+ Isabelle_System.with_tmp_file("logo", ext = "pdf") { tmp_path =>
+ Logo.create_logo(logo_name, output_file = tmp_path, quiet = true)
+ val path = Path.basic("isabelle_logo.pdf")
+ val content = Bytes.read(tmp_path)
+ File.content(path, content)
+ })
+ }
lazy val session_graph: File.Content = {
val path = Browser_Info.session_graph_path
@@ -213,15 +220,17 @@
File.content(path, content)
}
- lazy val isabelle_logo: Option[File.Content] = {
- document_logo.map(logo_name =>
- Isabelle_System.with_tmp_file("logo", ext = "pdf") { tmp_path =>
- Logo.create_logo(logo_name, output_file = tmp_path, quiet = true)
- val path = Path.basic("isabelle_logo.pdf")
- val content = Bytes.read(tmp_path)
- File.content(path, content)
- })
- }
+ lazy val document_latex: List[Document_Latex] =
+ for (name <- all_document_theories)
+ yield {
+ val body =
+ if (document_selection(name)) {
+ val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
+ YXML.parse_body(entry.text)
+ }
+ else Nil
+ Document_Latex(name, body)
+ }
/* build document */
@@ -263,11 +272,7 @@
}
session_tex.write(doc_dir)
-
- for ((content, file_pos) <- document_latex) {
- content.output(latex_output(_, file_pos = file_pos))
- .write(doc_dir)
- }
+ document_latex.foreach(_.write(latex_output, doc_dir))
val root_name1 = "root_" + doc.name
val root_name = if ((doc_dir + Path.explode(root_name1).tex).is_file) root_name1 else "root"
@@ -280,7 +285,6 @@
/* derived material: without SHA1 digest */
isabelle_logo.foreach(_.write(doc_dir))
-
session_graph.write(doc_dir)
Directory(doc_dir, doc, root_name, sources)
@@ -304,12 +308,16 @@
def root_name_script(ext: String = ""): String =
Bash.string(if (ext.isEmpty) root_name else root_name + "." + ext)
- def conditional_script(ext: String, exe: String, after: String = ""): String =
+ def conditional_script(
+ ext: String, exe: String, title: String = "", after: String = ""
+ ): String = {
"if [ -f " + root_name_script(ext) + " ]\n" +
"then\n" +
- " " + exe + " " + root_name_script() + "\n" +
+ " " + (if (title.nonEmpty) running_script(title) else "") +
+ exe + " " + root_name_script() + "\n" +
(if (after.isEmpty) "" else " " + after) +
"fi\n"
+ }
def log_errors(): List[String] =
Latex.latex_errors(doc_dir, root_name) :::
@@ -350,18 +358,19 @@
context.prepare_directory(dir, doc, new Latex.Output(context.options))
def use_pdflatex: Boolean = false
+ def running_latex: String = running_script(if (use_pdflatex) "pdflatex" else "lualatex")
def latex_script(context: Context, directory: Directory): String =
- (if (use_pdflatex) "$ISABELLE_PDFLATEX" else "$ISABELLE_LUALATEX") +
+ running_latex + (if (use_pdflatex) "$ISABELLE_PDFLATEX" else "$ISABELLE_LUALATEX") +
" " + directory.root_name_script() + "\n"
def bibtex_script(context: Context, directory: Directory, latex: Boolean = false): String = {
val ext = if (context.document_bibliography) "aux" else "bib"
- directory.conditional_script(ext, "$ISABELLE_BIBTEX",
+ directory.conditional_script(ext, "$ISABELLE_BIBTEX", title = "bibtex",
after = if (latex) latex_script(context, directory) else "")
}
def makeindex_script(context: Context, directory: Directory, latex: Boolean = false): String =
- directory.conditional_script("idx", "$ISABELLE_MAKEINDEX",
+ directory.conditional_script("idx", "$ISABELLE_MAKEINDEX", title = "makeindex",
after = if (latex) latex_script(context, directory) else "")
def use_build_script: Boolean = false
--- a/src/Tools/VSCode/src/dynamic_output.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/VSCode/src/dynamic_output.scala Sat Dec 24 15:35:43 2022 +0000
@@ -21,7 +21,7 @@
resources.get_caret() match {
case None => copy(output = Nil)
case Some(caret) =>
- val snapshot = caret.model.snapshot()
+ val snapshot = resources.snapshot(caret.model)
if (do_update && !snapshot.is_outdated) {
snapshot.current_command(caret.node_name, caret.offset) match {
case None => copy(output = Nil)
--- a/src/Tools/VSCode/src/language_server.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/VSCode/src/language_server.scala Sat Dec 24 15:35:43 2022 +0000
@@ -121,9 +121,8 @@
def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
for {
- model <- resources.get_model(new JFile(node_pos.name))
- rendering = model.rendering()
- offset <- model.content.doc.offset(node_pos.pos)
+ rendering <- resources.get_rendering(new JFile(node_pos.name))
+ offset <- rendering.model.content.doc.offset(node_pos.pos)
} yield (rendering, offset)
private val dynamic_output = Dynamic_Output(server)
@@ -366,7 +365,7 @@
for {
spell_checker <- resources.spell_checker.get
caret <- resources.get_caret()
- rendering = caret.model.rendering()
+ rendering = resources.rendering(caret.model)
range = rendering.before_caret_range(caret.offset)
Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
} {
@@ -493,11 +492,11 @@
override def current_node(context: Unit): Option[Document.Node.Name] =
resources.get_caret().map(_.model.node_name)
override def current_node_snapshot(context: Unit): Option[Document.Snapshot] =
- resources.get_caret().map(_.model.snapshot())
+ resources.get_caret().map(caret => resources.snapshot(caret.model))
override def node_snapshot(name: Document.Node.Name): Document.Snapshot = {
- resources.get_model(name) match {
- case Some(model) => model.snapshot()
+ resources.get_snapshot(name) match {
+ case Some(snapshot) => snapshot
case None => session.snapshot(name)
}
}
--- a/src/Tools/VSCode/src/preview_panel.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/VSCode/src/preview_panel.scala Sat Dec 24 15:35:43 2022 +0000
@@ -25,7 +25,7 @@
case (m, (file, column)) =>
resources.get_model(file) match {
case Some(model) =>
- val snapshot = model.snapshot()
+ val snapshot = resources.snapshot(model)
if (snapshot.is_outdated) m
else {
val context =
--- a/src/Tools/VSCode/src/vscode_model.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/VSCode/src/vscode_model.scala Sat Dec 24 15:35:43 2022 +0000
@@ -78,6 +78,7 @@
) extends Document.Model {
model =>
+
/* content */
def get_text(range: Text.Range): Option[String] = content.doc.get_text(range)
@@ -106,7 +107,7 @@
caret: Option[Line.Position]
): (Boolean, Document.Node.Perspective_Text.T) = {
if (is_theory) {
- val snapshot = model.snapshot()
+ val snapshot = resources.snapshot(model)
val required = node_required || editor.document_node_required(node_name)
@@ -231,11 +232,6 @@
def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
def is_stable: Boolean = pending_edits.isEmpty
- def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
-
- def rendering(snapshot: Document.Snapshot): VSCode_Rendering =
- new VSCode_Rendering(snapshot, model)
- def rendering(): VSCode_Rendering = rendering(snapshot())
/* syntax */
--- a/src/Tools/VSCode/src/vscode_rendering.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Sat Dec 24 15:35:43 2022 +0000
@@ -78,10 +78,10 @@
/* bibtex */
def bibtex_entries_iterator(): Iterator[Text.Info[(String, VSCode_Model)]] =
- Bibtex.entries_iterator(resources.get_models)
+ Bibtex.entries_iterator(resources.get_models())
def bibtex_completion(history: Completion.History, caret: Text.Offset): Option[Completion.Result] =
- Bibtex.completion(history, rendering, caret, resources.get_models)
+ Bibtex.completion(history, rendering, caret, resources.get_models())
/* completion */
--- a/src/Tools/VSCode/src/vscode_resources.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/VSCode/src/vscode_resources.scala Sat Dec 24 15:35:43 2022 +0000
@@ -113,11 +113,39 @@
else File.absolute_name(new JFile(dir + JFile.separator + File.platform_path(path)))
}
- def get_models: Map[JFile, VSCode_Model] = state.value.models
- def get_model(file: JFile): Option[VSCode_Model] = get_models.get(file)
+ def get_models(): Map[JFile, VSCode_Model] = state.value.models
+ def get_model(file: JFile): Option[VSCode_Model] = get_models().get(file)
def get_model(name: Document.Node.Name): Option[VSCode_Model] = get_model(node_file(name))
+ /* snapshot */
+
+ def snapshot(model: VSCode_Model): Document.Snapshot =
+ model.session.snapshot(
+ node_name = model.node_name,
+ pending_edits = Document.Pending_Edits.make(get_models().values))
+
+ def get_snapshot(file: JFile): Option[Document.Snapshot] =
+ get_model(file).map(snapshot)
+
+ def get_snapshot(name: Document.Node.Name): Option[Document.Snapshot] =
+ get_model(name).map(snapshot)
+
+
+ /* rendering */
+
+ def rendering(snapshot: Document.Snapshot, model: VSCode_Model): VSCode_Rendering =
+ new VSCode_Rendering(snapshot, model)
+
+ def rendering(model: VSCode_Model): VSCode_Rendering = rendering(snapshot(model), model)
+
+ def get_rendering(file: JFile): Option[VSCode_Rendering] =
+ get_model(file).map(rendering)
+
+ def get_rendering(name: Document.Node.Name): Option[VSCode_Rendering] =
+ get_model(name).map(rendering)
+
+
/* file content */
def read_file_content(name: Document.Node.Name): Option[String] = {
@@ -207,11 +235,10 @@
file_watcher: File_Watcher
): (Boolean, Boolean) = {
state.change_result { st =>
- val stable_tip_version = session.stable_tip_version(st.models)
+ val stable_tip_version = session.stable_tip_version(st.models.values)
val thy_files =
- resources.resolve_dependencies(st.models,
- editor.document_required().map((_, Position.none)))
+ resources.resolve_dependencies(st.models.values, editor.document_required())
val aux_files = stable_tip_version.toList.flatMap(undefined_blobs)
@@ -275,7 +302,7 @@
(for {
file <- st.pending_output.iterator
model <- st.models.get(file)
- } yield (file, model, model.rendering())).toList.partition(_._3.snapshot.is_outdated)
+ } yield (file, model, rendering(model))).toList.partition(_._3.snapshot.is_outdated)
val changed_iterator =
for {
--- a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Sat Dec 24 15:35:43 2022 +0000
@@ -175,8 +175,8 @@
class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup") {
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = {
val opt_snapshot =
- Document_Model.get(buffer) match {
- case Some(model) if model.is_theory => Some(model.snapshot())
+ Document_Model.get_model(buffer) match {
+ case Some(model) if model.is_theory => Some(Document_Model.snapshot(model))
case _ => None
}
opt_snapshot match {
--- a/src/Tools/jEdit/src/active.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/jEdit/src/active.scala Sat Dec 24 15:35:43 2022 +0000
@@ -28,7 +28,7 @@
Document_View.get(view.getTextArea) match {
case Some(doc_view) =>
doc_view.rich_text_area.robust_body(()) {
- val snapshot = doc_view.model.snapshot()
+ val snapshot = Document_Model.snapshot(doc_view.model)
if (!snapshot.is_outdated) {
handlers.find(_.handle(view, text, elem, doc_view, snapshot))
}
--- a/src/Tools/jEdit/src/completion_popup.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/jEdit/src/completion_popup.scala Sat Dec 24 15:35:43 2022 +0000
@@ -281,7 +281,7 @@
if (buffer.isEditable) {
val caret = text_area.getCaretPosition
- val opt_rendering = Document_View.get(text_area).map(_.get_rendering())
+ val opt_rendering = Document_View.get_rendering(text_area)
val result0 = syntax_completion(history, explicit, opt_rendering)
val (no_completion, semantic_completion) = {
opt_rendering match {
--- a/src/Tools/jEdit/src/debugger_dockable.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Sat Dec 24 15:35:43 2022 +0000
@@ -33,7 +33,7 @@
Document_View.get(text_area) match {
case Some(doc_view) =>
- val rendering = doc_view.get_rendering()
+ val rendering = Document_View.rendering(doc_view)
val range = JEdit_Lib.point_range(text_area.getBuffer, offset)
rendering.breakpoint(range)
case None => None
--- a/src/Tools/jEdit/src/document_dockable.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/jEdit/src/document_dockable.scala Sat Dec 24 15:35:43 2022 +0000
@@ -106,7 +106,7 @@
}
private val scroll_log_area = new ScrollPane(log_area)
- def log_progress(): Document_Editor.Log_Progress =
+ def log_progress(only_running: Boolean = false): Document_Editor.Log_Progress =
new Document_Editor.Log_Progress(PIDE.session) {
override def show(text: String): Unit =
if (text != log_area.text) {
@@ -114,6 +114,8 @@
val vertical = scroll_log_area.peer.getVerticalScrollBar
vertical.setValue(vertical.getMaximum)
}
+ override def echo(msg: String): Unit =
+ if (!only_running || Document_Build.is_running_script(msg)) super.echo(msg)
}
@@ -131,11 +133,13 @@
private def finish_process(output: List[XML.Tree]): Unit =
current_state.change(_.finish(output))
- private def run_process(body: Document_Editor.Log_Progress => Unit): Boolean = {
+ private def run_process(only_running: Boolean = false)(
+ body: Document_Editor.Log_Progress => Unit
+ ): Boolean = {
val started =
current_state.change_result { st =>
if (st.process.is_finished) {
- val progress = log_progress()
+ val progress = log_progress(only_running = only_running)
val process =
Future.thread[Unit](name = "Document_Dockable.process") {
await_process()
@@ -151,7 +155,7 @@
private def load_document(session: String): Boolean = {
val options = PIDE.options.value
- run_process { _ =>
+ run_process() { _ =>
try {
val session_background =
Document_Build.session_background(
@@ -212,7 +216,7 @@
private def build_document(): Unit = {
PIDE.editor.document_session() match {
case Some(session_background) if session_background.info.documents.nonEmpty =>
- run_process { progress =>
+ run_process(only_running = true) { progress =>
show_page(log_page)
val result = Exn.capture { document_build(session_background, progress) }
val msgs =
--- a/src/Tools/jEdit/src/document_model.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/jEdit/src/document_model.scala Sat Dec 24 15:35:43 2022 +0000
@@ -82,11 +82,20 @@
def reset(): Unit = state.change(_ => State())
+ def document_blobs(): Document.Blobs = state.value.document_blobs
+
def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
- def get(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
- def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
+ def get_model(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
+ def get_model(buffer: JEditBuffer): Option[Buffer_Model] =
+ state.value.buffer_models.get(buffer)
- def document_blobs(): Document.Blobs = state.value.document_blobs
+ def snapshot(model: Document_Model): Document.Snapshot =
+ PIDE.session.snapshot(
+ node_name = model.node_name,
+ pending_edits = Document.Pending_Edits.make(get_models().values))
+
+ def get_snapshot(name: Document.Node.Name): Option[Document.Snapshot] = get_model(name).map(snapshot)
+ def get_snapshot(buffer: JEditBuffer): Option[Document.Snapshot] = get_model(buffer).map(snapshot)
/* bibtex */
@@ -218,7 +227,7 @@
toggle: Boolean = false,
set: Boolean = false
): Unit =
- Document_Model.get(view.getBuffer).foreach(model =>
+ Document_Model.get_model(view.getBuffer).foreach(model =>
node_required(model.node_name, toggle = toggle, set = set))
@@ -290,7 +299,7 @@
/* HTTP preview */
def open_preview(view: View, plain_text: Boolean): Unit = {
- Document_Model.get(view.getBuffer) match {
+ Document_Model.get_model(view.getBuffer) match {
case Some(model) =>
val url = Preview_Service.server_url(plain_text, model.node_name)
PIDE.editor.hyperlink_url(url).follow(view)
@@ -311,7 +320,7 @@
for {
query <- request.decode_query
name = Library.perhaps_unprefix(plain_text_prefix, query)
- model <- get(PIDE.resources.node_name(name))
+ model <- get_model(PIDE.resources.node_name(name))
}
yield {
val snapshot = model.await_stable_snapshot()
@@ -328,6 +337,9 @@
}
sealed abstract class Document_Model extends Document.Model {
+ model =>
+
+
/* perspective */
def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil
@@ -339,7 +351,7 @@
GUI_Thread.require {}
if (JEdit_Options.continuous_checking() && is_theory) {
- val snapshot = this.snapshot()
+ val snapshot = Document_Model.snapshot(model)
val required = node_required || PIDE.editor.document_node_required(node_name)
@@ -362,7 +374,7 @@
/* snapshot */
@tailrec final def await_stable_snapshot(): Document.Snapshot = {
- val snapshot = this.snapshot()
+ val snapshot = Document_Model.snapshot(model)
if (snapshot.is_outdated) {
PIDE.session.output_delay.sleep()
await_stable_snapshot()
@@ -465,11 +477,7 @@
Some(node_edits(Document.Node.no_header, text_edits, Document.Node.Perspective_Text.empty))
}
-
- /* snapshot */
-
def is_stable: Boolean = pending_edits.isEmpty
- def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
}
case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
@@ -537,7 +545,7 @@
_blob = Some(x)
x
}
- val changed = pending_edits.nonEmpty
+ val changed = !buffer_edits.is_empty
Some(Document.Blob(bytes, text, chunk, changed))
}
}
@@ -568,13 +576,13 @@
}
- /* pending edits */
+ /* pending buffer edits */
- private object pending_edits {
+ private object buffer_edits {
private val pending = new mutable.ListBuffer[Text.Edit]
private var last_perspective = Document.Node.Perspective_Text.empty
- def nonEmpty: Boolean = synchronized { pending.nonEmpty }
+ def is_empty: Boolean = synchronized { pending.isEmpty }
def get_edits: List[Text.Edit] = synchronized { pending.toList }
def get_last_perspective: Document.Node.Perspective_Text.T = synchronized { last_perspective }
def set_last_perspective(perspective: Document.Node.Perspective_Text.T): Unit =
@@ -600,19 +608,20 @@
reset_blob()
reset_bibtex_entries()
- for (doc_view <- document_view_iterator)
+ for (doc_view <- document_view_iterator) {
doc_view.rich_text_area.active_reset()
+ }
pending ++= edits
PIDE.editor.invoke()
}
}
- def is_stable: Boolean = !pending_edits.nonEmpty
- def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits)
+ def is_stable: Boolean = buffer_edits.is_empty
+ def pending_edits: List[Text.Edit] = buffer_edits.get_edits
def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
- pending_edits.flush_edits(doc_blobs, hidden)
+ buffer_edits.flush_edits(doc_blobs, hidden)
/* buffer listener */
@@ -625,7 +634,7 @@
num_lines: Int,
length: Int
): Unit = {
- pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
+ buffer_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
}
override def preContentRemoved(
@@ -635,7 +644,7 @@
num_lines: Int,
removed_length: Int
): Unit = {
- pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
+ buffer_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
}
}
@@ -644,9 +653,10 @@
def syntax_changed(): Unit = {
JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0)
- for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
+ for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
invoke(text_area)
+ }
buffer.invalidateCachedFoldLevels()
}
@@ -667,11 +677,11 @@
old_model match {
case None =>
- pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
+ buffer_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
case Some(file_model) =>
set_node_required(file_model.node_required)
- pending_edits.set_last_perspective(file_model.last_perspective)
- pending_edits.edit(
+ buffer_edits.set_last_perspective(file_model.last_perspective)
+ buffer_edits.edit(
file_model.pending_edits :::
Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer)))
}
@@ -693,7 +703,7 @@
File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer),
node_required = _node_required,
- last_perspective = pending_edits.get_last_perspective,
- pending_edits = pending_edits.get_edits)
+ last_perspective = buffer_edits.get_last_perspective,
+ pending_edits = pending_edits)
}
}
--- a/src/Tools/jEdit/src/document_view.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/jEdit/src/document_view.scala Sat Dec 24 15:35:43 2022 +0000
@@ -49,17 +49,25 @@
doc_view.activate()
doc_view
}
+
+ def rendering(doc_view: Document_View): JEdit_Rendering = {
+ val model = doc_view.model
+ val snapshot = Document_Model.snapshot(model)
+ val options = PIDE.options.value
+ JEdit_Rendering(snapshot, model, options)
+ }
+
+ def get_rendering(text_area: TextArea): Option[JEdit_Rendering] = get(text_area).map(rendering)
}
+class Document_View(val model: Buffer_Model, val text_area: JEditTextArea) {
+ doc_view =>
-class Document_View(val model: Buffer_Model, val text_area: JEditTextArea) {
private val session = model.session
- def get_rendering(): JEdit_Rendering =
- JEdit_Rendering(model.snapshot(), model, PIDE.options.value)
-
- val rich_text_area =
- new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (), () => None,
+ val rich_text_area: Rich_Text_Area =
+ new Rich_Text_Area(text_area.getView, text_area,
+ () => Document_View.rendering(doc_view), () => (), () => None,
() => delay_caret_update.invoke(), caret_visible = true, enable_hovering = false)
@@ -138,7 +146,7 @@
val buffer = model.buffer
JEdit_Lib.buffer_lock(buffer) {
- val rendering = get_rendering()
+ val rendering = Document_View.rendering(doc_view)
for (i <- physical_lines.indices) {
if (physical_lines(i) != -1) {
@@ -199,7 +207,7 @@
/* text status overview left of scrollbar */
private val text_overview: Option[Text_Overview] =
- if (PIDE.options.bool("jedit_text_overview")) Some(new Text_Overview(this)) else None
+ if (PIDE.options.bool("jedit_text_overview")) Some(new Text_Overview(doc_view)) else None
/* main */
@@ -214,7 +222,7 @@
GUI_Thread.later {
JEdit_Lib.buffer_lock(buffer) {
if (model.buffer == text_area.getBuffer) {
- val snapshot = model.snapshot()
+ val snapshot = Document_Model.snapshot(model)
if (changed.assignment ||
(changed.nodes.contains(model.node_name) &&
--- a/src/Tools/jEdit/src/isabelle.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/jEdit/src/isabelle.scala Sat Dec 24 15:35:43 2022 +0000
@@ -60,7 +60,7 @@
def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
if (buffer == null) None
else
- (JEdit_Lib.buffer_mode(buffer), Document_Model.get(buffer)) match {
+ (JEdit_Lib.buffer_mode(buffer), Document_Model.get_model(buffer)) match {
case ("isabelle", Some(model)) =>
Some(PIDE.session.recent_syntax(model.node_name))
case (mode, _) => mode_syntax(mode)
@@ -328,7 +328,7 @@
): Unit = {
val buffer = text_area.getBuffer
if (!snapshot.is_outdated && text != "") {
- (snapshot.find_command(id), Document_Model.get(buffer)) match {
+ (snapshot.find_command(id), Document_Model.get_model(buffer)) match {
case (Some((node, command)), Some(model)) if command.node_name == model.node_name =>
node.command_start(command) match {
case Some(start) =>
@@ -365,16 +365,14 @@
def goto_entity(view: View): Unit = {
val text_area = view.getTextArea
for {
- doc_view <- Document_View.get(text_area)
- rendering = doc_view.get_rendering()
+ rendering <- Document_View.get_rendering(text_area)
caret_range = JEdit_Lib.caret_range(text_area)
link <- rendering.hyperlink_entity(caret_range)
} link.info.follow(view)
}
def select_entity(text_area: JEditTextArea): Unit = {
- for (doc_view <- Document_View.get(text_area)) {
- val rendering = doc_view.get_rendering()
+ for (rendering <- Document_View.get_rendering(text_area)) {
val caret_range = JEdit_Lib.caret_range(text_area)
val buffer_range = JEdit_Lib.buffer_range(text_area.getBuffer)
val active_focus = rendering.caret_focus_ranges(caret_range, buffer_range)
@@ -431,8 +429,7 @@
def antiquoted_cartouche(text_area: TextArea): Unit = {
val buffer = text_area.getBuffer
for {
- doc_view <- Document_View.get(text_area)
- rendering = doc_view.get_rendering()
+ rendering <- Document_View.get_rendering(text_area)
caret_range = JEdit_Lib.caret_range(text_area)
antiq_range <- rendering.antiquoted(caret_range)
antiq_text <- JEdit_Lib.get_text(buffer, antiq_range)
@@ -461,8 +458,7 @@
def update_dictionary(text_area: JEditTextArea, include: Boolean, permanent: Boolean): Unit = {
for {
spell_checker <- PIDE.plugin.spell_checker.get
- doc_view <- Document_View.get(text_area)
- rendering = doc_view.get_rendering()
+ rendering <- Document_View.get_rendering(text_area)
range = JEdit_Lib.caret_range(text_area)
Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
} {
@@ -527,8 +523,7 @@
val painter = text_area.getPainter
val caret_range = JEdit_Lib.caret_range(text_area)
for {
- doc_view <- Document_View.get(text_area)
- rendering = doc_view.get_rendering()
+ rendering <- Document_View.get_rendering(text_area)
tip <- rendering.tooltip(caret_range, control)
loc0 <- Option(text_area.offsetToXY(caret_range.start))
} {
@@ -551,8 +546,7 @@
GUI_Thread.require {}
val text_area = view.getTextArea
- for (doc_view <- Document_View.get(text_area)) {
- val rendering = doc_view.get_rendering()
+ for (rendering <- Document_View.get_rendering(text_area)) {
val errs = rendering.errors(range).filterNot(_.range.overlaps(avoid_range))
get(errs) match {
case Some(err) =>
--- a/src/Tools/jEdit/src/jedit_editor.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/jEdit/src/jedit_editor.scala Sat Dec 24 15:35:43 2022 +0000
@@ -67,18 +67,13 @@
/* current situation */
override def current_node(view: View): Option[Document.Node.Name] =
- GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) }
+ GUI_Thread.require { Document_Model.get_model(view.getBuffer).map(_.node_name) }
override def current_node_snapshot(view: View): Option[Document.Snapshot] =
- GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.snapshot()) }
+ GUI_Thread.require { Document_Model.get_snapshot(view.getBuffer) }
- override def node_snapshot(name: Document.Node.Name): Document.Snapshot = {
- GUI_Thread.require {}
- Document_Model.get(name) match {
- case Some(model) => model.snapshot()
- case None => session.snapshot(name)
- }
- }
+ override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
+ GUI_Thread.require { Document_Model.get_snapshot(name) getOrElse session.snapshot(name) }
override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] = {
GUI_Thread.require {}
@@ -90,7 +85,7 @@
case Some(doc_view) if doc_view.model.is_theory =>
snapshot.current_command(doc_view.model.node_name, text_area.getCaretPosition)
case _ =>
- Document_Model.get(buffer) match {
+ Document_Model.get_model(buffer) match {
case Some(model) if !model.is_theory =>
snapshot.version.nodes.commands_loading(model.node_name).headOption
case _ => None
--- a/src/Tools/jEdit/src/jedit_resources.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/jEdit/src/jedit_resources.scala Sat Dec 24 15:35:43 2022 +0000
@@ -86,7 +86,7 @@
}
def get_file_content(node_name: Document.Node.Name): Option[String] =
- Document_Model.get(node_name) match {
+ Document_Model.get_model(node_name) match {
case Some(model: Buffer_Model) => Some(JEdit_Lib.buffer_text(model.buffer))
case Some(model: File_Model) => Some(model.content.text)
case None => read_file_content(node_name)
@@ -94,7 +94,7 @@
override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = {
GUI_Thread.now {
- Document_Model.get(name) match {
+ Document_Model.get_model(name) match {
case Some(model: Buffer_Model) =>
JEdit_Lib.buffer_lock(model.buffer) { Some(f(JEdit_Lib.buffer_reader(model.buffer))) }
case Some(model: File_Model) => Some(f(Scan.char_reader(model.content.text)))
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala Sat Dec 24 15:35:43 2022 +0000
@@ -38,8 +38,7 @@
val result =
for {
spell_checker <- PIDE.plugin.spell_checker.get
- doc_view <- Document_View.get(text_area)
- rendering = doc_view.get_rendering()
+ rendering <- Document_View.get_rendering(text_area)
range = JEdit_Lib.point_range(text_area.getBuffer, offset)
Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
} yield (spell_checker, word)
--- a/src/Tools/jEdit/src/main_plugin.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/jEdit/src/main_plugin.scala Sat Dec 24 15:35:43 2022 +0000
@@ -27,12 +27,12 @@
def maybe_snapshot(view: View = null): Option[Document.Snapshot] = GUI_Thread.now {
val buffer = JEdit_Lib.jedit_view(view).getBuffer
- Document_Model.get(buffer).map(_.snapshot())
+ Document_Model.get_snapshot(buffer)
}
def maybe_rendering(view: View = null): Option[JEdit_Rendering] = GUI_Thread.now {
val text_area = JEdit_Lib.jedit_view(view).getTextArea
- Document_View.get(text_area).map(_.get_rendering())
+ Document_View.get_rendering(text_area)
}
def snapshot(view: View = null): Document.Snapshot =
@@ -113,12 +113,11 @@
val models = Document_Model.get_models()
val thy_files =
- resources.resolve_dependencies(models,
- PIDE.editor.document_required().map((_, Position.none)))
+ resources.resolve_dependencies(models.values, PIDE.editor.document_required())
val aux_files =
if (resources.auto_resolve) {
- session.stable_tip_version(models) match {
+ session.stable_tip_version(models.values) match {
case Some(version) => resources.undefined_blobs(version)
case None => delay_load.invoke(); Nil
}
@@ -236,7 +235,7 @@
def init_view(buffer: Buffer, text_area: JEditTextArea): Unit =
GUI_Thread.now {
JEdit_Lib.buffer_lock(buffer) {
- Document_Model.get(buffer) match {
+ Document_Model.get_model(buffer) match {
case Some(model) => Document_View.init(model, text_area)
case None =>
}
--- a/src/Tools/jEdit/src/text_overview.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/jEdit/src/text_overview.scala Sat Dec 24 15:35:43 2022 +0000
@@ -82,7 +82,7 @@
doc_view.rich_text_area.robust_body(()) {
JEdit_Lib.buffer_lock(buffer) {
- val rendering = doc_view.get_rendering()
+ val rendering = Document_View.rendering(doc_view)
val overview = get_overview()
if (rendering.snapshot.is_outdated || overview != current_overview) {
@@ -118,7 +118,7 @@
if (!doc_view.rich_text_area.check_robust_body) invoke()
else {
JEdit_Lib.buffer_lock(buffer) {
- val rendering = doc_view.get_rendering()
+ val rendering = Document_View.rendering(doc_view)
val overview = get_overview()
if (rendering.snapshot.is_outdated || is_running()) invoke()
--- a/src/Tools/jEdit/src/text_structure.scala Fri Dec 23 11:12:19 2022 +0000
+++ b/src/Tools/jEdit/src/text_structure.scala Sat Dec 24 15:35:43 2022 +0000
@@ -92,8 +92,8 @@
GUI_Thread.now {
(for {
text_area <- JEdit_Lib.jedit_text_areas(buffer)
- doc_view <- Document_View.get(text_area)
- } yield doc_view.get_rendering()).nextOption()
+ rendering <- Document_View.get_rendering(text_area)
+ } yield rendering).nextOption()
}
else None
val limit = PIDE.options.value.int("jedit_indent_script_limit")