equal
deleted
inserted
replaced
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 = |