--- a/src/Pure/PIDE/editor.scala Fri Jun 16 22:40:05 2017 +0200
+++ b/src/Pure/PIDE/editor.scala Sat Jun 17 14:47:36 2017 +0200
@@ -14,6 +14,10 @@
def session: Session
def flush(): Unit
def invoke(): Unit
+
+
+ /* current situation */
+
def current_node(context: Context): Option[Document.Node.Name]
def current_node_snapshot(context: Context): Option[Document.Snapshot]
def node_snapshot(name: Document.Node.Name): Document.Snapshot
@@ -22,16 +26,9 @@
/* overlays */
- private val overlays = Synchronized(Document.Overlays.empty)
-
- def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
- overlays.value(name)
-
- def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
- overlays.change(_.insert(command, fn, args))
-
- def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
- overlays.change(_.remove(command, fn, args))
+ def node_overlays(name: Document.Node.Name): Document.Node.Overlays
+ def insert_overlay(command: Command, fn: String, args: List[String])
+ def remove_overlay(command: Command, fn: String, args: List[String])
/* hyperlinks */