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;
     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
     3 +++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/MiscUtilities.java	2019-02-24 12:21:09.602678130 +0100
     4 @@ -126,6 +126,21 @@
     5  	static final Pattern winPattern = Pattern.compile(winPatternString);
     6  
     7  
     8 +	private static Map<String,String> environ =
     9 +		Collections.synchronizedMap(new HashMap(System.getenv()));
    10 +
    11 +	public static String getenv(String varName)
    12 +	{
    13 +		return environ.get(varName);
    14 +	}
    15 +
    16 +	public static void putenv(String varName, String value)
    17 +	{
    18 +		if (value == null) environ.remove(varName);
    19 +		else environ.put(varName, value);
    20 +	}
    21 +	
    22 +
    23  	/** A helper function for expandVariables when handling Windows paths on non-windows systems.
    24  	*/
    25  	private static String win2unix(String winPath)
    26 @@ -135,7 +150,7 @@
    27  		if (m.find())
    28  		{
    29  			String varName = m.group(2);
    30 -			String expansion = System.getenv(varName);
    31 +			String expansion = getenv(varName);
    32  			if (expansion != null)
    33  				return m.replaceFirst(expansion);
    34  		}
    35 @@ -174,7 +189,7 @@
    36  				return arg;
    37  		}
    38  		String varName = m.group(2);
    39 -		String expansion = System.getenv(varName);
    40 +		String expansion = getenv(varName);
    41  		if (expansion == null) {
    42  			if (varName.equalsIgnoreCase("jedit_settings") && jEdit.getSettingsDirectory() != null) {
    43  				expansion = jEdit.getSettingsDirectory();
    44 @@ -184,7 +199,7 @@
    45  				varName = varName.toUpperCase();
    46  				String uparg = arg.toUpperCase();
    47  				m = p.matcher(uparg);
    48 -				expansion = System.getenv(varName);
    49 +				expansion = getenv(varName);
    50  			}
    51  		}
    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;