diff --git a/ui-css/coq-dark.css b/ui-css/coq-dark.css
index d9f095327fbb8e66dcf94b8bfb01d11abd4c93c6..6d3af0edd34218d0d9309b77dbfb51db1b04bdd4 100644
--- a/ui-css/coq-dark.css
+++ b/ui-css/coq-dark.css
@@ -49,15 +49,22 @@
opacity: 0.6;
}
-.jscoq-theme-dark .link-to-github::after {
- background-image: url(../ui-images/themes/dark/github.png);
-}
-
.jscoq-theme-dark .flex-panel > .caption {
background: #666;
color: #ccc;
}
+.settings-panel[data-theme=dark] {
+ background: #555;
+ border-color: #888;
+ box-shadow: -3px 3px 6px 0px #fff2;
+ color: #ddd;
+}
+
+.settings-panel[data-theme=dark] .link-to-github::after {
+ background-image: url(../ui-images/themes/dark/github.png);
+}
+
/* Code settings */
/* Replaced by blackboard CM theme */
/*.CodeMirror-gutters { background-color: #000; }*/
diff --git a/ui-js/addon/company-coq.js b/ui-js/addon/company-coq.js
index 7596ce4698e5dda914d4c3ecadf35a9b2ab00e2f..acf2fc3b80db55d4955eba421fc406717b4ab9fb 100644
--- a/ui-js/addon/company-coq.js
+++ b/ui-js/addon/company-coq.js
@@ -41,8 +41,19 @@ class Markup {
attach(cm) {
this.cm = cm;
this.work = new WorkQueue(cm);
- cm.on('change', (cm, change_obj) => this._flush(change_obj));
- cm.on('renderLine', (cm, ln, el) => this._rescan(ln));
+ this._on = {
+ change: (cm, change_obj) => this._flush(change_obj),
+ renderLine: (cm, ln, el) => this._rescan(ln)
+ };
+ cm.on('change', this._on.change);
+ cm.on('renderLine', this._on.renderLine);
+ this.applyToDocument();
+ }
+
+ detach() {
+ this.clearAll();
+ this.cm.off('change', this._on.change);
+ this.cm.off('renderLine', this._on.renderLine);
}
applyToDocument() {
@@ -87,6 +98,11 @@ class Markup {
this.cm.display.maxLine.lineNo() === line) this._maxLineHack();
}
+ clearAll() {
+ for (let mark of this.cm.getAllMarks().filter(m => m.owner == this))
+ mark.clear();
+ }
+
clearFromLine(line) {
var from = {line, ch: 0},
to = {line, ch: this.cm.getLine(line).length};
@@ -226,6 +242,9 @@ class WorkQueue {
this.tasks.push(task);
if (!this.primed) this._engage();
}
+ clear() {
+ this.tasks.splice();
+ }
_engage() {
this.primed = true;
requestAnimationFrame(() => this.cm.operation(() => {
@@ -254,7 +273,13 @@ class AutoComplete {
}
attach(cm) {
- cm.on('change', (cm, evt) => this.senseContext(cm, evt));
+ this.cm = cm;
+ this._on = {change: (cm, evt) => this.senseContext(cm, evt)};
+ cm.on('change', this._on.change);
+ }
+
+ detach() {
+ this.cm.off('change', this._on.change);
}
lemmaHint(cm, options) { return this.hint(cm, options, ['keywords', 'lemmas']); }
@@ -414,7 +439,13 @@ class ObserveIdentifier {
}
attach(cm) {
- cm.on('cursorActivity', (cm, evt) => this.underCursor(cm));
+ this.cm = cm;
+ this._on = {cursorActivity: (cm, evt) => this.underCursor(cm)};
+ cm.on('cursorActivity', this._on.cursorActivity);
+ }
+
+ detach() {
+ this.cm.off('cursorActivity', this._on.cursorActivity);
}
underCursor(cm) {
@@ -547,6 +578,14 @@ class CompanyCoq {
return this;
}
+ detach() {
+ this.markup.detach();
+ this.completion.detach();
+ this.observe.detach();
+
+ return this;
+ }
+
static hint(cm, options) {
if (cm.company_coq)
return cm.company_coq.completion.getCompletions(cm, options);
@@ -578,15 +617,28 @@ class CompanyCoq {
ObserveIdentifier.instance.vocab = vocab;
CodeMirror.CompanyCoq = CompanyCoq;
- CodeMirror.defineInitHook(cm => {
- if (cm.options.mode['company-coq'])
- cm.company_coq = new CompanyCoq().attach(cm);
- });
+ CodeMirror.defineInitHook(cm =>
+ CompanyCoq.configure(cm, cm.options));
CodeMirror.registerGlobalHelper("hint", "company-coq",
(mode, cm) => mode.name === 'coq' && !!cm.company_coq,
CompanyCoq.hint);
}
+
+ static configure(cm, options) {
+ switch (options.mode && options.mode['company-coq']) {
+ case true:
+ if (!cm.company_coq)
+ cm.company_coq = new CompanyCoq().attach(cm);
+ break;
+ case false:
+ if (cm.company_coq) {
+ cm.company_coq.detach();
+ cm.company_coq = undefined;
+ }
+ break;
+ }
+ }
}
diff --git a/ui-js/cm-provider.js b/ui-js/cm-provider.js
index e9ba54fa453b2c10d3385f470611e650267a4ce1..0870072410eb18663662c338f88b4a3f8a284ca8 100644
--- a/ui-js/cm-provider.js
+++ b/ui-js/cm-provider.js
@@ -110,6 +110,7 @@ class CmCoqProvider {
if (options.theme) {
this.editor.setOption('theme', options.theme);
}
+ CodeMirror.CompanyCoq.configure(this.editor, options);
}
trackLineCount() {
diff --git a/ui-js/coq-layout-classic.js b/ui-js/coq-layout-classic.js
index 8c2e26632e0e69bb13b01dfbdb596d15a103d3da..8c643feb868fc5b744920c37cec292a68da82927 100644
--- a/ui-js/coq-layout-classic.js
+++ b/ui-js/coq-layout-classic.js
@@ -101,8 +101,6 @@ class CoqLayoutClassic {
this.panel.id = 'panel-wrapper';
this.panel.innerHTML = this.html({base_path: options.base_path, ...params});
- this.configure(options);
-
this.ide.appendChild(this.panel);
// UI setup.
@@ -134,6 +132,8 @@ class CoqLayoutClassic {
.on('change', ev => this.filterLog(parseInt(ev.target.value)));
this.filterLog(3); // Info
+ this.configure(options);
+
this._setupSettings();
this._preloadImages();
}
@@ -147,6 +147,11 @@ class CoqLayoutClassic {
this.panel.classList.remove(...this.panel.classList);
this.panel.classList.add(`jscoq-theme-${options.theme}`);
}
+ this.settings.configure({
+ theme: options.theme,
+ company: options.editor && options.editor.mode &&
+ options.editor.mode['company-coq']
+ });
}
show() {
diff --git a/ui-js/coq-manager.js b/ui-js/coq-manager.js
index 1e588ae2b2dc77458815ed74eab921bfab4615ad..fb6607a63b8f6ecc766c0f8e6740cbb2343a3dc5 100644
--- a/ui-js/coq-manager.js
+++ b/ui-js/coq-manager.js
@@ -408,6 +408,9 @@ class CoqManager {
this.layout.settings.model.theme.observe(theme => {
this.provider.configure({theme: editorThemes[theme]});
});
+ this.layout.settings.model.company.observe(enable => {
+ this.provider.configure({mode: {'company-coq': enable}});
+ });
}
_setupDragDrop() {
diff --git a/ui-js/settings.js b/ui-js/settings.js
index 7f199b9eac69194dba4153f08c06ca69602f4cf5..5f866840d9e72b67d269c14903037c6f0ce41420 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" checked class="switch">
+ <input id="settings--theme" type="checkbox" class="switch">
</div>
</label>
<label for="settings--company">
@@ -37,12 +37,27 @@ class SettingsPanel {
});
}
+ configure(options) {
+ var v;
+ if (v = options.theme) {
+ this.el.attr('data-theme', v);
+ this.model.theme.value = v;
+ this.el.find('#settings--theme').attr('checked', v == 'light');
+ }
+ if ((v = options.company) !== undefined) {
+ this.model.theme.company = v;
+ this.el.find('#settings--company').attr('checked', v);
+ }
+ }
+
show() {
- $(document.body).append(this.el);
+ if (this.el.parent().length == 0)
+ $(document.body).append(this.el);
+ this.el.show();
}
hide() {
- this.el.remove();
+ this.el.hide();
}
toggle() {
@@ -52,7 +67,7 @@ class SettingsPanel {
}
isVisible() {
- return this.el.parent().length > 0;
+ return this.el.is(':visible');
}
}
@@ -72,9 +87,11 @@ class ReactiveVar {
get value() { return this._value; }
set value(val) {
- this._value = val;
- for (let o of this.observers) {
- o(val);
+ if (val !== this._value) { // do not trigger for nothing
+ this._value = val;
+ for (let o of this.observers) {
+ o(val);
+ }
}
}