--- a/src/Tools/jEdit/src/jedit_editor.scala Fri Jun 16 22:40:05 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Sat Jun 17 14:47:36 2017 +0200
@@ -83,6 +83,18 @@
}
+ /* overlays */
+
+ override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
+ Document_Model.node_overlays(name)
+
+ override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
+ Document_Model.insert_overlay(command, fn, args)
+
+ override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
+ Document_Model.remove_overlay(command, fn, args)
+
+
/* navigation */
def push_position(view: View)