author | wenzelm |
Sat, 20 Feb 2021 13:42:37 +0100 | |
changeset 73255 | 7e2a9a8c2b85 |
parent 72247 | c06260b7152c |
child 73653 | d9823224fcfe |
permissions | -rw-r--r-- |
72247 | 1 |
diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/MiscUtilities.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java |
2 |
--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/MiscUtilities.java 2020-09-03 05:31:01.000000000 +0200 |
|
3 |
+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java 2020-09-08 20:13:35.648786692 +0200 |
|
71932
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
4 |
@@ -131,6 +131,21 @@ |
69188
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
5 |
static final Pattern winPattern = Pattern.compile(winPatternString); |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
6 |
|
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
7 |
|
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
8 |
+ private static Map<String,String> environ = |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
9 |
+ Collections.synchronizedMap(new HashMap(System.getenv())); |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
10 |
+ |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
11 |
+ public static String getenv(String varName) |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
12 |
+ { |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
13 |
+ return environ.get(varName); |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
14 |
+ } |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
15 |
+ |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
16 |
+ public static void putenv(String varName, String value) |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
17 |
+ { |
69191 | 18 |
+ if (value == null) environ.remove(varName); |
19 |
+ else environ.put(varName, value); |
|
69188
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
20 |
+ } |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
21 |
+ |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
22 |
+ |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
23 |
/** A helper function for expandVariables when handling Windows paths on non-windows systems. |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
24 |
*/ |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
25 |
private static String win2unix(String winPath) |
71932
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
26 |
@@ -140,7 +155,7 @@ |
69188
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
27 |
if (m.find()) |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
28 |
{ |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
29 |
String varName = m.group(2); |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
30 |
- String expansion = System.getenv(varName); |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
31 |
+ String expansion = getenv(varName); |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
32 |
if (expansion != null) |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
33 |
return m.replaceFirst(expansion); |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
34 |
} |
71932
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
35 |
@@ -179,7 +194,7 @@ |
69188
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
36 |
return arg; |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
37 |
} |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
38 |
String varName = m.group(2); |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
39 |
- String expansion = System.getenv(varName); |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
40 |
+ String expansion = getenv(varName); |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
41 |
if (expansion == null) { |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
42 |
if (varName.equalsIgnoreCase("jedit_settings") && jEdit.getSettingsDirectory() != null) { |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
43 |
expansion = jEdit.getSettingsDirectory(); |
71932
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
44 |
@@ -189,7 +204,7 @@ |
69188
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
45 |
varName = varName.toUpperCase(); |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
46 |
String uparg = arg.toUpperCase(); |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
47 |
m = p.matcher(uparg); |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
48 |
- expansion = System.getenv(varName); |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
49 |
+ expansion = getenv(varName); |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
50 |
} |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
51 |
} |
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
diff
changeset
|
52 |
if (expansion != null) { |
71932
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents:
69838
diff
changeset
|
53 |
@@ -1682,13 +1697,11 @@ |
69191 | 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; |