From 9e4243bc7ea9ad8417fe08db0eae82dec0e16703 Mon Sep 17 00:00:00 2001
From: Matthijs Kooijman <matthijs@stdin.nl>
Date: Tue, 8 Dec 2015 16:32:45 +0100
Subject: [PATCH] Add `FileUtils.splitFilename()`

This allows splitting a filename into a basename and extension.
`FileUtils.hasExtension()` is updated to use it, in favour of the
String.split-based approached it used before.
---
 .../src/processing/app/helpers/FileUtils.java | 39 ++++++++++++++++---
 1 file changed, 34 insertions(+), 5 deletions(-)

diff --git a/arduino-core/src/processing/app/helpers/FileUtils.java b/arduino-core/src/processing/app/helpers/FileUtils.java
index e256b0160..4083a0a69 100644
--- a/arduino-core/src/processing/app/helpers/FileUtils.java
+++ b/arduino-core/src/processing/app/helpers/FileUtils.java
@@ -241,15 +241,44 @@ public class FileUtils {
   }
 
   public static boolean hasExtension(File file, List<String> extensions) {
-    String pieces[] = file.getName().split("\\.");
-    if (pieces.length < 2) {
-      return false;
+    String extension = splitFilename(file).extension;
+    return extensions.contains(extension.toLowerCase());
+  }
+
+  /**
+   * The result of a splitFilename call.
+   */
+  public static class SplitFile {
+    public SplitFile(String basename, String extension) {
+      this.basename = basename;
+      this.extension = extension;
     }
 
-    String extension = pieces[pieces.length - 1];
+    public String basename;
+    public String extension;
+  }
 
-    return extensions.contains(extension.toLowerCase());
+  /**
+   * Splits the given filename into a basename (everything up to the
+   * last dot) and an extension (everything from the last dot). The dot
+   * is not included in either part.
+   *
+   * If no dot is present, the entire filename is returned as the
+   * basename, leaving the extension empty (empty string, not null).
+   */
+  public static SplitFile splitFilename(String filename) {
+    int index = filename.lastIndexOf(".");
 
+    if (index >= 0)
+      return new SplitFile(filename.substring(0, index), filename.substring(index + 1));
+    return new SplitFile(filename, "");
+  }
+
+  /**
+   * Helper function returning splitFilename(file.getName()).
+   */
+  public static SplitFile splitFilename(File file) {
+    return splitFilename(file.getName());
   }
 
   /**