X-Git-Url: http://source.jalview.org/gitweb/?a=blobdiff_plain;f=src%2Fjalview%2Futil%2FPlatform.java;fp=src%2Fjalview%2Futil%2FPlatform.java;h=ade9d8773359eb49cb711444a29b2492aaec1e3c;hb=17e4ea278bc9a5fb280db1252ce78b7a295215f5;hp=f9eb2a6bd853fc6087f933c1dab7bac58b416025;hpb=e6267883ffc25d76313c9e45967efe2c9e6d1d08;p=jalview.git diff --git a/src/jalview/util/Platform.java b/src/jalview/util/Platform.java index f9eb2a6..ade9d87 100644 --- a/src/jalview/util/Platform.java +++ b/src/jalview/util/Platform.java @@ -135,23 +135,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("\\", "\\\\"); } /** @@ -180,6 +172,20 @@ public class Platform if (!aMac) { return e.isControlDown(); + + // Jalview 2.11 code below: above is as amended for JalviewJS + // /* + // * answer false for right mouse button + // */ + // if (e.isPopupTrigger()) + // { + // return false; + // } + // return + // (jalview.util.ShortcutKeyMaskExWrapper.getMenuShortcutKeyMaskEx() // + // .getMenuShortcutKeyMaskEx() + // & jalview.util.ShortcutKeyMaskExWrapper + // .getModifiersEx(e)) != 0; // getModifiers()) != 0; } // answer false for right mouse button // shortcut key will be META for a Mac @@ -611,4 +617,26 @@ 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); + } }