From 8d70bd75076f3abd10acb241de75c1f52622d42f Mon Sep 17 00:00:00 2001
From: Shachar Itzhaky <corwin.amber@gmail.com>
Date: Sat, 15 May 2021 01:54:54 +0300
Subject: [PATCH] [feature] [ui] Attached light switch.
---
ui-js/cm-provider.js | 6 +++++
ui-js/coq-layout-classic.js | 31 +++++++++++++++++--------
ui-js/coq-manager.js | 24 ++++++++++++++++----
ui-js/settings.js | 45 ++++++++++++++++++++++++++++++++-----
4 files changed, 88 insertions(+), 18 deletions(-)
diff --git a/ui-js/cm-provider.js b/ui-js/cm-provider.js
index 00a9130b..e9ba54fa 100644
--- a/ui-js/cm-provider.js
+++ b/ui-js/cm-provider.js
@@ -106,6 +106,12 @@ class CmCoqProvider {
return editor;
}
+ configure(options) {
+ if (options.theme) {
+ this.editor.setOption('theme', options.theme);
+ }
+ }
+
trackLineCount() {
this.lineCount = this.editor.lineCount();
this.editor.on('change', ev => {
diff --git a/ui-js/coq-layout-classic.js b/ui-js/coq-layout-classic.js
index f817c664..8c2e2663 100644
--- a/ui-js/coq-layout-classic.js
+++ b/ui-js/coq-layout-classic.js
@@ -101,8 +101,7 @@ class CoqLayoutClassic {
this.panel.id = 'panel-wrapper';
this.panel.innerHTML = this.html({base_path: options.base_path, ...params});
- if (options.theme)
- this.panel.classList.add(`jscoq-theme-${options.theme}`);
+ this.configure(options);
this.ide.appendChild(this.panel);
@@ -135,9 +134,21 @@ class CoqLayoutClassic {
.on('change', ev => this.filterLog(parseInt(ev.target.value)));
this.filterLog(3); // Info
+ this._setupSettings();
this._preloadImages();
}
+ /**
+ * Configure or re-configure UI based on CoqManager options.
+ * @param {object} options
+ */
+ configure(options) {
+ if (options.theme) {
+ this.panel.classList.remove(...this.panel.classList);
+ this.panel.classList.add(`jscoq-theme-${options.theme}`);
+ }
+ }
+
show() {
this.ide.classList.add('goals-active');
this.ide.classList.remove('toggled');
@@ -191,13 +202,6 @@ class CoqLayoutClassic {
return this.outline = outline_pane[0];
}
- createOutline() {
- var outline_pane = $('<div>').attr('id', 'outline-pane');
- $(this.ide).prepend(outline_pane);
- requestAnimationFrame(() => $(this.ide).addClass('outline-active'));
- return this.outline = outline_pane[0];
- }
-
/**
* Shows a notice in the main goal pane (reserved for important messages,
* such as during startup).
@@ -340,6 +344,15 @@ class CoqLayoutClassic {
}
}
+ /**
+ * Set up hooks for when user changes settings.
+ */
+ _setupSettings() {
+ this.settings.model.theme.observe(theme => {
+ this.configure({theme});
+ });
+ }
+
/**
* Auxiliary function to improve UX by preloading images.
*/
diff --git a/ui-js/coq-manager.js b/ui-js/coq-manager.js
index 527d812a..1e588ae2 100644
--- a/ui-js/coq-manager.js
+++ b/ui-js/coq-manager.js
@@ -148,6 +148,11 @@ class ProviderContainer {
return new Promise(resolve => setTimeout(resolve, 0));
}
+ configure(options) {
+ for (let snippet of this.snippets)
+ snippet.configure(options);
+ }
+
// Get the next candidate and mark it.
getNext(prev, until) {
@@ -294,7 +299,7 @@ class CoqManager {
}
// Setup the Coq statement provider.
- this.provider = this.setupProvider(elems);
+ this.provider = this._setupProvider(elems);
// Setup the Panel UI.
this.layout = new CoqLayoutClassic(this.options, {kb: this.keyTooltips()});
@@ -306,7 +311,8 @@ class CoqManager {
if (this.coq) this.layout.onToggle = () => {};
};
- this.setupDragDrop();
+ this._setupSettings();
+ this._setupDragDrop();
// Setup pretty printer for feedback and goals
this.pprint = new FormatPrettyPrint();
@@ -351,7 +357,7 @@ class CoqManager {
}
// Provider setup
- setupProvider(elems) {
+ _setupProvider(elems) {
var provider = new ProviderContainer(elems, this.options);
@@ -394,7 +400,17 @@ class CoqManager {
return provider;
}
- setupDragDrop() {
+ /**
+ * Set up hooks for when user changes settings.
+ */
+ _setupSettings() {
+ const editorThemes = {'light': 'default', 'dark': 'blackboard'};
+ this.layout.settings.model.theme.observe(theme => {
+ this.provider.configure({theme: editorThemes[theme]});
+ });
+ }
+
+ _setupDragDrop() {
$(this.layout.ide).on('dragover', (evt) => {
evt.preventDefault();
evt.originalEvent.dataTransfer.dropEffect = 'link';
diff --git a/ui-js/settings.js b/ui-js/settings.js
index d4412ac2..7f199b9e 100644
--- a/ui-js/settings.js
+++ b/ui-js/settings.js
@@ -7,7 +7,7 @@ class SettingsPanel {
<label for="settings--theme">
<div class="setting">
Light switch</label>
- <input id="settings--theme" type="checkbox" class="switch">
+ <input id="settings--theme" type="checkbox" checked class="switch">
</div>
</label>
<label for="settings--company">
@@ -25,8 +25,16 @@ class SettingsPanel {
`;
}
- constructor() {
+ constructor(model) {
this.el = $(this.html());
+ this.model = model || new CoqSettings();
+
+ this.el.find('#settings--theme').on('change', ev => {
+ this.model.theme.value = ev.target.checked ? 'light' : 'dark';
+ });
+ this.el.find('#settings--company').on('change', ev => {
+ this.model.company.value = ev.target.checked;
+ });
}
show() {
@@ -38,12 +46,39 @@ class SettingsPanel {
}
toggle() {
- if (this.isShown()) this.hide();
+ if (this.isVisible()) this.hide();
else this.show();
- return this.isShown();
+ return this.isVisible();
}
- isShown() {
+ isVisible() {
return this.el.parent().length > 0;
}
+}
+
+
+class CoqSettings {
+ constructor() {
+ this.theme = new ReactiveVar('light');
+ this.company = new ReactiveVar(true);
+ }
+}
+
+class ReactiveVar {
+ constructor(value) {
+ this._value = value;
+ this.observers = [];
+ }
+
+ get value() { return this._value; }
+ set value(val) {
+ this._value = val;
+ for (let o of this.observers) {
+ o(val);
+ }
+ }
+
+ observe(callback) {
+ this.observers.push(callback);
+ }
}
\ No newline at end of file
--
GitLab