From 23a40f069b7ab0aafc73bd67b7059f541d51e091 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?J=C3=BCrgen=20Steitz?= <juergen.esipov@googlemail.com>
Date: Sat, 4 Mar 2017 13:02:16 +0100
Subject: [PATCH] Let didChangeConfiguration decide what options are
 interesting for the indexer

---
 src/Options.php          | 15 ---------------
 src/Server/Workspace.php |  5 ++++-
 2 files changed, 4 insertions(+), 16 deletions(-)

diff --git a/src/Options.php b/src/Options.php
index 9f61edb..99f1aab 100644
--- a/src/Options.php
+++ b/src/Options.php
@@ -11,11 +11,6 @@ class Options
      */
     public $fileTypes = ['.php'];
 
-    /**
-     * List of options that affect the indexer
-     */
-    private $indexerOptions = ['fileTypes'];
-
     /**
      * Validate/Filter input and set options for file types
      *
@@ -31,16 +26,6 @@ class Options
         $this->fileTypes = !empty($fileTypes) ? $fileTypes : $this->fileTypes;
     }
 
-    /**
-     * Get list with options that affect the indexer
-     *
-     * @return array
-     */
-    public function getIndexerOptions(): array
-    {
-        return $this->indexerOptions;
-    }
-
     /**
      * Filter valid file type
      *
diff --git a/src/Server/Workspace.php b/src/Server/Workspace.php
index ad724de..b983bf6 100644
--- a/src/Server/Workspace.php
+++ b/src/Server/Workspace.php
@@ -229,6 +229,9 @@ class Workspace
      */
     public function didChangeConfiguration($settings = null): bool
     {
+        // List of options that affect the indexer
+        $indexerOptions = ['fileTypes'];
+
         if ($settings === null) {
             return false;
         }
@@ -253,7 +256,7 @@ class Workspace
             $this->options->$prop = $val;
         }
 
-        if ($this->indexer && !empty(array_intersect($changedOptions, $this->options->getIndexerOptions()))) {
+        if ($this->indexer && !empty(array_intersect($changedOptions, $indexerOptions))) {
             // check list of options that changed since last time against the list of valid indexer options
 
             // wipe main index and start reindexing