src/Pure/PIDE/query_operation.scala

--- a/src/Pure/PIDE/query_operation.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -65,7 +65,7 @@
 
   private def content_update()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
 
     /* snapshot */
@@ -174,7 +174,7 @@
 
   def apply_query(query: List[String])
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     editor.current_node_snapshot(editor_context) match {
       case Some(snapshot) =>
@@ -199,7 +199,7 @@
 
   def locate_query()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     for {
       command <- current_location