--- 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 @@
} //}}}