# HG changeset patch
# User wenzelm
# Date 1620656775 -7200
# Node ID 0476728f28878cfd971be2688c9f95f769b34dbd
# Parent  1bd3463e30b8361b92ddd9811080f05737f49a72# Parent  26a1d66b9077bb29af1b9c416ddc26a67bc82930
merged

diff -r 1bd3463e30b8 -r 0476728f2887 Admin/components/components.sha1
--- 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
diff -r 1bd3463e30b8 -r 0476728f2887 Admin/components/main
--- 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
diff -r 1bd3463e30b8 -r 0476728f2887 src/HOL/Algebra/Finite_Extensions.thy
--- 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:
diff -r 1bd3463e30b8 -r 0476728f2887 src/HOL/Data_Structures/Interval_Tree.thy
--- 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"
diff -r 1bd3463e30b8 -r 0476728f2887 src/HOL/Datatype_Examples/FAE_Sequence.thy
--- 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')"
diff -r 1bd3463e30b8 -r 0476728f2887 src/HOL/Datatype_Examples/Regex_ACIDZ.thy
--- 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
diff -r 1bd3463e30b8 -r 0476728f2887 src/HOL/Hoare/Hoare_Logic_Abort.thy
--- 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"
diff -r 1bd3463e30b8 -r 0476728f2887 src/HOL/Homology/Simplices.thy
--- 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
 
diff -r 1bd3463e30b8 -r 0476728f2887 src/HOL/Library/Float.thy
--- 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
diff -r 1bd3463e30b8 -r 0476728f2887 src/HOL/Library/Interval_Float.thy
--- 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
 
 
diff -r 1bd3463e30b8 -r 0476728f2887 src/HOL/Library/Poly_Mapping.thy
--- 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 -
diff -r 1bd3463e30b8 -r 0476728f2887 src/HOL/Library/Ramsey.thy
--- 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"
diff -r 1bd3463e30b8 -r 0476728f2887 src/HOL/ROOT
--- 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
diff -r 1bd3463e30b8 -r 0476728f2887 src/Pure/Admin/build_cygwin.scala
--- 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
       })
   }
diff -r 1bd3463e30b8 -r 0476728f2887 src/Pure/Admin/build_fonts.scala
--- 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
diff -r 1bd3463e30b8 -r 0476728f2887 src/Pure/Admin/build_jedit.scala
--- /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)
+    })
+}
diff -r 1bd3463e30b8 -r 0476728f2887 src/Pure/Admin/build_spass.scala
--- 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 */
diff -r 1bd3463e30b8 -r 0476728f2887 src/Pure/Admin/build_vampire.scala
--- 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 =>
     {
diff -r 1bd3463e30b8 -r 0476728f2887 src/Pure/General/date.scala
--- 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
diff -r 1bd3463e30b8 -r 0476728f2887 src/Pure/System/isabelle_system.scala
--- 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
diff -r 1bd3463e30b8 -r 0476728f2887 src/Pure/System/isabelle_tool.scala
--- 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,
diff -r 1bd3463e30b8 -r 0476728f2887 src/Pure/build-jars
--- 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
diff -r 1bd3463e30b8 -r 0476728f2887 src/Tools/jEdit/lib/Tools/jedit
--- 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[@]}"
diff -r 1bd3463e30b8 -r 0476728f2887 src/Tools/jEdit/patches/accelerator_font
--- 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);
  			}
diff -r 1bd3463e30b8 -r 0476728f2887 src/Tools/jEdit/patches/docking
--- 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
diff -r 1bd3463e30b8 -r 0476728f2887 src/Tools/jEdit/patches/extended_styles
--- 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 @@
  			}
  		}
diff -r 1bd3463e30b8 -r 0476728f2887 src/Tools/jEdit/patches/folding
--- 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();
diff -r 1bd3463e30b8 -r 0476728f2887 src/Tools/jEdit/patches/panel_font
--- 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;
diff -r 1bd3463e30b8 -r 0476728f2887 src/Tools/jEdit/patches/props
--- 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
diff -r 1bd3463e30b8 -r 0476728f2887 src/Tools/jEdit/patches/putenv
--- 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);
  
diff -r 1bd3463e30b8 -r 0476728f2887 src/Tools/jEdit/patches/title
--- 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();
diff -r 1bd3463e30b8 -r 0476728f2887 src/Tools/jEdit/patches/vfs_manager
--- 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)
diff -r 1bd3463e30b8 -r 0476728f2887 src/Tools/jEdit/patches/vfs_marker
--- 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 @@
  	} //}}}
  
diff -r 1bd3463e30b8 -r 0476728f2887 src/Tools/jEdit/src/jedit_lib.scala
--- 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