src/Pure/PIDE/editor.scala

--- a/src/Pure/PIDE/editor.scala	Tue Jun 13 20:19:25 2017 +0200
+++ b/src/Pure/PIDE/editor.scala	Tue Jun 13 21:15:40 2017 +0200
@@ -12,7 +12,7 @@
   /* session */
 
   def session: Session
-  def flush(hidden: Boolean = false, purge: Boolean = false): Unit
+  def flush(): Unit
   def invoke(): Unit
   def current_node(context: Context): Option[Document.Node.Name]
   def current_node_snapshot(context: Context): Option[Document.Snapshot]
@@ -36,12 +36,13 @@
 
   /* hyperlinks */
 
-  abstract class Hyperlink {
+  abstract class Hyperlink
+  {
     def external: Boolean = false
     def follow(context: Context): Unit
   }
+
   def hyperlink_command(
     focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
       : Option[Hyperlink]
 }
-