Skip to content

Commit

Permalink
[bugfix] goNext() skipping ahead too much when there are whitespaces
Browse files Browse the repository at this point in the history 
between sentences.

[bugfix] reassureLoadPath() must be run at the same scope where the Require
occurs.
  • Loading branch information
@corwin-of-amber
corwin-of-amber committed Feb 4, 2019
1 parent c9c664e commit fd8d00d
Show file tree
Hide file tree
Showing 3 changed files with 128 additions and 46 deletions.
71 changes: 57 additions & 14 deletions coq-js/jscoq.js
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ class CoqWorker {
}

add(ontop_sid, new_sid, stm_text, resolve) {
this.sids[new_sid] = new Future();
this.sendCommand(["Add", ontop_sid, new_sid, stm_text, resolve || false]);
}

Expand All @@ -46,6 +47,8 @@ class CoqWorker {
}

cancel(sid) {
for (let i in this.sids)
if (i >= sid) this.sids[i].reject();
this.sendCommand(["Cancel", sid]);
}

Expand All @@ -61,15 +64,6 @@ class CoqWorker {
return rid;
}

queryPromise(sid, rid, query) {
let pfr = new PromiseFeedbackRoute();
rid = this.query(sid, rid, query);

this.routes[rid] = [pfr];
pfr.atexit = () => { delete this.routes[rid]; };
return pfr.promise;
}

loadPkg(base_path, pkg) {
this.sendCommand(["LoadPkg", base_path, pkg]);
}
Expand Down Expand Up @@ -102,6 +96,29 @@ class CoqWorker {
this.sendCommand(["Register", filename]);
}

// Promise-based APIs

execPromise(sid) {
this.exec(sid);

if (!this.sids[sid]) {
console.warn(`exec'd sid=${sid} that was not added (or was cancelled)`);
this.sids[sid] = new Future();
}
return this.sids[sid].promise;
}

queryPromise(sid, rid, query) {
let pfr = new PromiseFeedbackRoute();
rid = this.query(sid, rid, query);

this.routes[rid] = [pfr];
pfr.atexit = () => { delete this.routes[rid]; };
return pfr.promise;
}

// Internal event handling

coq_handler(evt) {

var msg = evt.data;
Expand Down Expand Up @@ -153,28 +170,54 @@ class CoqWorker {
console.warn(`Feedback type ${feed_tag} not handled (route ${feed_route})`);
}
}

feedProcessed(sid) {
var fut = this.sids[sid];
if (fut) fut.resolve();
}
}


class PromiseFeedbackRoute {
class Future {
constructor() {
this.promise = new Promise((resolve, reject) => {
this.resolve = resolve;
this.reject = reject;
this._resolve = resolve;
this._reject = reject;
});
this._done = false;
this._success = false;
}

resolve(val) { if (!this._done) { this._done = this._success = true; this._resolve(val); } }
reject(err) { if (!this._done) { this._done = true; this._reject(err); } }

isDone() { return this._done; }
isSuccessful() { return this._success; }
isFailed() { return this._done && !this._success; }
}


class PromiseFeedbackRoute extends Future {
constructor() {
super();
this.atexit = () => {};
this._got_message = false;
this._got_processed = false;
}

feedMessage(sid, lvl, loc, msg) {
this.atexit();
this._got_message = true;
if (this._got_processed) this.atexit();

if (lvl[0] === 'Error')
this.reject(msg);
else
this.resolve(msg);
}

feedProcessed(sid) {
/* ignore */
this._got_processed = true;
if (this._got_message) this.atexit();
}
}

Expand Down
35 changes: 33 additions & 2 deletions ui-js/cm-provider.js
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ class CmCoqProvider {
}

// If prev == null then get the first.
getNext(prev) {
getNext(prev, until) {

var start = {line : 0, ch : 0};
var doc = this.editor.getDoc();
Expand All @@ -65,6 +65,9 @@ class CmCoqProvider {
start = prev.end;
}

if (until && this.onlySpacesBetween(start, until))
return null;

// EOF
if (start.line === doc.lastLine() &&
start.ch === doc.getLine(doc.lastLine()).length) {
Expand All @@ -83,7 +86,7 @@ class CmCoqProvider {
var stm = new CmSentence(start, end,
doc.getRange({line : start.line, ch : start.ch},
{line : token.line, ch : token.end}),
token.type === 'comment'
token.type === 'comment' // XXX This is never true
);
return stm;
}
Expand Down Expand Up @@ -154,6 +157,10 @@ class CmCoqProvider {
stm.mark = mark;
}

getCursor() {
return this.editor.getCursor();
}

cursorLess(c1, c2) {

return (c1.line < c2.line ||
Expand All @@ -177,6 +184,30 @@ class CmCoqProvider {
doc.setCursor(stm.end);
}

/**
* Checks whether the range from start to end consists solely of
* whitespaces.
* @param {Pos} start starting position ({line, ch})
* @param {Pos} end ending position ({line, ch})
*/
onlySpacesBetween(start, end) {
console.warn("onlySpacesBetween", start, end);
if (start.line > end.line) return true;
var cur = {line: start.line, ch: start.ch};
while (cur.line < end.line) {
let cur_end = this.editor.getLine(cur.line).length,
portion = this.editor.getRange(cur, {line: cur.line, ch: cur_end});
if (!this._onlySpaces(portion)) return false;
cur.line++;
cur.ch = 0;
}
return this._onlySpaces(this.editor.getRange(cur, end));
}

_onlySpaces(str) {
return !!(/^\s*$/.exec(str));
}

// If any marks, then call the invalidate callback!
onCMChange(editor, evt) {

Expand Down
68 changes: 38 additions & 30 deletions ui-js/coq-manager.js
View file
Original file line number Diff line number Diff line change
Expand Up @@ -68,24 +68,23 @@ class ProviderContainer {
}

// Get the next candidate and mark it.
getNext(prev) {

var spr, next;
getNext(prev, until) {

// If we have no previous element start with the first
// snippet, else get the current one.
if (!prev) {
spr = this.snippets[0];
next = spr.getNext(null);
} else {
spr = prev.sp;
next = spr.getNext(prev);
}
// snippet, else continue with the current one.
var spr = prev ? prev.sp : this.snippets[0];

if (until && this.snippets.indexOf(spr) > this.snippets.indexOf(until.sp))
return null;

var next = spr.getNext(prev, (until && until.sp === spr) ? until.pos : null);

// We got a snippet!
if (next) {
next.sp = spr;
return next;
} else if (until && until.sp === spr) {
return null;
} else {
// Try the next snippet.
var idx = this.snippets.indexOf(spr);
Expand Down Expand Up @@ -130,6 +129,11 @@ class ProviderContainer {

}

getCursor() {
return {sp: this.currentFocus,
pos: this.currentFocus.getCursor()}
}

cursorToStart(stm) {
stm.sp.cursorToStart(stm);
}
Expand Down Expand Up @@ -234,8 +238,6 @@ class CoqManager {
goals: []
};

this.error = [];

// XXX: Initial sentence == hack
let dummyProvider = { mark : function() {},
getNext: function() { return null; },
Expand All @@ -244,6 +246,9 @@ class CoqManager {
this.doc.stm_id[1] = { text: "dummy sentence", coq_sid: 1, sp: dummyProvider };
this.doc.sentences = [this.doc.stm_id[1]];

this.error = [];
this.goTarget = null;

// XXX: Hack
this.waitForPkgs = [];

Expand Down Expand Up @@ -381,15 +386,9 @@ class CoqManager {
let cur_stm = this.doc.stm_id[nsid], exec = false;

if (this.goTarget) {
// [Modulo the same old bugs, we need a position comparison op]
if (this.provider.getAtPoint() || this.provider.afterPoint(cur_stm) ) {
// Go-to target has been reached
exec = true;
this.goTarget = false;
} else {
// We have not reached the destination, continue forward.
exec = !this.goNext(false);
}
exec = !this.goNext(false, this.goTarget);
if (exec)
this.goTarget = null;
} else {
exec = true;
}
Expand All @@ -402,7 +401,10 @@ class CoqManager {
// Gets a request to load packages
coqPending(nsid, prefix, module_names) {
let stm = this.doc.stm_id[nsid];
let ontop = this.doc.sentences[this.doc.sentences.indexOf(stm) - 1].coq_sid;
let ontop = this.doc.sentences[this.doc.sentences.indexOf(stm) - 1];

let ontop_finished = // assumes that exec is harmless if ontop was executed already...
this.coq.execPromise(ontop.coq_sid);

var pkgs_to_load = [];
for (let module_name of module_names) {
Expand All @@ -416,10 +418,10 @@ class CoqManager {
this.packages.expand();
}

this.packages.loadDeps(pkgs_to_load)
this.packages.loadDeps(pkgs_to_load).then(() => ontop_finished)
.then(() => {
this.coq.reassureLoadPath(this.packages.getLoadPath());
this.coq.resolve(ontop, nsid, stm.text)
this.coq.resolve(ontop.coq_sid, nsid, stm.text);
});
}

Expand Down Expand Up @@ -584,6 +586,8 @@ class CoqManager {
return;
}

if (this.goTarget) return;

// If we didn't load the prelude, prevent unloading it to
// workaround a bug in Coq.
if (this.doc.sentences.length <= 1) return;
Expand All @@ -609,14 +613,16 @@ class CoqManager {
}

// Return if we had success.
goNext(update_focus) {
goNext(update_focus, until) {

if (this.goTarget && !until) return false;

this.clearErrors();

let cur_stm = this.doc.sentences.last();
let cur_sid = cur_stm.coq_sid;

let next_stm = this.provider.getNext(cur_stm);
let next_stm = this.provider.getNext(cur_stm, until);

// We are the the end
if(!next_stm) { return false; }
Expand Down Expand Up @@ -654,7 +660,7 @@ class CoqManager {
if( (++this.doc.number_adds % so_threshold) === 0 )
this.coq.exec(next_sid);

return false;
return true;
}

goCursor() {
Expand All @@ -669,14 +675,16 @@ class CoqManager {
console.warn("in goCursor(): stm not registered");
}
} else {
this.goTarget = true;
this.goNext(false);
this.goTarget = this.provider.getCursor();
this.goNext(false, this.goTarget);
}
}

// Error handler.
handleError(sid, loc, msg) {

this.goTarget = null; // first of all, stop any pending additions

let err_stm = this.doc.stm_id[sid];

// The sentence has already vanished! This can happen for
Expand Down

0 comments on commit fd8d00d

Please sign in to comment.