equal
deleted
inserted
replaced
78 } |
78 } |
79 |
79 |
80 |
80 |
81 /* simple dialogs */ |
81 /* simple dialogs */ |
82 |
82 |
83 def scrollable_text(txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false) |
83 def scrollable_text(raw_txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false) |
84 : ScrollPane = |
84 : ScrollPane = |
85 { |
85 { |
|
86 val txt = Output.clean_yxml(raw_txt) |
86 val text = new TextArea(txt) |
87 val text = new TextArea(txt) |
87 if (width > 0) text.columns = width |
88 if (width > 0) text.columns = width |
88 if (height > 0 && split_lines(txt).length > height) text.rows = height |
89 if (height > 0 && split_lines(txt).length > height) text.rows = height |
89 text.editable = editable |
90 text.editable = editable |
90 new ScrollPane(text) |
91 new ScrollPane(text) |