From 64c2fa1182ec3c5df46f09b17c83ca55ec7608a2 Mon Sep 17 00:00:00 2001 From: sebthom Date: Fri, 16 Feb 2024 22:14:24 +0100 Subject: [PATCH] fix: default theme cannot be set in plugin customization file #713 --- .../main/java/org/eclipse/tm4e/ui/TMUIPlugin.java | 4 ++++ .../ui/internal/preferences/PreferenceHelper.java | 14 +++++++------- .../tm4e/ui/internal/themes/ThemeManager.java | 12 +++++------- 3 files changed, 16 insertions(+), 14 deletions(-) diff --git a/org.eclipse.tm4e.ui/src/main/java/org/eclipse/tm4e/ui/TMUIPlugin.java b/org.eclipse.tm4e.ui/src/main/java/org/eclipse/tm4e/ui/TMUIPlugin.java index 5f39018a8..e01d12d4b 100644 --- a/org.eclipse.tm4e.ui/src/main/java/org/eclipse/tm4e/ui/TMUIPlugin.java +++ b/org.eclipse.tm4e.ui/src/main/java/org/eclipse/tm4e/ui/TMUIPlugin.java @@ -43,6 +43,10 @@ public class TMUIPlugin extends AbstractUIPlugin { @Nullable private static volatile TMUIPlugin plugin; + public static @Nullable String getPreference(final String key, final @Nullable String defaultValue) { + return Platform.getPreferencesService().getString(PLUGIN_ID, key, defaultValue, null /* = search in all available scopes */); + } + public static void log(final IStatus status) { final var p = plugin; if (p != null) { diff --git a/org.eclipse.tm4e.ui/src/main/java/org/eclipse/tm4e/ui/internal/preferences/PreferenceHelper.java b/org.eclipse.tm4e.ui/src/main/java/org/eclipse/tm4e/ui/internal/preferences/PreferenceHelper.java index 1b71831fb..c1a73a160 100644 --- a/org.eclipse.tm4e.ui/src/main/java/org/eclipse/tm4e/ui/internal/preferences/PreferenceHelper.java +++ b/org.eclipse.tm4e.ui/src/main/java/org/eclipse/tm4e/ui/internal/preferences/PreferenceHelper.java @@ -84,14 +84,14 @@ public static String toJsonThemeAssociations(final Collection } public static Set loadMarkerConfigs() { - final var prefs = InstanceScope.INSTANCE.getNode(TMUIPlugin.PLUGIN_ID); - final var json = prefs.get(PreferenceConstants.TASK_TAGS, null); + final var json = TMUIPlugin.getPreference(PreferenceConstants.TASK_TAGS, null); Set result = null; - try { - result = loadMarkerConfigs(json); - } catch (final JsonSyntaxException ex) { - TMUIPlugin.logError(ex); - } + if (json != null) + try { + result = loadMarkerConfigs(json); + } catch (final JsonSyntaxException ex) { + TMUIPlugin.logError(ex); + } return result == null ? MarkerConfig.getDefaults() : result; } diff --git a/org.eclipse.tm4e.ui/src/main/java/org/eclipse/tm4e/ui/internal/themes/ThemeManager.java b/org.eclipse.tm4e.ui/src/main/java/org/eclipse/tm4e/ui/internal/themes/ThemeManager.java index ac8d97935..81f9df134 100644 --- a/org.eclipse.tm4e.ui/src/main/java/org/eclipse/tm4e/ui/internal/themes/ThemeManager.java +++ b/org.eclipse.tm4e.ui/src/main/java/org/eclipse/tm4e/ui/internal/themes/ThemeManager.java @@ -120,10 +120,8 @@ private void loadThemesFromExtensionPoints() { * Load TextMate Themes from preferences. */ private void loadThemesFromPreferences() { - // Load Theme definitions from the - // "${workspace_loc}/metadata/.plugins/org.eclipse.core.runtime/.settings/org.eclipse.tm4e.ui.prefs" - final var prefs = InstanceScope.INSTANCE.getNode(TMUIPlugin.PLUGIN_ID); - String json = prefs.get(PreferenceConstants.THEMES, null); + // Load Theme definitions from preferences + String json = TMUIPlugin.getPreference(PreferenceConstants.THEMES, null); if (json != null) { for (final var jsonElem : new Gson().fromJson(json, JsonObject[].class)) { final String name = jsonElem.get("id").getAsString(); @@ -134,7 +132,7 @@ private void loadThemesFromPreferences() { } } - json = prefs.get(PreferenceConstants.THEME_ASSOCIATIONS, null); + json = TMUIPlugin.getPreference(PreferenceConstants.THEME_ASSOCIATIONS, null); if (json != null) { final var themeAssociations = PreferenceHelper.loadThemeAssociations(json); for (final IThemeAssociation association : themeAssociations) { @@ -142,8 +140,8 @@ private void loadThemesFromPreferences() { } } - defaultDarkThemeId = prefs.get(PreferenceConstants.DEFAULT_DARK_THEME, null); - defaultLightThemeId = prefs.get(PreferenceConstants.DEFAULT_LIGHT_THEME, null); + defaultDarkThemeId = TMUIPlugin.getPreference(PreferenceConstants.DEFAULT_DARK_THEME, null); + defaultLightThemeId = TMUIPlugin.getPreference(PreferenceConstants.DEFAULT_LIGHT_THEME, null); } void save() throws BackingStoreException {