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