tuned;

--- a/src/Pure/PIDE/query_operation.scala	Tue Sep 24 13:23:25 2013 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Tue Sep 24 14:09:39 2013 +0200
@@ -198,7 +198,9 @@
     }
   }
 
-  def activate() { editor.session.commands_changed += main_actor }
+  def activate() {
+    editor.session.commands_changed += main_actor
+  }
 
   def deactivate() {
     editor.session.commands_changed -= main_actor