diff options
Diffstat (limited to 'common/content/editor.js')
| -rw-r--r-- | common/content/editor.js | 29 |
1 files changed, 15 insertions, 14 deletions
diff --git a/common/content/editor.js b/common/content/editor.js index 2448c7cb..90baf1ed 100644 --- a/common/content/editor.js +++ b/common/content/editor.js @@ -307,6 +307,21 @@ var Editor = Module("editor", { } }); + function update(force) { + if (force !== true && tmpfile.lastModifiedTime <= lastUpdate) + return; + lastUpdate = Date.now(); + + let val = tmpfile.read(); + if (textBox) + textBox.value = val; + else { + while (editor.rootElement.firstChild) + editor.rootElement.removeChild(editor.rootElement.firstChild); + editor.rootElement.innerHTML = val; + } + } + try { var tmpfile = io.createTempFile(); if (!tmpfile) @@ -322,20 +337,6 @@ var Editor = Module("editor", { "file encoding"); let lastUpdate = Date.now(); - function update(force) { - if (force !== true && tmpfile.lastModifiedTime <= lastUpdate) - return; - lastUpdate = Date.now(); - - let val = tmpfile.read(); - if (textBox) - textBox.value = val; - else { - while (editor.rootElement.firstChild) - editor.rootElement.removeChild(editor.rootElement.firstChild); - editor.rootElement.innerHTML = val; - } - } var timer = services.Timer(update, 100, services.Timer.TYPE_REPEATING_SLACK); this.editFileExternally({ file: tmpfile.path, line: line, column: column }, cleanup); |