src/Tools/VSCode/src/vscode_resources.scala
changeset 66101 0f0f294e314f
parent 66100 d1ad5a7458c2
child 66138 f7ef4c50b747
--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Jun 16 22:40:05 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sat Jun 17 14:47:36 2017 +0200
@@ -21,6 +21,7 @@
   sealed case class State(
     models: Map[JFile, Document_Model] = Map.empty,
     caret: Option[(JFile, Line.Position)] = None,
+    overlays: Document.Overlays = Document.Overlays.empty,
     pending_input: Set[JFile] = Set.empty,
     pending_output: Set[JFile] = Set.empty)
   {
@@ -49,6 +50,14 @@
           (_, model) <- models.iterator
           blob <- model.get_blob
         } yield (model.node_name -> blob)).toMap)
+
+    def change_overlay(insert: Boolean, file: JFile,
+        command: Command, fn: String, args: List[String]): State =
+      copy(
+        overlays =
+          if (insert) overlays.insert(command, fn, args)
+          else overlays.remove(command, fn, args),
+        pending_input = pending_input + file)
   }
 
 
@@ -183,6 +192,18 @@
       })
 
 
+  /* overlays */
+
+  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
+    state.value.overlays(name)
+
+  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
+    state.change(_.change_overlay(true, node_file(command.node_name), command, fn, args))
+
+  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
+    state.change(_.change_overlay(false, node_file(command.node_name), command, fn, args))
+
+
   /* resolve dependencies */
 
   def resolve_dependencies(