diff options
author | 2021-08-20 19:33:39 +0200 | |
---|---|---|
committer | 2021-08-20 19:33:39 +0200 | |
commit | 9ec6ce7b5a09d16f8bdb19e8140d7cae534f2ecb (patch) | |
tree | 305fa9342853d19b40613fedb6fb2adc01581b2e | |
parent | Simplify node naming (diff) | |
download | refinery-9ec6ce7b5a09d16f8bdb19e8140d7cae534f2ecb.tar.gz refinery-9ec6ce7b5a09d16f8bdb19e8140d7cae534f2ecb.tar.zst refinery-9ec6ce7b5a09d16f8bdb19e8140d7cae534f2ecb.zip |
Make Xtext CodeMirror more robust
-rw-r--r-- | language-web/src/main/js/editor/EditorButtons.jsx | 1 | ||||
-rw-r--r-- | language-web/src/main/js/xtext/xtext-codemirror.js | 3 |
2 files changed, 3 insertions, 1 deletions
diff --git a/language-web/src/main/js/editor/EditorButtons.jsx b/language-web/src/main/js/editor/EditorButtons.jsx index f67afdbf..18139bd4 100644 --- a/language-web/src/main/js/editor/EditorButtons.jsx +++ b/language-web/src/main/js/editor/EditorButtons.jsx | |||
@@ -62,6 +62,7 @@ export default observer(() => { | |||
62 | size='small' | 62 | size='small' |
63 | className={classes.iconButton} | 63 | className={classes.iconButton} |
64 | aria-label='Show line numbers' | 64 | aria-label='Show line numbers' |
65 | value='show-line-numbers' | ||
65 | > | 66 | > |
66 | <FormatListNumberedIcon fontSize='small'/> | 67 | <FormatListNumberedIcon fontSize='small'/> |
67 | </ToggleButton> | 68 | </ToggleButton> |
diff --git a/language-web/src/main/js/xtext/xtext-codemirror.js b/language-web/src/main/js/xtext/xtext-codemirror.js index 4d50718c..d246172a 100644 --- a/language-web/src/main/js/xtext/xtext-codemirror.js +++ b/language-web/src/main/js/xtext/xtext-codemirror.js | |||
@@ -279,6 +279,7 @@ define([ | |||
279 | } | 279 | } |
280 | }; | 280 | }; |
281 | }), | 281 | }), |
282 | from: cursor, | ||
282 | to: cursor | 283 | to: cursor |
283 | }; | 284 | }; |
284 | }}); | 285 | }}); |
@@ -329,10 +330,10 @@ define([ | |||
329 | 330 | ||
330 | CodeMirrorServiceBuilder.prototype._clearAnnotations = function(annotations) { | 331 | CodeMirrorServiceBuilder.prototype._clearAnnotations = function(annotations) { |
331 | var editor = this.editor; | 332 | var editor = this.editor; |
333 | editor.clearGutter('annotations-gutter'); | ||
332 | for (var i = 0; i < annotations.length; i++) { | 334 | for (var i = 0; i < annotations.length; i++) { |
333 | var annotation = annotations[i]; | 335 | var annotation = annotations[i]; |
334 | if (annotation) { | 336 | if (annotation) { |
335 | editor.setGutterMarker(i, 'annotations-gutter', null); | ||
336 | annotations[i] = undefined; | 337 | annotations[i] = undefined; |
337 | } | 338 | } |
338 | } | 339 | } |