tuned;
authorwenzelm
Tue Sep 24 14:09:39 2013 +0200 (2013-09-24 ago)
changeset 5384075243ba102d4
parent 53839 274a892b1230
child 53841 73536e119310
tuned;
src/Pure/PIDE/query_operation.scala
     1.1 --- a/src/Pure/PIDE/query_operation.scala	Tue Sep 24 13:23:25 2013 +0200
     1.2 +++ b/src/Pure/PIDE/query_operation.scala	Tue Sep 24 14:09:39 2013 +0200
     1.3 @@ -198,7 +198,9 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  def activate() { editor.session.commands_changed += main_actor }
     1.8 +  def activate() {
     1.9 +    editor.session.commands_changed += main_actor
    1.10 +  }
    1.11  
    1.12    def deactivate() {
    1.13      editor.session.commands_changed -= main_actor