--- a/src/Tools/VSCode/src/document_model.scala Tue Jan 10 16:09:04 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala Tue Jan 10 16:53:05 2017 +0100
@@ -103,7 +103,7 @@
{
val (reparse, perspective) = node_perspective(doc_blobs)
if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
- val edits = node_edits(pending_edits, perspective)
+ val edits = node_edits(node_header, pending_edits, perspective)
Some((edits, copy(pending_edits = Nil, last_perspective = perspective)))
}
else None