--- a/src/Pure/PIDE/editor.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/PIDE/editor.scala Mon Mar 01 22:22:12 2021 +0100
@@ -27,8 +27,8 @@
/* overlays */
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])
+ def insert_overlay(command: Command, fn: String, args: List[String]): Unit
+ def remove_overlay(command: Command, fn: String, args: List[String]): Unit
/* hyperlinks */