Skip to content
Snippets Groups Projects
Unverified Commit c7095b35 authored by Shachar Itzhaky's avatar Shachar Itzhaky Committed by GitHub
Browse files

Merge pull request #239 from jscoq/v8.13+settings-panel 

Settings Panel! :chipmunk:
parents c0d14ca1 5df75f78
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 519 additions and 49 deletions
CHANGES.md
+ 1
− 0
View file @ c7095b35
......@@ -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"
---------------------------------------
......
ui-css/coq-base.css
+ 21
− 21
View file @ c7095b35
......@@ -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 {
......
ui-css/coq-dark.css
+ 27
− 4
View file @ c7095b35
......@@ -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; }*/
......
ui-css/settings.css 0 → 100644
+ 218
− 0
View file @ c7095b35
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;
}
*/
ui-images/zulip-logo.png 0 → 100644
+ 0
− 0
View file @ c7095b35
ui-images/zulip-logo.png

17.2 KiB

ui-js/addon/company-coq.js
+ 60
− 8
View file @ c7095b35
......@@ -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;
}
}
}
......
ui-js/cm-provider.js
+ 7
− 0
View file @ c7095b35
......@@ -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 => {
......
ui-js/coq-layout-classic.js
+ 41
− 12
View file @ c7095b35
......@@ -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.
*/
......
ui-js/coq-manager.js
+ 26
− 4
View file @ c7095b35
......@@ -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';
......
ui-js/jscoq-loader.js
+ 2
− 0
View file @ c7095b35
......@@ -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'];
......
ui-js/settings.js 0 → 100644
+ 116
− 0
View file @ c7095b35
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
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment