# HG changeset patch
# User wenzelm
# Date 1497381340 -7200
# Node ID 7f8eeff20f7add380126784218de7b72989ab310
# Parent  dcc685d5c3f7d0ed874680547c91c64a1190a73c
tuned signature;

diff -r dcc685d5c3f7 -r 7f8eeff20f7a 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]
 }
-
diff -r dcc685d5c3f7 -r 7f8eeff20f7a src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Jun 13 20:19:25 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Jun 13 21:15:40 2017 +0200
@@ -22,13 +22,13 @@
 
   override def session: Session = PIDE.session
 
-  override def flush(hidden: Boolean = false, purge: Boolean = false): Unit =
+  def flush_edits(hidden: Boolean = false, purge: Boolean = false): Unit =
     GUI_Thread.require {
       val (doc_blobs, edits) = Document_Model.flush_edits(hidden, purge)
       session.update(doc_blobs, edits)
     }
-
-  def purge() { flush(purge = true) }
+  override def flush(): Unit = flush_edits()
+  def purge() { flush_edits(purge = true) }
 
   private val delay1_flush =
     GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
diff -r dcc685d5c3f7 -r 7f8eeff20f7a src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue Jun 13 20:19:25 2017 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Jun 13 21:15:40 2017 +0200
@@ -77,7 +77,7 @@
     if (output_state != b) {
       PIDE.options.bool("editor_output_state") = b
       PIDE.session.update_options(PIDE.options.value)
-      PIDE.editor.flush(hidden = true)
+      PIDE.editor.flush_edits(hidden = true)
       PIDE.editor.flush()
     }
   }