src/Tools/jEdit/patches/putenv
author wenzelm
Sat, 20 Feb 2021 13:42:37 +0100
changeset 73255 7e2a9a8c2b85
parent 72247 c06260b7152c
child 73653 d9823224fcfe
permissions -rw-r--r--
provide naproche-755224402e36;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
72247
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 71932
diff changeset
     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
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 71932
diff changeset
     2
--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/MiscUtilities.java	2020-09-03 05:31:01.000000000 +0200
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 71932
diff changeset
     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
96b633ac24f8 proper environment for variable folding;
wenzelm
parents: 69188
diff changeset
    18
+		if (value == null) environ.remove(varName);
96b633ac24f8 proper environment for variable folding;
wenzelm
parents: 69188
diff changeset
    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
96b633ac24f8 proper environment for variable folding;
wenzelm
parents: 69188
diff changeset
    54
 		//{{{ VarCompressor constructor
96b633ac24f8 proper environment for variable folding;
wenzelm
parents: 69188
diff changeset
    55
 		VarCompressor()
96b633ac24f8 proper environment for variable folding;
wenzelm
parents: 69188
diff changeset
    56
 		{
96b633ac24f8 proper environment for variable folding;
wenzelm
parents: 69188
diff changeset
    57
-			ProcessBuilder pb = new ProcessBuilder();
96b633ac24f8 proper environment for variable folding;
wenzelm
parents: 69188
diff changeset
    58
-			Map<String, String> env = pb.environment();
96b633ac24f8 proper environment for variable folding;
wenzelm
parents: 69188
diff changeset
    59
 			if (OperatingSystem.isUnix())
96b633ac24f8 proper environment for variable folding;
wenzelm
parents: 69188
diff changeset
    60
 				prefixMap.put(System.getProperty("user.home"), "~");
96b633ac24f8 proper environment for variable folding;
wenzelm
parents: 69188
diff changeset
    61
 			if (jEdit.getSettingsDirectory() != null)
96b633ac24f8 proper environment for variable folding;
wenzelm
parents: 69188
diff changeset
    62
 				prefixMap.put(jEdit.getSettingsDirectory(), "JEDIT_SETTINGS");
96b633ac24f8 proper environment for variable folding;
wenzelm
parents: 69188
diff changeset
    63
-			for (Map.Entry<String, String> entry: env.entrySet())
96b633ac24f8 proper environment for variable folding;
wenzelm
parents: 69188
diff changeset
    64
+			for (Map.Entry<String, String> entry: environ.entrySet())
96b633ac24f8 proper environment for variable folding;
wenzelm
parents: 69188
diff changeset
    65
 			{
96b633ac24f8 proper environment for variable folding;
wenzelm
parents: 69188
diff changeset
    66
 				String k = entry.getKey();
96b633ac24f8 proper environment for variable folding;
wenzelm
parents: 69188
diff changeset
    67
 				if (k.equalsIgnoreCase("pwd") || k.equalsIgnoreCase("oldpwd")) continue;