github/overleaf
1
0
Fork 0
mirror of https://github.com/overleaf/overleaf.git synced 2024-11-21 20:47:08 -05:00
Code Issues Projects Releases Packages Wiki Activity

update latex syntax validator (e4b016e)

Browse source
This commit is contained in:
Brian Gough 2016-10-26 15:15:18 +01:00
parent cb4380fa78
commit eab7d46fc5
2 changed files with 29 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
services/web/public/js/ace-1.2.5/mode-latex.js
View file

@ -214,18 +214,21 @@ var createLatexWorker = function (session) {
var suppressions = [];
var hints = [];
var changeHandler = null;
var docChangePending = false;
var firstPass = true;
var worker = new WorkerClient(["ace"], "ace/mode/latex_worker", "LatexWorker");
worker.attachToDocument(doc);
doc.on("change", function () {
var docChangeHandler = doc.on("change", function () {
docChangePending = true;
if(changeHandler) {
clearTimeout(changeHandler);
changeHandler = null;
}
});
selection.on("changeCursor", function () {
var cursorHandler = selection.on("changeCursor", function () {
if (docChangePending) { return; } ;
changeHandler = setTimeout(function () {
updateMarkers({cursorMoveOnly:true});
suppressions = [];
@ -307,11 +310,20 @@ var createLatexWorker = function (session) {
}
}
if (!cursorMoveOnly || suppressedChanges) {
if (firstPass) {
if (annotations.length > 0) {
var originalAnnotations = session.getAnnotations();
session.setAnnotations(originalAnnotations.concat(annotations));
};
firstPass = false;
} else {
session.setAnnotations(annotations);
}
};
};
worker.on("lint", function(results) {
if(docChangePending) { docChangePending = false; };
hints = results.data;
if (hints.length > 100) {
hints = hints.slice(0, 100); // limit to 100 errors
@ -319,14 +331,22 @@ var createLatexWorker = function (session) {
updateMarkers();
});
worker.on("terminate", function() {
if(changeHandler) {
clearTimeout(changeHandler);
changeHandler = null;
}
doc.off("change", docChangeHandler);
selection.off("changeCursor", cursorHandler);
for (var key in savedRange) {
var range = savedRange[key];
range.start.detach();
range.end.detach();
if (range.start !== cursorAnchor) { range.start.detach(); }
if (range.end !== cursorAnchor) { range.end.detach(); }
session.removeMarker(range.id);
delete savedRange[key];
}
savedRange = {};
hints = [];
suppressions = [];
session.clearAnnotations();
});
return worker;