# HG changeset patch
# User wenzelm
# Date 1540500137 -7200
# Node ID 2fd73a1a09373d6a2cb17a0cf0b05f0df25c5cfb
# Parent  d8849cfad60fcc368de5a828b7a92b074dd6a176
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;

diff -r d8849cfad60f -r 2fd73a1a0937 Admin/components/components.sha1
--- 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
diff -r d8849cfad60f -r 2fd73a1a0937 Admin/components/main
--- 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
diff -r d8849cfad60f -r 2fd73a1a0937 src/Pure/Tools/main.scala
--- 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")
-    }
-  }
 }
diff -r d8849cfad60f -r 2fd73a1a0937 src/Tools/jEdit/patches/putenv
--- /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) {