src/Tools/jEdit/patches/putenv
author wenzelm
Sun Feb 24 12:49:32 2019 +0100 (2 months ago ago)
changeset 70019 4419d4d675c3
parent 69194 96b633ac24f8
permissions -rw-r--r--
formal update of patches -- no change of content;
wenzelm@69189
     1
diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java
wenzelm@69189
     2
--- 5.5.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java	2018-04-09 01:57:06.000000000 +0200
wenzelm@70019
     3
+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java	2019-02-24 12:21:09.602678130 +0100
wenzelm@69194
     4
@@ -126,6 +126,21 @@
wenzelm@69189
     5
 	static final Pattern winPattern = Pattern.compile(winPatternString);
wenzelm@69189
     6
 
wenzelm@69189
     7
 
wenzelm@69189
     8
+	private static Map<String,String> environ =
wenzelm@69189
     9
+		Collections.synchronizedMap(new HashMap(System.getenv()));
wenzelm@69189
    10
+
wenzelm@69189
    11
+	public static String getenv(String varName)
wenzelm@69189
    12
+	{
wenzelm@69189
    13
+		return environ.get(varName);
wenzelm@69189
    14
+	}
wenzelm@69189
    15
+
wenzelm@69189
    16
+	public static void putenv(String varName, String value)
wenzelm@69189
    17
+	{
wenzelm@69194
    18
+		if (value == null) environ.remove(varName);
wenzelm@69194
    19
+		else environ.put(varName, value);
wenzelm@69189
    20
+	}
wenzelm@69189
    21
+	
wenzelm@69189
    22
+
wenzelm@69189
    23
 	/** A helper function for expandVariables when handling Windows paths on non-windows systems.
wenzelm@69189
    24
 	*/
wenzelm@69189
    25
 	private static String win2unix(String winPath)
wenzelm@69194
    26
@@ -135,7 +150,7 @@
wenzelm@69189
    27
 		if (m.find())
wenzelm@69189
    28
 		{
wenzelm@69189
    29
 			String varName = m.group(2);
wenzelm@69189
    30
-			String expansion = System.getenv(varName);
wenzelm@69189
    31
+			String expansion = getenv(varName);
wenzelm@69189
    32
 			if (expansion != null)
wenzelm@69189
    33
 				return m.replaceFirst(expansion);
wenzelm@69189
    34
 		}
wenzelm@69194
    35
@@ -174,7 +189,7 @@
wenzelm@69189
    36
 				return arg;
wenzelm@69189
    37
 		}
wenzelm@69189
    38
 		String varName = m.group(2);
wenzelm@69189
    39
-		String expansion = System.getenv(varName);
wenzelm@69189
    40
+		String expansion = getenv(varName);
wenzelm@69189
    41
 		if (expansion == null) {
wenzelm@69189
    42
 			if (varName.equalsIgnoreCase("jedit_settings") && jEdit.getSettingsDirectory() != null) {
wenzelm@69189
    43
 				expansion = jEdit.getSettingsDirectory();
wenzelm@69194
    44
@@ -184,7 +199,7 @@
wenzelm@69189
    45
 				varName = varName.toUpperCase();
wenzelm@69189
    46
 				String uparg = arg.toUpperCase();
wenzelm@69189
    47
 				m = p.matcher(uparg);
wenzelm@69189
    48
-				expansion = System.getenv(varName);
wenzelm@69189
    49
+				expansion = getenv(varName);
wenzelm@69189
    50
 			}
wenzelm@69189
    51
 		}
wenzelm@69189
    52
 		if (expansion != null) {
wenzelm@69194
    53
@@ -1637,13 +1652,11 @@
wenzelm@69194
    54
 		//{{{ VarCompressor constructor
wenzelm@69194
    55
 		VarCompressor()
wenzelm@69194
    56
 		{
wenzelm@69194
    57
-			ProcessBuilder pb = new ProcessBuilder();
wenzelm@69194
    58
-			Map<String, String> env = pb.environment();
wenzelm@69194
    59
 			if (OperatingSystem.isUnix())
wenzelm@69194
    60
 				prefixMap.put(System.getProperty("user.home"), "~");
wenzelm@69194
    61
 			if (jEdit.getSettingsDirectory() != null)
wenzelm@69194
    62
 				prefixMap.put(jEdit.getSettingsDirectory(), "JEDIT_SETTINGS");
wenzelm@69194
    63
-			for (Map.Entry<String, String> entry: env.entrySet())
wenzelm@69194
    64
+			for (Map.Entry<String, String> entry: environ.entrySet())
wenzelm@69194
    65
 			{
wenzelm@69194
    66
 				String k = entry.getKey();
wenzelm@69194
    67
 				if (k.equalsIgnoreCase("pwd") || k.equalsIgnoreCase("oldpwd")) continue;