diff --git a/CHANGES.md b/CHANGES.md
index 364430572606cd30d4ec957c245a89078a2e1eb0..a5ee611aaa6f9cfb0727eca5584a8046b7c11519 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -7,6 +7,7 @@
- Bump required compiler version to 4.10.2. (@ejgallego)
- Fixed missing indentation in pretty-printing of goals. (#126,
@corwin-of-amber)
+ - The long-awaited settings panel. (#12, @corwin-of-amber)
# jsCoq 0.12.3 "at midday"
---------------------------------------
diff --git a/ui-css/coq-base.css b/ui-css/coq-base.css
index f9b2cb3ab50e6e376a3cfd8e40922d6d01b12b49..4f7c5ec0bec1642769ac2d94c2700e41a7e0403f 100644
--- a/ui-css/coq-base.css
+++ b/ui-css/coq-base.css
@@ -27,6 +27,7 @@ a, a:link, a:visited, a:active {
margin-right: auto;
margin-left: auto;
overscroll-behavior: none;
+ --base-font-size: 11pt;
}
#ide-wrapper.layout-fixed {
@@ -70,7 +71,7 @@ a, a:link, a:visited, a:active {
/* CodeMirror */
.jscoq.CodeMirror {
- font-size: 11pt;
+ font-size: var(--base-font-size);
height: 100%; /* auto-size to fit content */
line-height: initial;
}
@@ -138,7 +139,7 @@ body.jscoq-main .CodeMirror-linenumber {
z-index: 20; /* notice: CodeMirror-dialog is at index 15 */
font-family: Helvetica, Geneva, Swiss, Arial, SunSans-Regular, sans-serif;
- font-size: 11pt;
+ font-size: var(--base-font-size);
}
#panel-wrapper * {
@@ -212,8 +213,8 @@ body.jscoq-main .CodeMirror-linenumber {
.flex-panel > .content {
flex: 1 0 0;
padding: 0 4px;
- /*transition: opacity 0.5s ease-in-out;*/
- font-family: monospace;
+ font-family: monospace, "Arial Unicode MS";
+ line-height: 1.2; /* because some characters are too tall (due to alternative font glyph rendering) */
overflow: auto;
overscroll-behavior: contain;
}
@@ -335,8 +336,8 @@ body.jscoq-main .CodeMirror-linenumber {
#toolbar .exits.right {
position: absolute;
- top: 4px;
- right: 4px;
+ top: 0px;
+ right: 0px;
transition: opacity 620ms ease-in;
}
@@ -345,22 +346,21 @@ body.jscoq-main .CodeMirror-linenumber {
transition: opacity 120ms linear;
}
-.link-to-github {
- word-spacing: -2px; /* aren't we picky */
+#toolbar svg.app-menu-button {
+ height: 36px;
+ fill: #ccc;
}
-
-.link-to-github::after {
- content: "";
- display: inline-block;
- height: 25px;
- width: 25px;
- background: url(../ui-images/github.png);
- background-size: 25px 25px;
- background-repeat: no-repeat;
- vertical-align: middle;
- margin-left: .3em;
- padding-bottom: 5px;
- box-sizing: content-box;
+#toolbar svg.app-menu-button:hover {
+ fill: #777;
+ background-color: #f2f6f2;
+}
+#toolbar svg.app-menu-button.active {
+ background-color: #676b67;
+ fill: #f2f6f2;
+}
+#toolbar svg.app-menu-button.active:hover {
+ background-color: #757a75;
+ fill: #f2f6f2;
}
#buttons {
diff --git a/ui-css/coq-dark.css b/ui-css/coq-dark.css
index d9f095327fbb8e66dcf94b8bfb01d11abd4c93c6..8781319401c6fd87e3e8f6cfba1d0899f7272e3f 100644
--- a/ui-css/coq-dark.css
+++ b/ui-css/coq-dark.css
@@ -49,15 +49,38 @@
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;
}
+.jscoq-theme-dark #toolbar svg.app-menu-button {
+ fill: #ccc;
+}
+.jscoq-theme-dark #toolbar svg.app-menu-button:hover {
+ fill: #ddd;
+ background-color: #393b39;
+}
+.jscoq-theme-dark #toolbar svg.app-menu-button.active {
+ background-color: #656965;
+ fill: #f2f6f2;
+}
+.jscoq-theme-dark #toolbar svg.app-menu-button.active:hover {
+ background-color: #757a75;
+ fill: #f2f6f2;
+}
+
+.settings-panel[data-theme=dark] {
+ background: #555;
+ border-color: #888;
+ box-shadow: -2px 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-css/settings.css b/ui-css/settings.css
new file mode 100644
index 0000000000000000000000000000000000000000..4c11ad18708e0686c08d3500e0b9f69e0d7c6568
--- /dev/null
+++ b/ui-css/settings.css
@@ -0,0 +1,218 @@
+
+div.settings-panel {
+ position: absolute;
+ right: 0;
+ top: 35px;
+ z-index: 99;
+ background: white;
+ border: 1px solid black;
+ min-width: 200px;
+ font-family: Helvetica, Geneva, Swiss, Arial, SunSans-Regular, sans-serif;
+ font-size: 11pt;
+ padding: .75em .75em .2em .75em;
+ box-shadow: -2px 3px 6px 0px #3332;
+ outline: none !important;
+}
+
+div.settings-panel div.setting {
+ line-height: 1.75em;
+}
+
+div.settings-panel .switch {
+ float: right;
+}
+div.settings-panel input.switch {
+ height: 1.75em;
+ margin: 0;
+}
+
+div.settings-panel div.links {
+ margin-top: .2em;
+ text-align: right;
+}
+
+.link-to-github {
+ word-spacing: -2px; /* aren't we picky */
+}
+
+.link-to-github::after,
+.link-to-zulip::after {
+ content: "";
+ display: inline-block;
+ height: 25px;
+ width: 25px;
+ background-size: 25px 25px;
+ background-repeat: no-repeat;
+ vertical-align: middle;
+ margin-left: .3em;
+ padding-bottom: 5px;
+ box-sizing: content-box;
+}
+
+.link-to-github::after {
+ background-image: url(../ui-images/github.png);
+}
+
+.link-to-zulip::after {
+ background-image: url(../ui-images/zulip-logo.png);
+ background-size: 20px 22px;
+ background-position: 3px 2px;
+ width: 23px;
+}
+
+/* Light switch (https://codepen.io/marcusconnor/pen/QJNvMa) */
+
+.rocker, .rocker *, .rocker *::before, .rocker *::after {
+ box-sizing: border-box;
+ margin:0;
+ padding:0;
+}
+
+/* Switch starts here */
+.rocker {
+ display: inline-block;
+ position: relative;
+ /*
+ SIZE OF SWITCH
+ ==============
+ All sizes are in em - therefore
+ changing the font-size here
+ will change the size of the switch.
+ See .rocker-small below as example.
+ */
+ font-size: 2em;
+ font-weight: bold;
+ text-align: center;
+ text-transform: uppercase;
+ color: #888;
+ width: 7em;
+ height: 4em;
+ overflow: hidden;
+ border-bottom: 0.5em solid #eee;
+}
+
+.rocker-small {
+ font-size: 0.35em; /* Sizes the switch */
+ height: 4.15em; /* had to change this for small font size */
+ margin: 0;
+}
+
+.rocker-small .switch-left,
+.rocker-small .switch-right {
+ transition: 0.1s; /* shorter transition for small */
+}
+
+.rocker::before {
+ content: "";
+ position: absolute;
+ top: 0.5em;
+ left: 0;
+ right: 0;
+ bottom: 0;
+ background-color: #999;
+ border: 0.5em solid #eee;
+ border-bottom: 0;
+}
+
+.rocker input {
+ opacity: 0;
+ width: 0;
+ height: 0;
+}
+
+.switch-left,
+.switch-right {
+ cursor: pointer;
+ position: absolute;
+ display: flex;
+ align-items: center;
+ justify-content: center;
+ height: 2.5em;
+ width: 3em;
+ transition: 0.2s;
+}
+
+.switch-left {
+ height: 2.4em;
+ width: 2.75em;
+ left: 0.85em;
+ bottom: 0.4em;
+ background-color: #ddd;
+ transform: rotate(15deg) skewX(15deg);
+}
+
+.switch-right {
+ right: 0.5em;
+ bottom: 0;
+ background-color: /*#bd5757;*/ #535;
+ color: #fff;
+}
+
+.switch-left::before,
+.switch-right::before {
+ content: "";
+ position: absolute;
+ width: 0.4em;
+ height: 2.45em;
+ bottom: -0.45em;
+ background-color: #ccc;
+ transform: skewY(-65deg);
+}
+
+.switch-left::before {
+ left: -0.4em;
+}
+
+.switch-right::before {
+ right: -0.375em;
+ background-color: transparent;
+ transform: skewY(65deg);
+}
+
+input:checked + .switch-left {
+ background-color: #eed3aa;
+ color: #880;
+ bottom: 0px;
+ left: 0.5em;
+ height: 2.5em;
+ width: 3em;
+ transform: rotate(0deg) skewX(0deg);
+}
+
+input:checked + .switch-left::before {
+ background-color: transparent;
+ width: 3.0833em;
+}
+
+input:checked + .switch-left + .switch-right {
+ background-color: #ddd;
+ color: #888;
+ bottom: 0.4em;
+ right: 0.8em;
+ height: 2.4em;
+ width: 2.75em;
+ transform: rotate(-15deg) skewX(-15deg);
+}
+
+input:checked + .switch-left + .switch-right::before {
+ background-color: #ccc;
+}
+
+/* Keyboard Users */
+/*
+input:focus + .switch-left {
+ color: #333;
+}
+
+input:checked:focus + .switch-left {
+ color: #fff;
+}
+
+input:focus + .switch-left + .switch-right {
+ color: #fff;
+}
+
+input:checked:focus + .switch-left + .switch-right {
+ color: #333;
+}
+*/
diff --git a/ui-images/zulip-logo.png b/ui-images/zulip-logo.png
new file mode 100644
index 0000000000000000000000000000000000000000..842091c933411298c360d02a54240edb40cb9fac
Binary files /dev/null and b/ui-images/zulip-logo.png differ
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 00a9130b52796af5711f3b3e1cf8336df8f3c82d..0870072410eb18663662c338f88b4a3f8a284ca8 100644
--- a/ui-js/cm-provider.js
+++ b/ui-js/cm-provider.js
@@ -106,6 +106,13 @@ class CmCoqProvider {
return editor;
}
+ configure(options) {
+ if (options.theme) {
+ this.editor.setOption('theme', options.theme);
+ }
+ CodeMirror.CompanyCoq.configure(this.editor, options);
+ }
+
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 d9828977d9a653f1e9cfccf6a08f39352d205667..c992f511cf24bb7b1c0b1c74ca2d7748364d1f63 100644
--- a/ui-js/coq-layout-classic.js
+++ b/ui-js/coq-layout-classic.js
@@ -47,7 +47,11 @@ class CoqLayoutClassic {
<button name="reset" alt="Reset worker" title="Reset worker"></button>
</span>
<div class="exits right">
- <a href="https://github.com/jscoq/jscoq" class="link-to-github"></a>
+ <svg class="app-menu-button" viewBox="0 0 80 80">
+ <circle cx="40" cy="24" r="5"></circle>
+ <circle cx="40" cy="40" r="5"></circle>
+ <circle cx="40" cy="56" r="5"></circle>
+ </svg>
</div> <!-- /.exits -->
</div> <!-- /#toolbar -->
<div class="flex-container">
@@ -97,9 +101,6 @@ 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.ide.appendChild(this.panel);
// UI setup.
@@ -107,6 +108,8 @@ class CoqLayoutClassic {
this.query = this.panel.querySelector('#query-panel');
this.packages = this.panel.querySelector('#packages-panel');
this.buttons = this.panel.querySelector('#buttons');
+ this.menubtn = this.panel.querySelector('.app-menu-button');
+ this.settings = new SettingsPanel();
var flex_container = this.panel.getElementsByClassName('flex-container')[0];
flex_container.addEventListener('click', evt => { this.panelClickHandler(evt); });
@@ -120,15 +123,39 @@ class CoqLayoutClassic {
this.onAction = evt => {};
this.buttons.addEventListener('click', evt => this.onAction(evt));
+ this.menubtn.addEventListener('mousedown', () =>
+ this.settings.toggle());
+ this.settings.active.observe(active =>
+ this.menubtn.classList.toggle('active', active));
+
// Configure log
this.log_levels = ['Error', 'Warning', 'Notice', 'Info', 'Debug']
$(this.panel).find('select[name=msg_filter]')
- .change(ev => this.filterLog(parseInt(ev.target.value)));
+ .on('change', ev => this.filterLog(parseInt(ev.target.value)));
this.filterLog(3); // Info
+ this.configure(options);
+
+ 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}`);
+ }
+ this.settings.configure({
+ theme: options.theme,
+ company: options.editor && options.editor.mode &&
+ options.editor.mode['company-coq']
+ });
+ }
+
show() {
this.ide.classList.add('goals-active');
this.ide.classList.remove('toggled');
@@ -182,13 +209,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).
@@ -331,6 +351,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 527d812a5cb84d2bc8bc6f1c72540cd0136435c2..5fdffae27d3b8628dedd5fec988aba8656c6c631 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,23 @@ 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 might take some time (do async like renumber?) */
+ this.provider.configure({theme: editorThemes[theme]});
+ });
+ this.layout.settings.model.company.observe(enable => {
+ this.provider.configure({mode: {'company-coq': enable}});
+ this.company_coq = this.contextual_info.company_coq =
+ enable ? new CodeMirror.CompanyCoq() : undefined;
+ });
+ }
+
+ _setupDragDrop() {
$(this.layout.ide).on('dragover', (evt) => {
evt.preventDefault();
evt.originalEvent.dataTransfer.dropEffect = 'link';
diff --git a/ui-js/jscoq-loader.js b/ui-js/jscoq-loader.js
index 87434c5b261938963d4dbd71f1e04f9fef39c195..deed1882a88ab38e4e39390dd982e73cd028b0ec 100644
--- a/ui-js/jscoq-loader.js
+++ b/ui-js/jscoq-loader.js
@@ -65,6 +65,7 @@ var loadJsCoq, JsCoq;
loadCss(base_path + 'ui-css/coq-base');
loadCss(base_path + 'ui-css/coq-light');
loadCss(base_path + 'ui-css/coq-dark');
+ loadCss(base_path + 'ui-css/settings');
var files = [node_modules_path + 'codemirror/lib/codemirror',
node_modules_path + 'codemirror/keymap/emacs',
@@ -81,6 +82,7 @@ var loadJsCoq, JsCoq;
base_path + 'ui-js/addon/company-coq',
base_path + 'ui-js/cm-provider',
base_path + 'ui-js/format-pprint',
+ base_path + 'ui-js/settings',
base_path + 'ui-js/coq-packages',
base_path + 'ui-js/coq-layout-classic',
base_path + 'ui-js/coq-manager'];
diff --git a/ui-js/settings.js b/ui-js/settings.js
new file mode 100644
index 0000000000000000000000000000000000000000..ce92c665a19174050edb3fb1f019f929996371fe
--- /dev/null
+++ b/ui-js/settings.js
@@ -0,0 +1,116 @@
+
+class SettingsPanel {
+ html() {
+ return `
+ <div class="settings-panel" tabindex="0">
+ <div>
+ <label for="settings--theme">
+ <div class="setting">
+ Light switch
+ <div class="switch rocker rocker-small">
+ <input id="settings--theme" type="checkbox" checked>
+ <span class="switch-left">ON</span>
+ <span class="switch-right">OFF</span>
+ </div>
+ </div>
+ </label>
+ <label for="settings--company">
+ <div class="setting">
+ Enable company-coq
+ <input id="settings--company" type="checkbox" class="switch">
+ </div>
+ </label>
+ </div>
+ <div class="links">
+ <a href="https://coq.zulipchat.com/#narrow/stream/256336-jsCoq" title="Zulip" class="link-to-zulip"></a>
+ <a href="https://github.com/jscoq/jscoq" title="GitHub" class="link-to-github"></a>
+ </div>
+ </div>
+ `;
+ }
+
+ constructor(model) {
+ this.el = $(this.html());
+ this.model = model || new CoqSettings();
+ this.active = new ReactiveVar(false);
+
+ 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;
+ });
+ // clickaway trick
+ this.el.on('blur', ev => {
+ if (this.el.has(ev.originalEvent.relatedTarget).length)
+ setTimeout(() => this.el[0].focus(), 1);
+ else
+ this.hide();
+ });
+ }
+
+ 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() {
+ if (this.el.parent().length == 0)
+ $(document.body).append(this.el);
+ this.el.show();
+ this.active.value = true;
+ setTimeout(() => this.el[0].focus(), 10); // avoid race between panel and button
+ }
+
+ hide() {
+ this.active.value = false;
+ this.el.hide();
+ }
+
+ toggle() {
+ if (this.isVisible()) this.hide();
+ else this.show();
+ return this.isVisible();
+ }
+
+ isVisible() {
+ return this.el.is(':visible');
+ }
+}
+
+
+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) {
+ if (val !== this._value) { // do not trigger for nothing
+ this._value = val;
+ for (let o of this.observers) {
+ o(val);
+ }
+ }
+ }
+
+ observe(callback) {
+ this.observers.push(callback);
+ }
+}
\ No newline at end of file