Quelle  putenv   Sprache: Isabelle

diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/MiscUtilities.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2024-08-03 19:53:15.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/MiscUtilities.java 2024-10-29 11:50:54.062016616 +0100
@@ -131,6 +131,21 @@
  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)
+ {
+  if (value == null) environ.remove(varName);
+  else environ.put(varName, value);
+ }
+ 
+
  /** A helper function for expandVariables when handling Windows paths on non-windows systems.
  */
  private static String win2unix(String winPath)
@@ -140,7 +155,7 @@
   if (m.find())
   {
    String varName = m.group(2);
-   String expansion = jEdit.systemManager.getenv(varName);
+   String expansion = getenv(varName);
    if (expansion != null)
    {
     expansion = Matcher.quoteReplacement(expansion);
@@ -182,7 +197,7 @@
     return arg;
   }
   String varName = m.group(2);
-  String expansion = jEdit.systemManager.getenv(varName);
+  String expansion = getenv(varName);
   if (expansion == null) {
    if (varName.equalsIgnoreCase("jedit_settings") && jEdit.getSettingsDirectory() != null) {
     expansion = jEdit.getSettingsDirectory();
@@ -192,7 +207,7 @@
     varName = varName.toUpperCase();
     String uparg = arg.toUpperCase();
     m = p.matcher(uparg);
-    expansion = System.getenv(varName);
+    expansion = getenv(varName);
    }
   }
   if (expansion != null) {
@@ -1674,13 +1689,11 @@
   //{{{ VarCompressor constructor
   VarCompressor()
   {
-   ProcessBuilder pb = new ProcessBuilder();
-   Map<String, String> env = pb.environment();
    if (OperatingSystem.isUnix())
     prefixMap.put(System.getProperty("user.home"), "~");
    if (jEdit.getSettingsDirectory() != null)
     prefixMap.put(jEdit.getSettingsDirectory(), "JEDIT_SETTINGS");
-   for (Map.Entry<String, String> entry: env.entrySet())
+   for (Map.Entry<String, String> entry: environ.entrySet())
    {
     String k = entry.getKey();
     if (k.equalsIgnoreCase("pwd") || k.equalsIgnoreCase("oldpwd")) continue;
diff -ru jedit5.7.0/jEdit/test/org/gjt/sp/jedit/MiscUtilitiesTest.java jedit5.7.0-patched/jEdit/test/org/gjt/sp/jedit/MiscUtilitiesTest.java
--- jedit5.7.0/jEdit/test/org/gjt/sp/jedit/MiscUtilitiesTest.java 2024-08-03 19:53:29.000000000 +0200
+++ jedit5.7.0-patched/jEdit/test/org/gjt/sp/jedit/MiscUtilitiesTest.java 2024-10-29 12:21:05.284840022 +0100
@@ -167,56 +167,6 @@
  }
 
  @Test
- public void expandVariablesEnvWindowsAsWindows() throws Exception
- {
-  jEdit.systemManager = Mockito.mock(SystemManager.class);
-  var captor = ArgumentCaptor.forClass(String.class);
-  var value = "c:\\home\\jEdit";
-  Mockito.when(jEdit.systemManager.getenv(captor.capture())).thenReturn(value);
-  updateOS(WINDOWS_NT);
-  var key = "jEdit_TEST";
-  assertEquals(value, MiscUtilities.expandVariables('%' + key + '%'));
-  assertEquals(captor.getValue(), key);
- }
- @Test
- public void expandVariablesEnvWindowsAsUnix() throws Exception
- {
-  jEdit.systemManager = Mockito.mock(SystemManager.class);
-  var captor = ArgumentCaptor.forClass(String.class);
-  var value = "c:\\home\\jEdit";
-  Mockito.when(jEdit.systemManager.getenv(captor.capture())).thenReturn(value);
-  updateOS(UNIX);
-  var key = "jEdit_TEST";
-  assertEquals(value, MiscUtilities.expandVariables('%' + key + '%'));
-  assertEquals(captor.getValue(), key);
- }
-
- @Test
- public void expandVariablesEnvUnix() throws Exception
- {
-  jEdit.systemManager = Mockito.mock(SystemManager.class);
-  var captor = ArgumentCaptor.forClass(String.class);
-  var value = "c:\\home\\jEdit";
-  Mockito.when(jEdit.systemManager.getenv(captor.capture())).thenReturn(value);
-  updateOS(UNIX);
-  var key = "jEdit_TEST";
-  assertEquals(value, MiscUtilities.expandVariables('$' + key));
-  assertEquals(captor.getValue(), key);
- }
-
- @Test
- public void expandVariablesEnvUnix2() throws Exception
- {
-  jEdit.systemManager = Mockito.mock(SystemManager.class);
-  var captor = ArgumentCaptor.forClass(String.class);
-  var value = "c:\\home\\jEdit";
-  Mockito.when(jEdit.systemManager.getenv(captor.capture())).thenReturn(value);
-  updateOS(UNIX);
-  var key = "jEdit_TEST";
-  assertEquals(value, MiscUtilities.expandVariables("${" + key + '}'));
- }
-
- @Test
  public void expandVariablesEnvUnixNoMatch() throws Exception
  {
   updateOS(UNIX);