src/Tools/jEdit/src/query_dockable.scala
changeset 56918 a442dc6d244d
parent 56911 dc3ba749d3b8
child 57000 c914618feef8
equal deleted inserted replaced
56917:7b65f4da136d 56918:a442dc6d244d
   296   override def focusOnDefaultComponent { for (op <- get_operation()) op.query.requestFocus }
   296   override def focusOnDefaultComponent { for (op <- get_operation()) op.query.requestFocus }
   297 
   297 
   298   select_operation()
   298   select_operation()
   299   set_content(operations_pane)
   299   set_content(operations_pane)
   300 
   300 
   301   override val detach_operation = Some(() => get_operation().foreach(_.pretty_text_area.detach))
   301   override def detach_operation =
       
   302     get_operation() match {
       
   303       case None => None
       
   304       case Some(op) => op.pretty_text_area.detach_operation
       
   305     }
   302 
   306 
   303 
   307 
   304   /* resize */
   308   /* resize */
   305 
   309 
   306   private def handle_resize(): Unit =
   310   private def handle_resize(): Unit =