# HG changeset patch
# User wenzelm
# Date 1497645605 -7200
# Node ID d1ad5a7458c26443661137099e0c7c227cd5b4b6
# Parent  d1639e7877cc3e6434c708a70a5748fd5970146d
proper treatment of editor overlays;

diff -r d1639e7877cc -r d1ad5a7458c2 src/Tools/VSCode/src/document_model.scala
--- 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)
   }
diff -r d1639e7877cc -r d1ad5a7458c2 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Fri Jun 16 22:38:19 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala	Fri Jun 16 22:40:05 2017 +0200
@@ -21,6 +21,9 @@
 
 object Server
 {
+  type Editor = isabelle.Editor[Unit]
+
+
   /* Isabelle tool wrapper */
 
   private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
@@ -118,7 +121,8 @@
 
   private val delay_load: Standard_Thread.Delay =
     Standard_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
-      val (invoke_input, invoke_load) = resources.resolve_dependencies(session, file_watcher)
+      val (invoke_input, invoke_load) =
+        resources.resolve_dependencies(session, editor, file_watcher)
       if (invoke_input) delay_input.invoke()
       if (invoke_load) delay_load.invoke
     }
@@ -158,7 +162,7 @@
     }
     norm(changes)
     norm_changes.foreach(change =>
-      resources.change_model(session, file, change.text, change.range))
+      resources.change_model(session, editor, file, change.text, change.range))
 
     delay_input.invoke()
     delay_output.invoke()
@@ -430,7 +434,7 @@
 
   /* abstract editor operations */
 
-  object editor extends Editor[Unit]
+  object editor extends Server.Editor
   {
     override def session: Session = server.session
     override def flush(): Unit = resources.flush_input(session)
diff -r d1639e7877cc -r d1ad5a7458c2 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Jun 16 22:38:19 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Jun 16 22:40:05 2017 +0200
@@ -147,11 +147,16 @@
       case None => false
     }
 
-  def change_model(session: Session, file: JFile, text: String, range: Option[Line.Range] = None)
+  def change_model(
+    session: Session,
+    editor: Server.Editor,
+    file: JFile,
+    text: String,
+    range: Option[Line.Range] = None)
   {
     state.change(st =>
       {
-        val model = st.models.getOrElse(file, Document_Model.init(session, node_name(file)))
+        val model = st.models.getOrElse(file, Document_Model.init(session, editor, node_name(file)))
         val model1 = (model.change_text(text, range) getOrElse model).external(false)
         st.update_models(Some(file -> model1))
       })
@@ -180,7 +185,10 @@
 
   /* resolve dependencies */
 
-  def resolve_dependencies(session: Session, file_watcher: File_Watcher): (Boolean, Boolean) =
+  def resolve_dependencies(
+    session: Session,
+    editor: Server.Editor,
+    file_watcher: File_Watcher): (Boolean, Boolean) =
   {
     state.change_result(st =>
       {
@@ -217,7 +225,7 @@
             text <- { file_watcher.register_parent(file); read_file_content(file) }
           }
           yield {
-            val model = Document_Model.init(session, node_name)
+            val model = Document_Model.init(session, editor, node_name)
             val model1 = (model.change_text(text) getOrElse model).external(true)
             (file, model1)
           }).toList