update package
This commit is contained in:
parent
e064fe4dc2
commit
5b5669258f
3 changed files with 5 additions and 9848 deletions
|
|
@ -7195,7 +7195,7 @@ var EditSession = function(text, mode) {
|
||||||
this.onChange = function(e) {
|
this.onChange = function(e) {
|
||||||
var delta = e.data;
|
var delta = e.data;
|
||||||
this.$modified = true;
|
this.$modified = true;
|
||||||
if (!this.$fromUndo && this.$undoManager) {
|
if (!this.$fromUndo && this.$undoManager && !delta.ignore) {
|
||||||
this.$deltas.push(delta);
|
this.$deltas.push(delta);
|
||||||
this.$informUndoManager.schedule();
|
this.$informUndoManager.schedule();
|
||||||
}
|
}
|
||||||
|
|
@ -7457,10 +7457,10 @@ var EditSession = function(text, mode) {
|
||||||
this.setUseWorker = function(useWorker) {
|
this.setUseWorker = function(useWorker) {
|
||||||
if (this.$useWorker == useWorker)
|
if (this.$useWorker == useWorker)
|
||||||
return;
|
return;
|
||||||
|
|
||||||
if (useWorker && !this.$worker && window.Worker)
|
if (useWorker && !this.$worker && window.Worker)
|
||||||
this.$worker = mode.createWorker(this);
|
this.$worker = mode.createWorker(this);
|
||||||
|
|
||||||
if (!useWorker && this.$worker) {
|
if (!useWorker && this.$worker) {
|
||||||
this.$worker.terminate();
|
this.$worker.terminate();
|
||||||
this.$worker = null;
|
this.$worker = null;
|
||||||
|
|
|
||||||
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
Loading…
Add table
Add a link
Reference in a new issue