--- 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(