JAL-3253 reconciled with Jalview-JS/develop

diff --git a/src/jalview/util/Platform.java b/src/jalview/util/Platform.java
index b779c20..389768f 100644 (file)
--- a/src/jalview/util/Platform.java
+++ b/src/jalview/util/Platform.java
@@ -154,23 +154,15 @@ public class Platform
   }
 
   /**
-   * escape a string according to the local platform's escape character
+   * Answers the input with every backslash replaced with a double backslash (an
+   * 'escaped' single backslash)
    * 
-   * @param file
-   * @return escaped file
+   * @param s
+   * @return
    */
-  public static String escapeString(String file)
+  public static String escapeBackslashes(String s)
   {
-    StringBuffer f = new StringBuffer();
-    int p = 0, lastp = 0;
-    while ((p = file.indexOf('\\', lastp)) > -1)
-    {
-      f.append(file.subSequence(lastp, p));
-      f.append("\\\\");
-      lastp = p + 1;
-    }
-    f.append(file.substring(lastp));
-    return f.toString();
+    return s == null ? null : s.replace("\\", "\\\\");
   }
 
   /**
@@ -339,48 +331,6 @@ public class Platform
       break;
     }
   }
-
-  /**
-   * Encode the URI using JavaScript encodeURIComponent
-   * 
-   * @param value
-   * @return encoded value
-   */
-  public static String encodeURI(String value)
-  {
-    /**
-     * @j2sNative value = encodeURIComponent(value);
-     */
-    return value;
-  }
-
-  /**
-   * Open the URL using a simple window call if this is JavaScript
-   * 
-   * @param url
-   * @return true if window has been opened
-   */
-  public static boolean openURL(String url) throws IOException
-  {
-    if (!isJS())
-    {
-      BrowserLauncher.openURL(url);
-      return false;
-    }
-    /**
-     * @j2sNative
-     * 
-     * 
-     *            window.open(url);
-     */
-    return true;
-  }
-
-  public static void stackTrace()
-  {
-    new NullPointerException("testing only").printStackTrace();
-  }
-
   public static void cacheFileData(String path, Object data)
   {
     if (isJS())
@@ -459,6 +409,49 @@ public class Platform
   }
 
   /**
+   * Encode the URI using JavaScript encodeURIComponent
+   * 
+   * @param value
+   * @return encoded value
+   */
+  public static String encodeURI(String value)
+  {
+    /**
+     * @j2sNative value = encodeURIComponent(value);
+     */
+    return value;
+  }
+
+  /**
+   * Open the URL using a simple window call if this is JavaScript
+   * 
+   * @param url
+   * @return true if window has been opened
+   */
+  public static boolean openURL(String url) throws IOException
+  {
+    if (!isJS())
+    {
+      BrowserLauncher.openURL(url);
+      return false;
+    }
+    /**
+     * @j2sNative
+     * 
+     * 
+     *            window.open(url);
+     */
+    return true;
+  }
+
+  public static String getUniqueAppletID()
+  {
+         // Caution -- null here means using current thread instead of a known component.
+         
+         return jsutil.getAppletForComponent(null)._getID();
+  }
+
+  /**
    * Read the Info block for this applet.
    * 
    * @param prefix
@@ -616,6 +609,31 @@ public class Platform
 
   }
 
+
+  /**
+   * A (case sensitive) file path comparator that ignores the difference between /
+   * and \
+   * 
+   * 
+   * @param path1
+   * @param path2
+   * @return
+   */
+  public static boolean pathEquals(String path1, String path2)
+  {
+    if (path1 == null)
+    {
+      return path2 == null;
+    }
+    if (path2 == null)
+    {
+      return false;
+    }
+    String p1 = path1.replace('\\', '/');
+    String p2 = path2.replace('\\', '/');
+    return p1.equals(p2);
+  }
+  
   public static URL getDocumentBase()
   {
     return (isJS() ? jsutil.getDocumentBase() : null);
@@ -794,4 +812,32 @@ public class Platform
     hs.add("one");
     return (hs.iterator().next() == (enabled ? "two" : "one"));
   }
+  
+
+  public static void stackTrace()
+  {
+    new NullPointerException("testing only").printStackTrace();
+  }
+
+
+  /**
+   * escape a string according to the local platform's escape character
+   * 
+   * @param file
+   * @return escaped file
+   */
+  public static String escapeString(String file)
+  {
+    StringBuffer f = new StringBuffer();
+    int p = 0, lastp = 0;
+    while ((p = file.indexOf('\\', lastp)) > -1)
+    {
+      f.append(file.subSequence(lastp, p));
+      f.append("\\\\");
+      lastp = p + 1;
+    }
+    f.append(file.substring(lastp));
+    return f.toString();
+  }
+
 }