diff -r 9efdebe24c65 -r 0ffcad1f6130 src/Pure/PIDE/editor.scala --- 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 */