| changeset 61742 | fd3b214b0979 |
| parent 61680 | f7c00119e6e7 |
| child 62973 | 744266e32612 |
| 61741:adf6dd1d490e | 61742:fd3b214b0979 |
|---|---|
43 private val text = new TextArea { |
43 private val text = new TextArea { |
44 editable = false |
44 editable = false |
45 columns = 65 |
45 columns = 65 |
46 rows = 24 |
46 rows = 24 |
47 } |
47 } |
48 text.font = (new Label).font |
48 text.font = GUI.copy_font((new Label).font) |
49 |
49 |
50 private val scroll_text = new ScrollPane(text) |
50 private val scroll_text = new ScrollPane(text) |
51 |
51 |
52 |
52 |
53 /* progress */ |
53 /* progress */ |