diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -24,7 +24,7 @@
 
   override def flush()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val doc_blobs = PIDE.document_blobs()
     val edits = PIDE.document_models().flatMap(_.flushed_edits(doc_blobs))
@@ -50,7 +50,7 @@
 
   override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     JEdit_Lib.jedit_buffer(name) match {
       case Some(buffer) =>
@@ -64,7 +64,7 @@
 
   override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val text_area = view.getTextArea
     val buffer = view.getBuffer
@@ -125,7 +125,7 @@
 
   def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     push_position(view)