--- a/Admin/components/components.sha1 Thu Jul 08 14:20:36 2021 +0200
+++ b/Admin/components/components.sha1 Thu Jul 08 16:27:35 2021 +0200
@@ -210,6 +210,7 @@
0bdbd36eda5992396e9c6b66aa24259d4dd7559c jedit_build-20210201.tar.gz
a0744f1948abdde4bfb51dd4769b619e7444baf1 jedit_build-20210510-1.tar.gz
837d6c8f72ecb21ad59a2544c69aadc9f05684c6 jedit_build-20210510.tar.gz
+7bdae3d24b10261f6cb277446cf9ecab6062bd6f jedit_build-20210708.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 Thu Jul 08 14:20:36 2021 +0200
+++ b/Admin/components/main Thu Jul 08 16:27:35 2021 +0200
@@ -10,7 +10,7 @@
isabelle_fonts-20210322
isabelle_setup-20210701
jdk-15.0.2+7
-jedit_build-20210510-1
+jedit_build-20210708
jfreechart-1.5.1
jortho-1.0-2
kodkodi-1.5.6-1
--- a/src/Pure/Admin/build_jedit.scala Thu Jul 08 14:20:36 2021 +0200
+++ b/src/Pure/Admin/build_jedit.scala Thu Jul 08 16:27:35 2021 +0200
@@ -614,9 +614,10 @@
File.write(etc_dir + Path.explode("settings"),
"""# -*- shell-script -*- :mode=shellscript:
-ISABELLE_JEDIT_BUILD_HOME="$COMPONENT"
-ISABELLE_JEDIT_BUILD_VERSION=""" + quote(jedit_patched) + """
-""")
+ISABELLE_JEDIT_HOME="$COMPONENT/""" + jedit_patched + """"
+ISABELLE_JEDIT_JARS=""" +
+ File.read_dir(jars_dir).map("$ISABELLE_JEDIT_HOME/jars/" + _).mkString("\"", ":", "\"\n")
+)
/* README */
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Jul 08 14:20:36 2021 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Jul 08 16:27:35 2021 +0200
@@ -257,12 +257,11 @@
declare -a TARGET_DEPS=("lib/classes/Pure.jar" "$TARGET_DIR/jedit.jar")
-if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
- for DEP in "$ISABELLE_JEDIT_BUILD_HOME/$ISABELLE_JEDIT_BUILD_VERSION"/jars/*.jar
- do
- TARGET_DEPS["${#TARGET_DEPS[@]}"]="$TARGET_DIR/jars/$(basename "$DEP")"
- done
-fi
+splitarray ":" "$ISABELLE_JEDIT_JARS"
+for DEP in "${SPLITARRAY[@]}"
+do
+ TARGET_DEPS["${#TARGET_DEPS[@]}"]="$TARGET_DIR/jars/$(basename "$DEP")"
+done
function target_shasum()
(
@@ -315,13 +314,10 @@
if [ -e "$ISABELLE_HOME/Admin/build" -a "$?" -ne 0 ]; then
echo "### Building Isabelle/jEdit ..."
- [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
- fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component"
-
target_clean || failed
mkdir -p "$TARGET_DIR" || failed
- cp -p -R "$ISABELLE_JEDIT_BUILD_HOME/$ISABELLE_JEDIT_BUILD_VERSION/." "$TARGET_DIR/."
+ cp -p -R "$ISABELLE_JEDIT_HOME/." "$TARGET_DIR/."
init_resources "${RESOURCES0[@]}"
compile_sources "${SOURCES0[@]}"
--- a/src/Tools/jEdit/src/plugin.scala Thu Jul 08 14:20:36 2021 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Thu Jul 08 16:27:35 2021 +0200
@@ -496,3 +496,4 @@
PIDE.editor.shutdown()
}
}
+