Skip to content
Snippets Groups Projects
Commit 64438ed5 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

Merge branch '1334-dome-text-buffer-proxy-requires-a-state' into 'master'

Resolve "[Dome] text buffer proxy requires a state"

Closes #1334

See merge request frama-c/frama-c!4410
parents 79f40a3f aa66417b
No related branches found
No related tags found
No related merge requests found
......@@ -335,7 +335,11 @@ export class TextBuffer extends TextProxy {
const view = this.proxy;
if (view) { appendContents(view, data); }
else {
this.text = this.toText().append(textOf(data));
const state = CS.EditorState.create({ doc: this.toText() });
const offset = state.doc.length;
const changes = { from: offset, insert: data };
const transaction = state.update({ changes });
this.text = transaction.state.doc;
this.contents = undefined;
// invariant established
}
......@@ -356,9 +360,12 @@ export class TextBuffer extends TextProxy {
const view = this.proxy;
if (view) dispatchReplace(view, range, data);
else {
const doc = this.toText();
const { offset, length } = range;
this.text = doc.replace(offset, offset+length, textOf(data));
const endOffset = offset + length;
const state = CS.EditorState.create({ doc: this.toText() });
const changes = { from: offset, to: endOffset, insert: data };
const transaction = state.update({ changes });
this.text = transaction.state.doc;
// invariant preserved
}
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment