|
|
@ -149,14 +149,6 @@ function Editor (doNotLoadStorage, storage) { |
|
|
|
editor.getSession().setAnnotations(sourceAnnotations) |
|
|
|
editor.getSession().setAnnotations(sourceAnnotations) |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
this.onChangeSetup = function (onChange) { |
|
|
|
|
|
|
|
editor.getSession().on('change', onChange) |
|
|
|
|
|
|
|
editor.on('changeSession', function () { |
|
|
|
|
|
|
|
editor.getSession().on('change', onChange) |
|
|
|
|
|
|
|
onChange() |
|
|
|
|
|
|
|
}) |
|
|
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
this.handleErrorClick = function (errLine, errCol) { |
|
|
|
this.handleErrorClick = function (errLine, errCol) { |
|
|
|
editor.focus() |
|
|
|
editor.focus() |
|
|
|
editor.gotoLine(errLine + 1, errCol - 1, true) |
|
|
|
editor.gotoLine(errLine + 1, errCol - 1, true) |
|
|
@ -172,6 +164,13 @@ function Editor (doNotLoadStorage, storage) { |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
// Do setup on initialisation here
|
|
|
|
// Do setup on initialisation here
|
|
|
|
|
|
|
|
editor.on('changeSession', function () { |
|
|
|
|
|
|
|
event.trigger('switched', []) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
editor.getSession().on('change', function () { |
|
|
|
|
|
|
|
event.trigger('changed', []) |
|
|
|
|
|
|
|
}) |
|
|
|
|
|
|
|
}) |
|
|
|
|
|
|
|
|
|
|
|
// Unmap ctrl-t & ctrl-f
|
|
|
|
// Unmap ctrl-t & ctrl-f
|
|
|
|
editor.commands.bindKeys({ 'ctrl-t': null }) |
|
|
|
editor.commands.bindKeys({ 'ctrl-t': null }) |
|
|
|