equal
deleted
inserted
replaced
19 |
19 |
20 class Raw_Output_Dockable(view: View, position: String) |
20 class Raw_Output_Dockable(view: View, position: String) |
21 extends Dockable(view: View, position: String) |
21 extends Dockable(view: View, position: String) |
22 { |
22 { |
23 private val text_area = new TextArea |
23 private val text_area = new TextArea |
24 text_area.editable = false |
|
25 set_content(new ScrollPane(text_area)) |
24 set_content(new ScrollPane(text_area)) |
26 |
25 |
27 |
26 |
28 /* main actor */ |
27 /* main actor */ |
29 |
28 |