mirror of https://github.com/buggins/dlangide.git
fix theme update
This commit is contained in:
parent
b5744a8411
commit
a7bf256d15
2
dub.json
2
dub.json
|
@ -12,7 +12,7 @@
|
||||||
"stringImportPaths": ["views", "views/res", "views/res/i18n", "views/res/mdpi", "views/res/hdpi"],
|
"stringImportPaths": ["views", "views/res", "views/res/i18n", "views/res/mdpi", "views/res/hdpi"],
|
||||||
|
|
||||||
"dependencies": {
|
"dependencies": {
|
||||||
"dlangui": "==0.9.99",
|
"dlangui": "==0.9.101",
|
||||||
"dcd": "~>0.9.1"
|
"dcd": "~>0.9.1"
|
||||||
},
|
},
|
||||||
|
|
||||||
|
|
|
@ -1370,8 +1370,10 @@ class IDEFrame : AppFrame, ProgramExecutionStatusListener, BreakpointListChangeL
|
||||||
currentTheme.fontSize = settings.uiFontSize;
|
currentTheme.fontSize = settings.uiFontSize;
|
||||||
needUpdateTheme = true;
|
needUpdateTheme = true;
|
||||||
}
|
}
|
||||||
if (needUpdateTheme)
|
if (needUpdateTheme) {
|
||||||
|
Log.d("updating theme after UI font change");
|
||||||
Platform.instance.onThemeChanged();
|
Platform.instance.onThemeChanged();
|
||||||
|
}
|
||||||
requestLayout();
|
requestLayout();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -65,10 +65,6 @@ SettingsPage createSettingsPages() {
|
||||||
// Root page
|
// Root page
|
||||||
SettingsPage res = new SettingsPage("", UIString.fromRaw(""d));
|
SettingsPage res = new SettingsPage("", UIString.fromRaw(""d));
|
||||||
|
|
||||||
// Common page
|
|
||||||
SettingsPage common = res.addChild("common", UIString.fromId("OPTION_COMMON"c));
|
|
||||||
common.addCheckbox("common/autoOpenLastProject", UIString.fromId("OPTION_AUTO_OPEN_LAST_PROJECT"c));
|
|
||||||
|
|
||||||
// UI settings page
|
// UI settings page
|
||||||
SettingsPage ui = res.addChild("interface", UIString.fromId("OPTION_INTERFACE"c));
|
SettingsPage ui = res.addChild("interface", UIString.fromId("OPTION_INTERFACE"c));
|
||||||
ui.addStringComboBox("interface/theme", UIString.fromId("OPTION_THEME"c), [
|
ui.addStringComboBox("interface/theme", UIString.fromId("OPTION_THEME"c), [
|
||||||
|
@ -134,6 +130,10 @@ SettingsPage createSettingsPages() {
|
||||||
texted.addCheckbox("editors/textEditor/showWhiteSpaceMarks", UIString.fromId("OPTION_SHOW_SPACES"c));
|
texted.addCheckbox("editors/textEditor/showWhiteSpaceMarks", UIString.fromId("OPTION_SHOW_SPACES"c));
|
||||||
texted.addCheckbox("editors/textEditor/showTabPositionMarks", UIString.fromId("OPTION_SHOW_TABS"c));
|
texted.addCheckbox("editors/textEditor/showTabPositionMarks", UIString.fromId("OPTION_SHOW_TABS"c));
|
||||||
|
|
||||||
|
// Common page
|
||||||
|
SettingsPage common = res.addChild("common", UIString.fromId("OPTION_COMMON"c));
|
||||||
|
common.addCheckbox("common/autoOpenLastProject", UIString.fromId("OPTION_AUTO_OPEN_LAST_PROJECT"c));
|
||||||
|
|
||||||
|
|
||||||
SettingsPage dlang = res.addChild("dlang", UIString.fromRaw("D"d));
|
SettingsPage dlang = res.addChild("dlang", UIString.fromRaw("D"d));
|
||||||
SettingsPage dub = dlang.addChild("dlang/dub", UIString.fromRaw("DUB"d));
|
SettingsPage dub = dlang.addChild("dlang/dub", UIString.fromRaw("DUB"d));
|
||||||
|
|
|
@ -1 +1 @@
|
||||||
v0.7.52
|
v0.7.53
|
Loading…
Reference in New Issue