DeCarabas/lrparsers
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

[dingus] Parse and report status

Browse source
This commit is contained in:
John Doty 2024-10-01 07:23:59 -07:00
parent efc6eac842
commit bcf1bbb948
2 changed files with 126 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

47
dingus/dingus.js
View file

@ -1,6 +1,10 @@
// TODO: Abstract/Factor
let pending_grammar = null;
let next_grammar = null;
let pending_document = null;
let next_document = null;
const STATUS = document.getElementById("status-line");
function submit_grammar(code) {
@ -14,6 +18,17 @@ function submit_grammar(code) {
}
}
function submit_document(code) {
if (pending_document) {
console.log("Document still pending, parking it");
next_document = code;
} else {
pending_document = code;
worker.postMessage({kind: "document", data: code});
console.log("Document posted");
}
}
const worker = new Worker('worker.js');
worker.onmessage = (e) => {
const message = e.data;
@ -31,6 +46,21 @@ worker.onmessage = (e) => {
}
}
}
if (message.kind === "doc_status") {
STATUS.innerText = message.message;
if ((message.status === "ok") || (message.status === "error")) {
pending_document = null;
if (next_document) {
pending_document = next_document;
next_document = null;
worker.postMessage({kind: "document", data: pending_document});
console.log("Posted another document");
}
}
}
};
@ -44,11 +74,11 @@ function setup_editors() {
},
);
let change_timer_id = null;
let grammar_change_timer_id = null;
grammar_editor.doc.on("change", () => {
clearTimeout(change_timer_id);
change_timer_id = setTimeout(() => {
change_timer_id = null;
clearTimeout(grammar_change_timer_id);
grammar_change_timer_id = setTimeout(() => {
grammar_change_timer_id = null;
submit_grammar(grammar_editor.doc.getValue());
}, 100);
});
@ -59,6 +89,15 @@ function setup_editors() {
lineNumbers: true,
},
);
let input_change_timer_id = null;
input_editor.doc.on("change", () => {
clearTimeout(input_change_timer_id);
input_change_timer_id = setTimeout(() => {
input_change_timer_id = null;
submit_document(input_editor.doc.getValue());
}, 100);
});
}
setup_editors();