here to learn
Published
Edited
Feb 3, 2020
Importers
5 stars
leanEditor({}, invalidation)
leanEditor({
value: `-- import .src.scratch`,
}, invalidation)
import {leanEditor, leanEditorFrom, InfoView, LeanFile, leanControl, leanHL, parseLeanMsgs,
lean, serverReset, currentlyRunning, config, CoalescedTimer, CSS_CLASSES,
__LEAN_SERVER_RESTARTS, resetOpenLeanFiles,logByDefault }
with {transport, deleteIdb, deleteJSWasm, attachRunningHandlers, server}
from '@bryangingechen/hello-lean-prover'
wsUrl = 'ws://localhost:43263'
transport = {
// https://github.com/leanprover/lean-client-js/blob/master/lean-client-js-core/src/transport.ts
/* export declare type TransportError = StderrError | ConnectError;
export interface Transport {
connect(): Connection;
}
export interface Connection {
error: Event<TransportError>;
jsonMessage: Event<any>;
alive: boolean;
send(jsonMsg: any): any;
dispose(): any;
} */
const { Event } = lean;
function connect() {
const error = new Event();
const jsonMessage = new Event();
const ws = new WebSocket(wsUrl);
const conn = { error, jsonMessage, alive: true, send, dispose, ws };
let opened = false;
let openResolve = null;
const openedPromise = new Promise(resolve => (openResolve = resolve));
ws.onopen = () => {
openResolve();
opened = true;
console.log(`Lean websocket connected at ${wsUrl}`);
};
ws.onmessage = ({ data }) => {
try {
jsonMessage.fire(JSON.parse(data));
} catch (e) {
error.fire({
error: 'connect',
message: `cannot parse: ${data}, error: ${e}`
});
}
};
ws.onerror = e => {
error.fire({ error: 'websocketError' }); // websocket errors don't give much info: https://www.w3.org/TR/websockets/#concept-websocket-close-fail
};
ws.onclose = () => {
conn.alive = false;
};
function send(msg) {
if (!opened) openedPromise.then(() => ws.send(JSON.stringify(msg)));
else ws.send(JSON.stringify(msg));
}
function dispose() {
ws.close();
}
return conn;
}
return { connect };
}
server = {
__LEAN_SERVER_RESTARTS; // create dependency to be able to restart the server (this is a bit hacky)
resetOpenLeanFiles();
const server = new lean.Server(transport);
server.logMessagesToConsole = logByDefault;
server.error.on(err => console.log('error:', err));
// window.server = server; // uncomment this to allow running commands from the dev console
try {
server.connect();
} catch (e) {
console.log('Lean server: WebSocket connection failed!');
return fakeServer;
}
server.conn.ws.addEventListener('close', () => {
server.error.fire('Lean websocket closed');
});
return Generators.disposable(server, server => {
console.log('disposing lean server...');
server.dispose(); // dispose server when cell is invalidated
});
}
function attachRunningHandlers({editor, node, fileName, opts}) {
const containerDiv = node.querySelector(`.${CSS_CLASSES.LEAN_EDITOR_CONTAINER}`);
const decoTimer = new CoalescedTimer();
return [
currentlyRunning.updated.on((files) => {
containerDiv.className = `${CSS_CLASSES.LEAN_EDITOR_CONTAINER} ${files.length ? CSS_CLASSES.RUNNING : CSS_CLASSES.DONE}`;
}),
// tasks as orange lines in the gutter
server.tasks.on(({tasks, is_running}) => {
decoTimer.do(0 && config.debounceAllMessages, () => {
const min_line = opts.lineNumberFormatter(1);
const filteredTasks = tasks.filter(({file_name}) => file_name === fileName);
if (filteredTasks.length) {
filteredTasks.map(({pos_line, end_pos_line}) => {
for (let j=0; j<editor.lineCount(); j++) {
if (j+min_line >= pos_line || j+min_line < end_pos_line) {
editor.addLineClass(j, "gutter", `${CSS_CLASSES.CODE_MIRROR_GUTTER_BUSY}`);
} else {
editor.removeLineClass(j, "gutter", `${CSS_CLASSES.CODE_MIRROR_GUTTER_BUSY}`);
}
}
});
} else {
for (let j=0; j<editor.lineCount(); j++) {
editor.removeLineClass(j, "gutter", `${CSS_CLASSES.CODE_MIRROR_GUTTER_BUSY}`);
}
}
containerDiv.className = `${CSS_CLASSES.LEAN_EDITOR_CONTAINER} ${is_running ? CSS_CLASSES.RUNNING : CSS_CLASSES.DONE}`;
});
})
];
}
fakeServer = ({
conn: { alive: false },
allMessages: new lean.Event(),
error: new lean.Event(),
tasks: new lean.Event(),
alive: () => false,
roi: () => {},
fake: true
})
Purpose-built for displays of data
Observable is your go-to platform for exploring data and creating expressive data visualizations. Use reactive JavaScript notebooks for prototyping and a collaborative canvas for visual data exploration and dashboard creation.
