--- a/src/Tools/VSCode/src/document_model.scala Fri Jun 16 22:38:19 2017 +0200
+++ b/src/Tools/VSCode/src/document_model.scala Fri Jun 16 22:40:05 2017 +0200
@@ -48,12 +48,13 @@
catch { case ERROR(_) => Nil }
}
- def init(session: Session, node_name: Document.Node.Name): Document_Model =
- Document_Model(session, node_name, Content.empty)
+ def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model =
+ Document_Model(session, editor, node_name, Content.empty)
}
sealed case class Document_Model(
session: Session,
+ editor: Server.Editor,
node_name: Document.Node.Name,
content: Document_Model.Content,
external_file: Boolean = false,
@@ -109,8 +110,10 @@
case None => Text.Perspective.empty
}
+ val overlays = editor.node_overlays(node_name)
+
(snapshot.node.load_commands_changed(doc_blobs),
- Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty))
+ Document.Node.Perspective(node_required, text_perspective, overlays))
}
else (false, Document.Node.no_perspective_text)
}