# HG changeset patch # User wenzelm # Date 1379513897 -7200 # Node ID 89fb20ae9b73fa22dd1ae52445c9c873d36834a8 # Parent bb15972a644debec40270963601f77ccc69802f8 limit for text height; diff -r bb15972a644d -r 89fb20ae9b73 src/Pure/System/gui.scala --- a/src/Pure/System/gui.scala Wed Sep 18 16:09:38 2013 +0200 +++ b/src/Pure/System/gui.scala Wed Sep 18 16:18:17 2013 +0200 @@ -35,10 +35,12 @@ /* simple dialogs */ - def scrollable_text(txt: String, width: Int = 60, editable: Boolean = false): ScrollPane = + def scrollable_text(txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false) + : ScrollPane = { val text = new TextArea(txt) if (width > 0) text.columns = width + if (height > 0 && split_lines(txt).length > height) text.rows = height text.editable = editable new ScrollPane(text) }