updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
proper update of jEdit environment -- avoid warnings in Java 11;
activate jdk-11+28;
--- a/Admin/components/components.sha1 Thu Oct 25 21:29:08 2018 +0200
+++ b/Admin/components/components.sha1 Thu Oct 25 22:42:17 2018 +0200
@@ -134,6 +134,7 @@
d806c1c26b571b5b4ef05ea11e8b9cf936518e06 jedit_build-20170319.tar.gz
7bcb202e13358dd750e964b2f747664428b5d8b3 jedit_build-20180417.tar.gz
23c8a05687d05a6937f7d600ac3aa19e3ce59c9c jedit_build-20180504.tar.gz
+9c64ee0705e5284b507ca527196081979d689519 jedit_build-20181025.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 Oct 25 21:29:08 2018 +0200
+++ b/Admin/components/main Thu Oct 25 22:42:17 2018 +0200
@@ -5,8 +5,8 @@
cvc4-1.5-4
e-2.0-2
isabelle_fonts-20180113
-jdk-8u181
-jedit_build-20180504
+jdk-11+28
+jedit_build-20181025
jfreechart-1.5.0
jortho-1.0-2
kodkodi-1.5.2-1
--- a/src/Pure/Tools/main.scala Thu Oct 25 21:29:08 2018 +0200
+++ b/src/Pure/Tools/main.scala Thu Oct 25 22:42:17 2018 +0200
@@ -90,14 +90,31 @@
}
- /* main startup */
+ /* environment */
- update_environment()
+ def putenv(name: String, value: String)
+ {
+ val misc =
+ Class.forName("org.gjt.sp.jedit.MiscUtilities", true, ClassLoader.getSystemClassLoader)
+ val putenv = misc.getMethod("putenv", classOf[String], classOf[String])
+ putenv.invoke(null, name, value)
+ }
+
+ for (name <- List("ISABELLE_HOME", "ISABELLE_HOME_USER", "JEDIT_HOME", "JEDIT_SETTINGS")) {
+ putenv(name, File.platform_path(Isabelle_System.getenv(name)))
+ }
+ putenv("ISABELLE_ROOT", null)
+
+
+ /* properties */
System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist")))
System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME")))
System.setProperty("scala.color", "false")
+
+ /* main startup */
+
val jedit =
Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)
val jedit_main = jedit.getMethod("main", classOf[Array[String]])
@@ -114,46 +131,4 @@
}
start()
}
-
-
- /* adhoc update of JVM environment variables */
-
- def update_environment()
- {
- val update =
- {
- val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME")
- val isabelle_home_user = Isabelle_System.getenv("ISABELLE_HOME_USER")
- val jedit_home = Isabelle_System.getenv("JEDIT_HOME")
- val jedit_settings = Isabelle_System.getenv("JEDIT_SETTINGS")
-
- (env0: Any) => {
- val env = env0.asInstanceOf[java.util.Map[String, String]]
- env.put("ISABELLE_HOME", File.platform_path(isabelle_home))
- env.put("ISABELLE_HOME_USER", File.platform_path(isabelle_home_user))
- env.put("JEDIT_HOME", File.platform_path(jedit_home))
- env.put("JEDIT_SETTINGS", File.platform_path(jedit_settings))
- env.remove("ISABELLE_ROOT")
- }
- }
-
- classOf[java.util.Collections].getDeclaredClasses
- .find(c => c.getName == "java.util.Collections$UnmodifiableMap") match
- {
- case Some(c) =>
- val m = c.getDeclaredField("m")
- m.setAccessible(true)
- update(m.get(System.getenv()))
-
- if (Platform.is_windows) {
- val ProcessEnvironment = Class.forName("java.lang.ProcessEnvironment")
- val field = ProcessEnvironment.getDeclaredField("theCaseInsensitiveEnvironment")
- field.setAccessible(true)
- update(field.get(null))
- }
-
- case None =>
- error("Failed to update JVM environment -- platform incompatibility")
- }
- }
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/putenv Thu Oct 25 22:42:17 2018 +0200
@@ -0,0 +1,51 @@
+diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java
+--- 5.5.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2018-04-09 01:57:06.000000000 +0200
++++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java 2018-10-25 22:06:22.258705636 +0200
+@@ -126,6 +126,20 @@
+ static final Pattern winPattern = Pattern.compile(winPatternString);
+
+
++ private static Map<String,String> environ =
++ Collections.synchronizedMap(new HashMap(System.getenv()));
++
++ public static String getenv(String varName)
++ {
++ return environ.get(varName);
++ }
++
++ public static void putenv(String varName, String value)
++ {
++ environ.put(varName, value);
++ }
++
++
+ /** A helper function for expandVariables when handling Windows paths on non-windows systems.
+ */
+ private static String win2unix(String winPath)
+@@ -135,7 +149,7 @@
+ if (m.find())
+ {
+ String varName = m.group(2);
+- String expansion = System.getenv(varName);
++ String expansion = getenv(varName);
+ if (expansion != null)
+ return m.replaceFirst(expansion);
+ }
+@@ -174,7 +188,7 @@
+ return arg;
+ }
+ String varName = m.group(2);
+- String expansion = System.getenv(varName);
++ String expansion = getenv(varName);
+ if (expansion == null) {
+ if (varName.equalsIgnoreCase("jedit_settings") && jEdit.getSettingsDirectory() != null) {
+ expansion = jEdit.getSettingsDirectory();
+@@ -184,7 +198,7 @@
+ varName = varName.toUpperCase();
+ String uparg = arg.toUpperCase();
+ m = p.matcher(uparg);
+- expansion = System.getenv(varName);
++ expansion = getenv(varName);
+ }
+ }
+ if (expansion != null) {