# 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)
   }