src/Pure/PIDE/query_operation.scala
changeset 56662 f373fb77e0a4
parent 56372 fadb0fef09d7
child 56715 52125652e82a
     1.1 --- a/src/Pure/PIDE/query_operation.scala	Tue Apr 22 23:31:45 2014 +0200
     1.2 +++ b/src/Pure/PIDE/query_operation.scala	Tue Apr 22 23:49:15 2014 +0200
     1.3 @@ -65,7 +65,7 @@
     1.4  
     1.5    private def content_update()
     1.6    {
     1.7 -    Swing_Thread.require()
     1.8 +    Swing_Thread.require {}
     1.9  
    1.10  
    1.11      /* snapshot */
    1.12 @@ -174,7 +174,7 @@
    1.13  
    1.14    def apply_query(query: List[String])
    1.15    {
    1.16 -    Swing_Thread.require()
    1.17 +    Swing_Thread.require {}
    1.18  
    1.19      editor.current_node_snapshot(editor_context) match {
    1.20        case Some(snapshot) =>
    1.21 @@ -199,7 +199,7 @@
    1.22  
    1.23    def locate_query()
    1.24    {
    1.25 -    Swing_Thread.require()
    1.26 +    Swing_Thread.require {}
    1.27  
    1.28      for {
    1.29        command <- current_location