src/Tools/VSCode/src/document_model.scala
changeset 66100 d1ad5a7458c2
parent 66054 fb0eea226a4d
child 66114 c137a9f038a6
--- 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)
   }