changeset 64672 | d8e0619abb60 |
parent 64671 | 93e375bd3283 |
child 64673 | b5965890e54d |
--- a/src/Tools/VSCode/src/document_model.scala Mon Dec 26 13:21:08 2016 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Mon Dec 26 13:28:37 2016 +0100 @@ -30,7 +30,7 @@ /* edits */ def text_edits: List[Text.Edit] = - if (changed) List(Text.Edit.insert(0, doc.text)) else Nil + if (changed) List(Text.Edit.insert(0, doc.make_text)) else Nil def node_edits: List[Document.Edit_Text] = if (changed) {