X-Git-Url: http://source.jalview.org/gitweb/?a=blobdiff_plain;f=src%2Fjalview%2Futil%2FPlatform.java;h=e8558fa14739a0fced7f5360c43712746dfdfce4;hb=fa750d6b432ef31a7407fdb8bf01c1edf687bcf4;hp=2c7460956736d88743d5e23409de5072f933ffa2;hpb=f4766a7bbcfae845fc95923b01fa14ff83d589ff;p=jalview.git diff --git a/src/jalview/util/Platform.java b/src/jalview/util/Platform.java index 2c74609..e8558fa 100644 --- a/src/jalview/util/Platform.java +++ b/src/jalview/util/Platform.java @@ -20,7 +20,6 @@ */ package jalview.util; -import java.awt.Toolkit; import java.awt.event.MouseEvent; /** @@ -88,23 +87,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("\\", "\\\\"); } /** @@ -140,10 +131,33 @@ public class Platform { return false; } - return (Toolkit.getDefaultToolkit().getMenuShortcutKeyMask() - & e.getModifiers()) != 0; - // could we use e.isMetaDown() here? + return (jalview.util.ShortcutKeyMaskExWrapper.getMenuShortcutKeyMaskEx() // .getMenuShortcutKeyMaskEx() + & jalview.util.ShortcutKeyMaskExWrapper + .getModifiersEx(e)) != 0; // getModifiers()) != 0; } return e.isControlDown(); } + + /** + * 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); + } }