# HG changeset patch
# User wenzelm
# Date 1380365733 -7200
# Node ID cca95e9055ba9c02cdd22559045d23f933a11f85
# Parent  ac0e4ca891f9f03622513f30386191d2029ba71d
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;

diff -r ac0e4ca891f9 -r cca95e9055ba src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala	Fri Sep 27 21:54:55 2013 +0200
+++ b/src/Pure/Tools/main.scala	Sat Sep 28 12:55:33 2013 +0200
@@ -110,6 +110,8 @@
 
           /* startup */
 
+          update_environment()
+
           System.setProperty("jedit.home",
             Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist")))
 
@@ -213,5 +215,35 @@
     system_dialog.echo("init ...")
     Isabelle_System.init()
   }
+
+
+
+  /** adhoc update of JVM environment variables **/
+
+  def update_environment()
+  {
+    val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME")
+    val update =
+      if (Platform.is_windows)
+        List("ISABELLE_HOME" -> Isabelle_System.jvm_path(isabelle_home), "INI_DIR" -> "")
+      else
+        List("ISABELLE_HOME" -> isabelle_home)
+
+    val official_env = System.getenv()
+
+    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)
+        val env = m.get(official_env).asInstanceOf[java.util.Map[String, String]]
+        update.foreach {
+          case (x, "") => env.remove(x)
+          case (x, y) => env.put(x, y)
+        }
+      case None => error("Failed to update JVM environment -- platform incompatibility")
+    }
+  }
 }