--- a/Admin/components/components.sha1 Sun May 09 05:48:50 2021 +0000
+++ b/Admin/components/components.sha1 Mon May 10 16:26:15 2021 +0200
@@ -92,6 +92,7 @@
7ca3e6a8c9bd837990e64d89e7fa07a7e7cf78ff flatlaf-1.0.tar.gz
f339234ec18369679be0095264e0c0af7762f351 gnu-utils-20210414.tar.gz
683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz
+989234b3799fe8750f3c24825d1f717c24fb0214 idea-icons-20210508.tar.gz
20b53cfc3ffc5b15c1eabc91846915b49b4c0367 isabelle_fonts-20151021.tar.gz
736844204b2ef83974cd9f0a215738b767958c41 isabelle_fonts-20151104.tar.gz
9502c1aea938021f154adadff254c5c55da344bd isabelle_fonts-20151106.tar.gz
@@ -204,6 +205,7 @@
533b1ee6459f59bcbe4f09e214ad2cb990fb6952 jedit_build-20200908.tar.gz
f9966b5ed26740bb5b8bddbfe947fcefaea43d4d jedit_build-20201223.tar.gz
0bdbd36eda5992396e9c6b66aa24259d4dd7559c jedit_build-20210201.tar.gz
+837d6c8f72ecb21ad59a2544c69aadc9f05684c6 jedit_build-20210510.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
d911f63a5c9b4c7335bb73f805cb1711ce017a84 jfreechart-1.5.0.tar.gz
--- a/Admin/components/main Sun May 09 05:48:50 2021 +0000
+++ b/Admin/components/main Mon May 10 16:26:15 2021 +0200
@@ -6,9 +6,10 @@
cvc4-1.8
e-2.5-1
flatlaf-1.0
+idea-icons-20210508
isabelle_fonts-20210322
jdk-15.0.2+7
-jedit_build-20210201
+jedit_build-20210510
jfreechart-1.5.1
jortho-1.0-2
kodkodi-1.5.6-1
--- a/src/HOL/Algebra/Finite_Extensions.thy Sun May 09 05:48:50 2021 +0000
+++ b/src/HOL/Algebra/Finite_Extensions.thy Mon May 10 16:26:15 2021 +0200
@@ -616,15 +616,33 @@
using assms simple_extension_is_subring by (induct xs) (auto)
corollary (in domain) finite_extension_mem:
- assumes "subring K R" "set xs \<subseteq> carrier R" shows "set xs \<subseteq> finite_extension K xs"
-proof -
- { fix x xs assume "x \<in> carrier R" "set xs \<subseteq> carrier R"
- hence "x \<in> finite_extension K (x # xs)"
- using simple_extension_mem[OF finite_extension_is_subring[OF assms(1), of xs]] by simp }
- note aux_lemma = this
- show ?thesis
- using aux_lemma finite_extension_incl_aux[OF subringE(1)[OF assms(1)]] assms(2)
- by (induct xs) (simp, smt insert_subset list.simps(15) subset_trans)
+ assumes subring: "subring K R"
+ shows "set xs \<subseteq> carrier R \<Longrightarrow> set xs \<subseteq> finite_extension K xs"
+proof (induct xs)
+ case Nil
+ then show ?case by simp
+next
+ case (Cons a xs)
+ from Cons(2) have a: "a \<in> carrier R" and xs: "set xs \<subseteq> carrier R" by auto
+ show ?case
+ proof
+ fix x assume "x \<in> set (a # xs)"
+ then consider "x = a" | "x \<in> set xs" by auto
+ then show "x \<in> finite_extension K (a # xs)"
+ proof cases
+ case 1
+ with a have "x \<in> carrier R" by simp
+ with xs have "x \<in> finite_extension K (x # xs)"
+ using simple_extension_mem[OF finite_extension_is_subring[OF subring]] by simp
+ with 1 show ?thesis by simp
+ next
+ case 2
+ with Cons have *: "x \<in> finite_extension K xs" by auto
+ from a xs have "finite_extension K xs \<subseteq> finite_extension K (a # xs)"
+ by (rule finite_extension_incl_aux[OF subringE(1)[OF subring]])
+ with * show ?thesis by auto
+ qed
+ qed
qed
corollary (in domain) finite_extension_minimal:
--- a/src/HOL/Data_Structures/Interval_Tree.thy Sun May 09 05:48:50 2021 +0000
+++ b/src/HOL/Data_Structures/Interval_Tree.thy Mon May 10 16:26:15 2021 +0200
@@ -50,7 +50,7 @@
show b: "x \<le> x"
by (simp add: ivl_less_eq)
show c: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
- by (smt ivl_less_eq dual_order.trans less_trans)
+ using ivl_less_eq by fastforce
show d: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
using ivl_less_eq a ivl_inj ivl_less by fastforce
show e: "x \<le> y \<or> y \<le> x"
--- a/src/HOL/Datatype_Examples/FAE_Sequence.thy Sun May 09 05:48:50 2021 +0000
+++ b/src/HOL/Datatype_Examples/FAE_Sequence.thy Mon May 10 16:26:15 2021 +0200
@@ -114,7 +114,10 @@
lemma fseq_at_infinite_Inr:
"\<lbrakk>infinite (fseq_at f x); fseq_eq (map_fseq Inr f) g\<rbrakk> \<Longrightarrow> \<exists>x'\<in>set_fseq g. x \<in> Basic_BNFs.setr x'"
- by transfer(auto simp add: seq_at_def vimage_def; smt (z3) finite_nat_set_iff_bounded_le mem_Collect_eq setr.intros)
+ apply transfer
+ apply (auto simp add: seq_at_def vimage_def)
+ apply (smt (verit, ccfv_SIG) finite_subset mem_Collect_eq setr.simps subsetI)
+ done
lemma fseq_at_Inr_infinite:
assumes "\<And>g. fseq_eq (map_fseq Inr f) g \<longrightarrow> (\<exists>x'\<in>set_fseq g. x \<in> Basic_BNFs.setr x')"
--- a/src/HOL/Datatype_Examples/Regex_ACIDZ.thy Sun May 09 05:48:50 2021 +0000
+++ b/src/HOL/Datatype_Examples/Regex_ACIDZ.thy Mon May 10 16:26:15 2021 +0200
@@ -204,7 +204,7 @@
next
case (d r t)
then show ?case
- by (smt (z3) ACIDZ.d R distribute.simps(3) elim_zeros.simps(2) elim_zeros.simps(3) elim_zeros_distribute_idem z)
+ by (smt (verit, ccfv_SIG) ACIDZ.d R elim_zeros.simps(2) elim_zeros_distribute_Zero elim_zeros_distribute_idem z)
next
case (A r r' s s')
then show ?case
@@ -212,7 +212,7 @@
next
case (C r r' s)
then show ?case
- by (smt (z3) ACIDZ.C elim_zeros.simps(2,3) z elim_zeros_ACIDZ_Zero)
+ by (smt (verit, best) ACIDZ.C R elim_zeros.simps(2) elim_zeros_ACIDZ_Zero z)
qed (auto simp: Let_def)
lemma AA': "r ~ r' \<Longrightarrow> s ~ s' \<Longrightarrow> t = elim_zeros (Alt r' s') \<Longrightarrow> Alt r s ~ t"
@@ -437,7 +437,7 @@
qed
private lemma CZ: "Conc Zero r ~~ Zero"
- by (smt (z3) R elim_zeros.simps(2) elim_zeros.simps(3) r_into_equivclp z)
+ by (metis R distribute.simps(3) elim_zeros.simps(3) elim_zeros_distribute_Zero r_into_equivclp z)
private lemma AZ: "Alt Zero r ~~ r"
by (smt (verit, ccfv_threshold) converse_r_into_equivclp converse_rtranclp_into_rtranclp
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy Sun May 09 05:48:50 2021 +0000
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Mon May 10 16:26:15 2021 +0200
@@ -62,7 +62,7 @@
lemma tc_implies_pc:
"ValidTC p c q \<Longrightarrow> Valid p c q"
- by (smt Sem_deterministic ValidTC_def Valid_def image_iff)
+ by (smt (verit) Sem_deterministic ValidTC_def Valid_def image_iff)
lemma tc_extract_function:
"ValidTC p c q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
--- a/src/HOL/Homology/Simplices.thy Sun May 09 05:48:50 2021 +0000
+++ b/src/HOL/Homology/Simplices.thy Mon May 10 16:26:15 2021 +0200
@@ -2347,7 +2347,8 @@
show "chain_boundary (Suc p) (?h p c) + ?h (p - Suc 0) (chain_boundary p c) = (singular_subdivision p ^^ Suc n) c - c"
using chain_boundary_singular_subdivision [of "Suc p" X]
apply (simp add: chain_boundary_add f5 h k algebra_simps)
- by (smt add.assoc add.commute diff_add_cancel h(4) k(4) sc singular_subdivision_add)
+ apply (smt (verit, ccfv_threshold) add.commute add_diff_eq diff_add_cancel diff_diff_eq2 h(4) k(4) sc singular_subdivision_add)
+ done
qed (auto simp: k h singular_subdivision_diff)
qed
--- a/src/HOL/Library/Float.thy Sun May 09 05:48:50 2021 +0000
+++ b/src/HOL/Library/Float.thy Mon May 10 16:26:15 2021 +0200
@@ -2122,7 +2122,7 @@
proof cases
assume [simp]: "even j"
have "a * power_down prec a j \<le> b * power_down prec b j"
- by (smt IH(1) IH(2) \<open>even j\<close> lessI mult_mono' mult_mono_nonpos_nonneg power_down_even_nonneg)
+ by (metis IH(1) IH(2) \<open>even j\<close> lessI linear mult_mono mult_mono' mult_mono_nonpos_nonneg power_down_even_nonneg)
then have "truncate_down (Suc prec) (a * power_down prec a j) \<le> truncate_down (Suc prec) (b * power_down prec b j)"
by (auto intro!: truncate_down_mono simp: abs_le_square_iff[symmetric] abs_real_def)
then show ?thesis
@@ -2193,7 +2193,7 @@
proof cases
assume [simp]: "even j"
have "a * power_up prec a j \<le> b * power_up prec b j"
- by (smt IH(1) IH(2) \<open>even j\<close> lessI mult_mono' mult_mono_nonpos_nonneg power_up_even_nonneg)
+ by (metis IH(1) IH(2) \<open>even j\<close> lessI linear mult_mono mult_mono' mult_mono_nonpos_nonneg power_up_even_nonneg)
then have "truncate_up prec (a * power_up prec a j) \<le> truncate_up prec (b * power_up prec b j)"
by (auto intro!: truncate_up_mono simp: abs_le_square_iff[symmetric] abs_real_def)
then show ?thesis
--- a/src/HOL/Library/Interval_Float.thy Sun May 09 05:48:50 2021 +0000
+++ b/src/HOL/Library/Interval_Float.thy Mon May 10 16:26:15 2021 +0200
@@ -298,7 +298,7 @@
using Cons(1)[OF \<open>xs all_in Is\<close>]
split_correct[OF \<open>x' \<in>\<^sub>r I\<close>]
apply (auto simp add: list_ex_iff set_of_eq)
- by (smt length_Cons less_Suc_eq_0_disj nth_Cons_0 nth_Cons_Suc x_decomp)
+ by (smt (verit, ccfv_SIG) One_nat_def Suc_pred \<open>x \<noteq> []\<close> le_simps(3) length_greater_0_conv length_tl linorder_not_less list.sel(3) neq0_conv nth_Cons' x_decomp)
qed simp
--- a/src/HOL/Library/Poly_Mapping.thy Sun May 09 05:48:50 2021 +0000
+++ b/src/HOL/Library/Poly_Mapping.thy Mon May 10 16:26:15 2021 +0200
@@ -1796,7 +1796,7 @@
lemma keys_frag_extend: "Poly_Mapping.keys(frag_extend f c) \<subseteq> (\<Union>x \<in> Poly_Mapping.keys c. Poly_Mapping.keys(f x))"
unfolding frag_extend_def
- by (smt SUP_mono' keys_cmul keys_sum order_trans)
+ using keys_sum by fastforce
lemma frag_expansion: "a = frag_extend frag_of a"
proof -
--- a/src/HOL/Library/Ramsey.thy Sun May 09 05:48:50 2021 +0000
+++ b/src/HOL/Library/Ramsey.thy Mon May 10 16:26:15 2021 +0200
@@ -595,7 +595,7 @@
then obtain u where u: "bij_betw u {..<q} U"
using ex_bij_betw_nat_finite lessThan_atLeast0 by (fastforce simp add: nsets_def)
then have Usub: "U \<subseteq> {..<p}"
- by (smt \<open>U \<in> nsets {..<p} q\<close> mem_Collect_eq nsets_def)
+ by (smt (verit) U mem_Collect_eq nsets_def)
have u_nsets: "u ` X \<in> nsets {..<p} n" if "X \<in> nsets {..<q} n" for X n
proof -
have "inj_on u X"
--- a/src/HOL/ROOT Sun May 09 05:48:50 2021 +0000
+++ b/src/HOL/ROOT Mon May 10 16:26:15 2021 +0200
@@ -953,9 +953,10 @@
Boogie
SMT_Examples
SMT_Word_Examples
- SMT_Tests
+ SMT_Examples_Verit
SMT_Tests_Verit
- SMT_Examples_Verit
+ theories [condition = Z3_SOLVER]
+ SMT_Tests
session "HOL-SPARK" in "SPARK" = HOL +
sessions
--- a/src/Pure/Admin/build_cygwin.scala Sun May 09 05:48:50 2021 +0000
+++ b/src/Pure/Admin/build_cygwin.scala Mon May 10 16:26:15 2021 +0200
@@ -52,7 +52,7 @@
(cygwin + Path.explode("Cygwin.bat")).file.delete
- val archive = "cygwin-" + Date.Format("uuuuMMdd")(Date.now()) + ".tar.gz"
+ val archive = "cygwin-" + Date.Format.alt_date(Date.now()) + ".tar.gz"
Isabelle_System.gnutar("-czf " + Bash.string(archive) + " cygwin", dir = tmp_dir).check
})
}
--- a/src/Pure/Admin/build_fonts.scala Sun May 09 05:48:50 2021 +0000
+++ b/src/Pure/Admin/build_fonts.scala Mon May 10 16:26:15 2021 +0200
@@ -358,7 +358,7 @@
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val target_version = Date.Format("uuuuMMdd")(Date.now())
+ val target_version = Date.Format.alt_date(Date.now())
val target_dir = Path.explode("isabelle_fonts-" + target_version)
val progress = new Console_Progress
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_jedit.scala Mon May 10 16:26:15 2021 +0200
@@ -0,0 +1,207 @@
+/* Title: Pure/Admin/build_jedit.scala
+ Author: Makarius
+
+Build auxiliary jEdit component.
+*/
+
+package isabelle
+
+
+object Build_JEdit
+{
+ /* build jEdit component */
+
+ private val download_jars: List[(String, String)] =
+ List(
+ "https://repo1.maven.org/maven2/com/google/code/findbugs/jsr305/3.0.2/jsr305-3.0.2.jar" ->
+ "jsr305-3.0.2.jar")
+
+ private val download_plugins: List[(String, String)] =
+ List(
+ "Code2HTML" -> "0.7",
+ "CommonControls" -> "1.7.4",
+ "Console" -> "5.1.4",
+ "ErrorList" -> "2.4.0",
+ "Highlight" -> "2.2",
+ "Navigator" -> "2.7",
+ "SideKick" -> "1.8")
+
+ def build_jedit(
+ component_dir: Path,
+ version: String,
+ original: Boolean = false,
+ java_home: Path = default_java_home,
+ progress: Progress = new Progress): Unit =
+ {
+ Isabelle_System.require_command("ant", test = "-version")
+ Isabelle_System.require_command("patch")
+ Isabelle_System.require_command("unzip", test = "-h")
+
+ Isabelle_System.new_directory(component_dir)
+
+
+ /* jEdit directory */
+
+ val jedit = "jedit" + version
+ val jedit_patched = jedit + "-patched"
+
+ val jedit_dir = Isabelle_System.make_directory(component_dir + Path.basic(jedit))
+ val jedit_patched_dir = component_dir + Path.basic(jedit_patched)
+
+ def download_jedit(dir: Path, name: String): Path =
+ {
+ val jedit_name = jedit + name
+ val url =
+ "https://sourceforge.net/projects/jedit/files/jedit/" +
+ version + "/" + jedit_name + "/download"
+ val path = dir + Path.basic(jedit_name)
+ Isabelle_System.download_file(url, path, progress = progress)
+ path
+ }
+
+ Isabelle_System.with_tmp_dir("tmp")(tmp_dir =>
+ {
+ /* original version */
+
+ val install_path = download_jedit(tmp_dir, "install.jar")
+ Isabelle_System.bash("""export CLASSPATH=""
+isabelle_java java -Duser.home=""" + File.bash_platform_path(tmp_dir) +
+ " -jar " + File.bash_platform_path(install_path) + " auto " +
+ File.bash_platform_path(jedit_dir) + " unix-script=off unix-man=off").check
+
+ val source_path = download_jedit(tmp_dir, "source.tar.bz2")
+ Isabelle_System.gnutar("-xjf " + File.bash_path(source_path), dir = jedit_dir).check
+
+
+ /* patched version */
+
+ Isabelle_System.copy_dir(jedit_dir, jedit_patched_dir)
+
+ val source_dir = jedit_patched_dir + Path.basic("jEdit")
+ val tmp_source_dir = tmp_dir + Path.basic("jEdit")
+
+ progress.echo("Patching jEdit sources ...")
+ for {
+ file <- File.find_files(Path.explode("~~/src/Tools/jEdit/patches").file).iterator
+ name = file.getName
+ if !name.endsWith("~") && !name.endsWith(".orig")
+ } {
+ progress.bash("patch -p2 < " + File.bash_path(File.path(file)),
+ cwd = source_dir.file, echo = true).check
+ }
+
+ progress.echo("Building jEdit ...")
+ Isabelle_System.copy_dir(source_dir, tmp_source_dir)
+ progress.bash("env JAVA_HOME=" + File.bash_platform_path(java_home) + " ant",
+ cwd = tmp_source_dir.file, echo = true).check
+ Isabelle_System.copy_file(tmp_source_dir + Path.explode("build/jedit.jar"), jedit_patched_dir)
+ })
+
+
+ /* jars */
+
+ val jars_dir = Isabelle_System.make_directory(jedit_patched_dir + Path.basic("jars"))
+
+ for { (url, name) <- download_jars } {
+ Isabelle_System.download_file(url, jars_dir + Path.basic(name), progress = progress)
+ }
+
+ for { (name, vers) <- download_plugins } {
+ Isabelle_System.with_tmp_file("tmp", ext = "zip")(zip_path =>
+ {
+ val url =
+ "https://sourceforge.net/projects/jedit-plugins/files/" + name + "/" + vers + "/" +
+ name + "-" + vers + "-bin.zip/download"
+ Isabelle_System.download_file(url, zip_path, progress = progress)
+ Isabelle_System.bash("unzip -x " + File.bash_path(zip_path), cwd = jars_dir.file).check
+ })
+ }
+
+
+
+ /* diff */
+
+ Isabelle_System.bash(
+ "diff -ru " + Bash.string(jedit) + " " + Bash.string(jedit_patched) +
+ " > " + Bash.string(jedit + ".patch"),
+ cwd = component_dir.file).check_rc(_ <= 1)
+
+ if (!original) Isabelle_System.rm_tree(jedit_dir)
+
+
+ /* doc */
+
+ val doc_dir = Isabelle_System.make_directory(component_dir + Path.explode("doc"))
+
+ download_jedit(doc_dir, "manual-a4.pdf")
+ download_jedit(doc_dir, "manual-letter.pdf")
+
+
+ /* etc */
+
+ val etc_dir = Isabelle_System.make_directory(component_dir + Path.explode("etc"))
+
+ File.write(etc_dir + Path.explode("settings"),
+ """# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_JEDIT_BUILD_HOME="$COMPONENT"
+ISABELLE_JEDIT_BUILD_VERSION=""" + quote(jedit_patched) + """
+""")
+
+
+ /* README */
+
+ File.write(component_dir + Path.basic("README"),
+"""This is a slightly patched version of jEdit """ + version + """ from
+https://sourceforge.net/projects/jedit/files/jedit with some
+additional plugins jars from
+https://sourceforge.net/projects/jedit-plugins/files
+
+
+ Makarius
+ """ + Date.Format.date(Date.now()) + "\n")
+ }
+
+
+
+ /** Isabelle tool wrappers **/
+
+ val default_version = "5.6.0"
+ def default_java_home: Path = Path.explode("$JAVA_HOME").expand
+
+ val isabelle_tool =
+ Isabelle_Tool("build_jedit", "build auxiliary jEdit component", Scala_Project.here, args =>
+ {
+ var target_dir = Path.current
+ var java_home = default_java_home
+ var original = false
+ var version = default_version
+
+ val getopts = Getopts("""
+Usage: isabelle build_jedit [OPTIONS]
+
+ Options are:
+ -D DIR target directory (default ".")
+ -J JAVA_HOME Java version for building jedit.jar (e.g. version 11)
+ -O retain copy of original jEdit directory
+ -V VERSION jEdit version (default: """ + quote(default_version) + """)
+
+ Build auxiliary jEdit component from original sources, with some patches.
+""",
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "J:" -> (arg => java_home = Path.explode(arg)),
+ "O" -> (arg => original = true),
+ "V:" -> (arg => version = arg))
+
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
+
+ val component_dir =
+ target_dir + Path.basic("jedit_build-" + Date.Format.alt_date(Date.now()))
+
+ val progress = new Console_Progress()
+
+ build_jedit(component_dir, version, original = original,
+ java_home = java_home, progress = progress)
+ })
+}
--- a/src/Pure/Admin/build_spass.scala Sun May 09 05:48:50 2021 +0000
+++ b/src/Pure/Admin/build_spass.scala Mon May 10 16:26:15 2021 +0200
@@ -22,7 +22,8 @@
{
Isabelle_System.with_tmp_dir("build")(tmp_dir =>
{
- Isabelle_System.require_command("bison", "flex")
+ Isabelle_System.require_command("bison")
+ Isabelle_System.require_command("flex")
/* component */
--- a/src/Pure/Admin/build_vampire.scala Sun May 09 05:48:50 2021 +0000
+++ b/src/Pure/Admin/build_vampire.scala Mon May 10 16:26:15 2021 +0200
@@ -29,7 +29,8 @@
progress: Progress = new Progress,
target_dir: Path = Path.current): Unit =
{
- Isabelle_System.require_command("git", "cmake")
+ Isabelle_System.require_command("git")
+ Isabelle_System.require_command("cmake")
Isabelle_System.with_tmp_dir("build")(tmp_dir =>
{
--- a/src/Pure/General/date.scala Sun May 09 05:48:50 2021 +0000
+++ b/src/Pure/General/date.scala Mon May 10 16:26:15 2021 +0200
@@ -38,6 +38,7 @@
val default: Format = Format("dd-MMM-uuuu HH:mm:ss xx")
val date: Format = Format("dd-MMM-uuuu")
val time: Format = Format("HH:mm:ss")
+ val alt_date: Format = Format("uuuuMMdd")
}
abstract class Format private
--- a/src/Pure/System/isabelle_system.scala Sun May 09 05:48:50 2021 +0000
+++ b/src/Pure/System/isabelle_system.scala Mon May 10 16:26:15 2021 +0200
@@ -300,7 +300,7 @@
}
catch {
case ERROR(msg) =>
- cat_error("Failed top copy file " +
+ cat_error("Failed to copy file " +
File.path(src).absolute + " to " + File.path(dst).absolute, msg)
}
}
@@ -543,11 +543,9 @@
else error("Expected to find GNU tar executable")
}
- def require_command(cmds: String*): Unit =
+ def require_command(cmd: String, test: String = "--version"): Unit =
{
- for (cmd <- cmds) {
- if (!bash(Bash.string(cmd) + " --version").ok) error("Missing system command: " + quote(cmd))
- }
+ if (!bash(Bash.string(cmd) + " " + test).ok) error("Missing system command: " + quote(cmd))
}
def hostname(): String = bash("hostname -s").check.out
--- a/src/Pure/System/isabelle_tool.scala Sun May 09 05:48:50 2021 +0000
+++ b/src/Pure/System/isabelle_tool.scala Mon May 10 16:26:15 2021 +0200
@@ -220,6 +220,7 @@
Build_Fonts.isabelle_tool,
Build_JCEF.isabelle_tool,
Build_JDK.isabelle_tool,
+ Build_JEdit.isabelle_tool,
Build_PolyML.isabelle_tool1,
Build_PolyML.isabelle_tool2,
Build_SPASS.isabelle_tool,
--- a/src/Pure/build-jars Sun May 09 05:48:50 2021 +0000
+++ b/src/Pure/build-jars Mon May 10 16:26:15 2021 +0200
@@ -21,6 +21,7 @@
src/Pure/Admin/build_history.scala
src/Pure/Admin/build_jcef.scala
src/Pure/Admin/build_jdk.scala
+ src/Pure/Admin/build_jedit.scala
src/Pure/Admin/build_log.scala
src/Pure/Admin/build_polyml.scala
src/Pure/Admin/build_release.scala
--- a/src/Tools/jEdit/lib/Tools/jedit Sun May 09 05:48:50 2021 +0000
+++ b/src/Tools/jEdit/lib/Tools/jedit Mon May 10 16:26:15 2021 +0200
@@ -253,21 +253,6 @@
FRESH_BUILD=""
fi
-JEDIT_BUILD_JAR="$ISABELLE_JEDIT_BUILD_VERSION/jedit.jar"
-
-declare -a JEDIT_BUILD_JARS=(
- "Code2HTML.jar"
- "CommonControls.jar"
- "Console.jar"
- "ErrorList.jar"
- "Highlight.jar"
- "kappalayout.jar"
- "Navigator.jar"
- "SideKick.jar"
- "idea-icons.jar"
- "jsr305-2.0.0.jar"
-)
-
# target
@@ -279,9 +264,9 @@
TARGET_SHASUM="$TARGET_DIR/Isabelle-jEdit.shasum"
declare -a TARGET_DEPS=("lib/classes/Pure.jar" "$TARGET_DIR/jedit.jar")
-for DEP in "${JEDIT_BUILD_JARS[@]}"
+for DEP in "$TARGET_DIR"/jars/*.jar
do
- TARGET_DEPS["${#TARGET_DEPS[@]}"]="$TARGET_DIR/jars/$DEP"
+ TARGET_DEPS["${#TARGET_DEPS[@]}"]="$DEP"
done
function target_shasum()
@@ -341,12 +326,7 @@
target_clean || failed
mkdir -p "$TARGET_DIR" || failed
- cp -p -R "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." "$TARGET_DIR/."
-
- for DEP in "${JEDIT_BUILD_JARS[@]}"
- do
- cp -p "$ISABELLE_JEDIT_BUILD_HOME/contrib/$DEP" "$TARGET_DIR/jars/."
- done
+ cp -p -R "$ISABELLE_JEDIT_BUILD_HOME/$ISABELLE_JEDIT_BUILD_VERSION/." "$TARGET_DIR/."
init_resources "${RESOURCES0[@]}"
compile_sources "${SOURCES0[@]}"
--- a/src/Tools/jEdit/patches/accelerator_font Sun May 09 05:48:50 2021 +0000
+++ b/src/Tools/jEdit/patches/accelerator_font Mon May 10 16:26:15 2021 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/GUIUtilities.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java
---- 5.6.0/jEdit-orig/org/gjt/sp/jedit/GUIUtilities.java 2020-09-03 05:31:04.000000000 +0200
-+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/GUIUtilities.java 2020-09-08 20:13:23.561140312 +0200
+diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java
+--- jedit5.6.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2020-09-03 05:31:04.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2021-05-10 11:02:05.784257753 +0200
@@ -1130,9 +1130,7 @@
return new Font("Monospaced", Font.PLAIN, 12);
}
--- a/src/Tools/jEdit/patches/docking Sun May 09 05:48:50 2021 +0000
+++ b/src/Tools/jEdit/patches/docking Mon May 10 16:26:15 2021 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
---- 5.6.0/jEdit-orig/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2020-09-03 05:31:01.000000000 +0200
-+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2020-09-08 20:13:23.565140195 +0200
+diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
+--- jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2020-09-03 05:31:01.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2021-05-10 11:02:05.760257760 +0200
@@ -45,14 +45,15 @@
* @version $Id: FloatingWindowContainer.java 25333 2020-05-10 09:40:02Z kpouer $
* @since jEdit 4.0pre1
--- a/src/Tools/jEdit/patches/extended_styles Sun May 09 05:48:50 2021 +0000
+++ b/src/Tools/jEdit/patches/extended_styles Mon May 10 16:26:15 2021 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
---- 5.6.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 2020-09-03 05:31:01.000000000 +0200
-+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2020-09-08 20:13:23.565140195 +0200
+diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java
+--- jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2020-09-03 05:31:01.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2021-05-10 11:02:05.816257745 +0200
@@ -332,9 +332,9 @@
//{{{ Package private members
@@ -24,9 +24,9 @@
private GlyphData glyphData;
//}}}
-diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
---- 5.6.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 2020-09-03 05:31:01.000000000 +0200
-+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2020-09-08 20:13:23.569140077 +0200
+diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java
+--- jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2020-09-03 05:31:01.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2021-05-10 11:02:05.820257742 +0200
@@ -914,6 +914,11 @@
return chunkCache.getLineInfo(screenLine).physicalLine;
} //}}}
@@ -39,9 +39,9 @@
//{{{ getScreenLineOfOffset() method
/**
* Returns the screen (wrapped) line containing the specified offset.
-diff -ru 5.6.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.6.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
---- 5.6.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 2020-09-03 05:31:09.000000000 +0200
-+++ 5.6.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2020-09-08 20:13:23.569140077 +0200
+diff -ru jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java
+--- jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2020-09-03 05:31:09.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2021-05-10 11:02:05.820257742 +0200
@@ -344,8 +344,28 @@
}
}
--- a/src/Tools/jEdit/patches/folding Sun May 09 05:48:50 2021 +0000
+++ b/src/Tools/jEdit/patches/folding Mon May 10 16:26:15 2021 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java
---- 5.6.0/jEdit-orig/org/gjt/sp/jedit/buffer/JEditBuffer.java 2020-09-03 05:31:04.000000000 +0200
-+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/buffer/JEditBuffer.java 2020-09-08 20:13:23.573139959 +0200
+diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java
+--- jedit5.6.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2020-09-03 05:31:04.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java 2021-05-10 11:02:05.776257756 +0200
@@ -1968,29 +1968,23 @@
{
Segment seg = new Segment();
--- a/src/Tools/jEdit/patches/panel_font Sun May 09 05:48:50 2021 +0000
+++ b/src/Tools/jEdit/patches/panel_font Mon May 10 16:26:15 2021 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/gui/PanelWindowContainer.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java
---- 5.6.0/jEdit-orig/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2020-09-03 05:31:02.000000000 +0200
-+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2020-12-23 13:16:31.059779643 +0100
+diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java
+--- jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2020-09-03 05:31:02.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2021-05-10 11:23:04.107511056 +0200
@@ -52,6 +52,7 @@
import javax.swing.JComponent;
import javax.swing.JPanel;
--- a/src/Tools/jEdit/patches/props Sun May 09 05:48:50 2021 +0000
+++ b/src/Tools/jEdit/patches/props Mon May 10 16:26:15 2021 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6.0/jEdit-orig/org/jedit/localization/jedit_en.props 5.6.0/jEdit-patched/org/jedit/localization/jedit_en.props
---- 5.6.0/jEdit-orig/org/jedit/localization/jedit_en.props 2020-09-03 05:31:10.000000000 +0200
-+++ 5.6.0/jEdit-patched/org/jedit/localization/jedit_en.props 2020-09-08 20:13:35.644786809 +0200
+diff -ru jedit5.6.0/jEdit/org/jedit/localization/jedit_en.props jedit5.6.0-patched/jEdit/org/jedit/localization/jedit_en.props
+--- jedit5.6.0/jEdit/org/jedit/localization/jedit_en.props 2020-09-03 05:31:10.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/jedit/localization/jedit_en.props 2021-05-10 11:02:05.788257753 +0200
@@ -1277,8 +1277,7 @@
The most likely reason is that the JAR file is corrupt; try\n\
reinstalling it. See Utilities->Troubleshooting->Activity Log\n\
@@ -11,3 +11,4 @@
plugin-error.already-loaded=Two copies installed. Please remove one of the \
two copies.
plugin-error.dep-jdk=Requires Java {0} or later, but you only have version {1}.
+Binary files jedit5.6.0/jedit.jar and jedit5.6.0-patched/jedit.jar differ
--- a/src/Tools/jEdit/patches/putenv Sun May 09 05:48:50 2021 +0000
+++ b/src/Tools/jEdit/patches/putenv Mon May 10 16:26:15 2021 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/MiscUtilities.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java
---- 5.6.0/jEdit-orig/org/gjt/sp/jedit/MiscUtilities.java 2020-09-03 05:31:01.000000000 +0200
-+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java 2020-09-08 20:13:35.648786692 +0200
+diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/MiscUtilities.java
+--- jedit5.6.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2020-09-03 05:31:01.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2021-05-10 11:23:04.139510558 +0200
@@ -131,6 +131,21 @@
static final Pattern winPattern = Pattern.compile(winPatternString);
--- a/src/Tools/jEdit/patches/title Sun May 09 05:48:50 2021 +0000
+++ b/src/Tools/jEdit/patches/title Mon May 10 16:26:15 2021 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/View.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/View.java
---- 5.6.0/jEdit-orig/org/gjt/sp/jedit/View.java 2020-09-03 05:31:01.000000000 +0200
-+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/View.java 2020-09-08 20:13:35.652786577 +0200
+diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/View.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/View.java
+--- jedit5.6.0/jEdit/org/gjt/sp/jedit/View.java 2020-09-03 05:31:01.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/View.java 2021-05-10 11:02:05.792257750 +0200
@@ -1262,15 +1262,10 @@
StringBuilder title = new StringBuilder();
--- a/src/Tools/jEdit/patches/vfs_manager Sun May 09 05:48:50 2021 +0000
+++ b/src/Tools/jEdit/patches/vfs_manager Mon May 10 16:26:15 2021 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSManager.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java
---- 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSManager.java 2020-09-03 05:31:03.000000000 +0200
-+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSManager.java 2020-09-08 20:13:35.656786460 +0200
+diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSManager.java
+--- jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java 2020-09-03 05:31:03.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSManager.java 2021-05-10 11:02:05.808257746 +0200
@@ -380,6 +380,18 @@
if(vfsUpdates.size() == 1)
--- a/src/Tools/jEdit/patches/vfs_marker Sun May 09 05:48:50 2021 +0000
+++ b/src/Tools/jEdit/patches/vfs_marker Mon May 10 16:26:15 2021 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java
---- 5.6.0/jEdit-orig/org/gjt/sp/jedit/browser/VFSBrowser.java 2020-09-03 05:31:04.000000000 +0200
-+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/browser/VFSBrowser.java 2020-09-08 20:13:45.348505646 +0200
+diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java
+--- jedit5.6.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2020-09-03 05:31:04.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2021-05-10 11:02:05.824257741 +0200
@@ -1194,6 +1194,7 @@
VFSFile[] selectedFiles = browserView.getSelectedFiles();
@@ -53,9 +53,9 @@
}
Object[] listeners = listenerList.getListenerList();
-diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java
---- 5.6.0/jEdit-orig/org/gjt/sp/jedit/io/VFSFile.java 2020-09-03 05:31:03.000000000 +0200
-+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/io/VFSFile.java 2020-09-08 20:13:45.348505646 +0200
+diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java
+--- jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2020-09-03 05:31:03.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2021-05-10 11:02:05.824257741 +0200
@@ -302,6 +302,12 @@
}
} //}}}
@@ -69,9 +69,9 @@
//{{{ getPath() method
public String getPath()
{
-diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/jEdit.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java
---- 5.6.0/jEdit-orig/org/gjt/sp/jedit/jEdit.java 2020-09-03 05:31:01.000000000 +0200
-+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/jEdit.java 2020-09-08 20:13:45.348505646 +0200
+diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/jEdit.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java
+--- jedit5.6.0/jEdit/org/gjt/sp/jedit/jEdit.java 2020-09-03 05:31:01.000000000 +0200
++++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java 2021-05-10 11:02:05.824257741 +0200
@@ -4242,7 +4242,7 @@
} //}}}
--- a/src/Tools/jEdit/src/jedit_lib.scala Sun May 09 05:48:50 2021 +0000
+++ b/src/Tools/jEdit/src/jedit_lib.scala Mon May 10 16:26:15 2021 +0200
@@ -301,7 +301,7 @@
{
val name1 =
if (name.startsWith("idea-icons/")) {
- val file = Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar").file.toURI.toASCIIString
+ val file = Path.explode("$ISABELLE_IDEA_ICONS").file.toURI.toASCIIString
"jar:" + file + "!/" + name
}
else name