# HG changeset patch
# User wenzelm
# Date 1380024579 -7200
# Node ID 75243ba102d41c895625489d8223c0e3566468cb
# Parent  274a892b1230c279ab1a0e793a1f3e4bc8b36105
tuned;

diff -r 274a892b1230 -r 75243ba102d4 src/Pure/PIDE/query_operation.scala
--- 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