282 } |
282 } |
283 |
283 |
284 private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() } |
284 private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() } |
285 |
285 |
286 private val controls = |
286 private val controls = |
287 new Wrap_Panel(Wrap_Panel.Alignment.Right)( |
287 Wrap_Panel( |
288 break_button, continue_button, step_button, step_over_button, step_out_button, |
288 List( |
289 context_label, Component.wrap(context_field), |
289 break_button, continue_button, step_button, step_over_button, step_out_button, |
290 expression_label, Component.wrap(expression_field), eval_button, sml_button, |
290 context_label, Component.wrap(context_field), |
291 pretty_text_area.search_label, pretty_text_area.search_field, zoom) |
291 expression_label, Component.wrap(expression_field), eval_button, sml_button, |
|
292 pretty_text_area.search_label, pretty_text_area.search_field, zoom), |
|
293 Wrap_Panel.Alignment.Right) |
|
294 |
292 add(controls.peer, BorderLayout.NORTH) |
295 add(controls.peer, BorderLayout.NORTH) |
293 |
296 |
294 |
297 |
295 /* focus */ |
298 /* focus */ |
296 |
299 |