| changeset 50541 | 021f054ff1fa |
| parent 50501 | 6f41f1646617 |
| child 50773 | 205d12333fdc |
| 50540:f4aac67a6405 | 50541:021f054ff1fa |
|---|---|
35 private var current_output: List[XML.Tree] = Nil |
35 private var current_output: List[XML.Tree] = Nil |
36 |
36 |
37 |
37 |
38 /* pretty text area */ |
38 /* pretty text area */ |
39 |
39 |
40 private val pretty_text_area = new Pretty_Text_Area(view) |
40 val pretty_text_area = new Pretty_Text_Area(view) |
41 set_content(pretty_text_area) |
41 set_content(pretty_text_area) |
42 |
42 |
43 |
43 |
44 private def handle_resize() |
44 private def handle_resize() |
45 { |
45 { |