build auxiliary jEdit component in Isabelle/Scala;
authorwenzelm
Mon, 10 May 2021 12:23:30 +0200
changeset 73909 d9823224fcfe
parent 73908 d5c3eee7da74
child 73910 6e85281177df
build auxiliary jEdit component in Isabelle/Scala; clarified directory layout;
Admin/components/components.sha1
Admin/components/main
src/Pure/Admin/build_jedit.scala
src/Pure/System/isabelle_tool.scala
src/Pure/build-jars
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/patches/accelerator_font
src/Tools/jEdit/patches/docking
src/Tools/jEdit/patches/extended_styles
src/Tools/jEdit/patches/folding
src/Tools/jEdit/patches/panel_font
src/Tools/jEdit/patches/props
src/Tools/jEdit/patches/putenv
src/Tools/jEdit/patches/title
src/Tools/jEdit/patches/vfs_manager
src/Tools/jEdit/patches/vfs_marker
--- a/Admin/components/components.sha1	Sat May 08 13:06:30 2021 +0200
+++ b/Admin/components/components.sha1	Mon May 10 12:23:30 2021 +0200
@@ -205,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	Sat May 08 13:06:30 2021 +0200
+++ b/Admin/components/main	Mon May 10 12:23:30 2021 +0200
@@ -9,7 +9,7 @@
 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
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_jedit.scala	Mon May 10 12:23:30 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/System/isabelle_tool.scala	Sat May 08 13:06:30 2021 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Mon May 10 12:23:30 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	Sat May 08 13:06:30 2021 +0200
+++ b/src/Pure/build-jars	Mon May 10 12:23:30 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	Sat May 08 13:06:30 2021 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Mon May 10 12:23:30 2021 +0200
@@ -253,20 +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"
-  "jsr305-2.0.0.jar"
-)
-
 
 # target
 
@@ -278,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()
@@ -340,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	Sat May 08 13:06:30 2021 +0200
+++ b/src/Tools/jEdit/patches/accelerator_font	Mon May 10 12:23:30 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	Sat May 08 13:06:30 2021 +0200
+++ b/src/Tools/jEdit/patches/docking	Mon May 10 12:23:30 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	Sat May 08 13:06:30 2021 +0200
+++ b/src/Tools/jEdit/patches/extended_styles	Mon May 10 12:23:30 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	Sat May 08 13:06:30 2021 +0200
+++ b/src/Tools/jEdit/patches/folding	Mon May 10 12:23:30 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	Sat May 08 13:06:30 2021 +0200
+++ b/src/Tools/jEdit/patches/panel_font	Mon May 10 12:23:30 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	Sat May 08 13:06:30 2021 +0200
+++ b/src/Tools/jEdit/patches/props	Mon May 10 12:23:30 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	Sat May 08 13:06:30 2021 +0200
+++ b/src/Tools/jEdit/patches/putenv	Mon May 10 12:23:30 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	Sat May 08 13:06:30 2021 +0200
+++ b/src/Tools/jEdit/patches/title	Mon May 10 12:23:30 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	Sat May 08 13:06:30 2021 +0200
+++ b/src/Tools/jEdit/patches/vfs_manager	Mon May 10 12:23:30 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	Sat May 08 13:06:30 2021 +0200
+++ b/src/Tools/jEdit/patches/vfs_marker	Mon May 10 12:23:30 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 @@
  	} //}}}