# HG changeset patch
# User wenzelm
# Date 1625754455 -7200
# Node ID 75b29d65228e12b07cef737391a92519a8894dc0
# Parent  4d4c806cb7c8ce57babfd3e3133842eabab85dc9
clarified component settings;

diff -r 4d4c806cb7c8 -r 75b29d65228e Admin/components/components.sha1
--- 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
diff -r 4d4c806cb7c8 -r 75b29d65228e Admin/components/main
--- 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
diff -r 4d4c806cb7c8 -r 75b29d65228e src/Pure/Admin/build_jedit.scala
--- 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 */
diff -r 4d4c806cb7c8 -r 75b29d65228e src/Tools/jEdit/lib/Tools/jedit
--- 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[@]}"
diff -r 4d4c806cb7c8 -r 75b29d65228e src/Tools/jEdit/src/plugin.scala
--- 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()
   }
 }
+