src/Tools/jEdit/src/jedit_editor.scala

--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 13:32:26 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 14:27:58 2013 +0200
@@ -15,6 +15,8 @@
 
 class JEdit_Editor extends Editor[View]
 {
+  /* session */
+
   def session: Session = PIDE.session
 
   def flush()
@@ -34,6 +36,9 @@
     )
   }
 
+
+  /* current situation */
+
   def current_context: View =
     Swing_Thread.require { jEdit.getActiveView() }
 
@@ -72,4 +77,18 @@
       }
     }
   }
+
+
+  /* overlays */
+
+  private var overlays = Document.Overlays.empty
+
+  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
+    synchronized { overlays(name) }
+
+  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
+    synchronized { overlays = overlays.insert(command, fn, args) }
+
+  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
+    synchronized { overlays = overlays.remove(command, fn, args) }
 }