src/Pure/System/gui.scala
changeset 53714 89fb20ae9b73
parent 53712 ea51046be71b
child 53778 29eaacff4078
equal deleted inserted replaced
53713:bb15972a644d 53714:89fb20ae9b73
    33   def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
    33   def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
    34 
    34 
    35 
    35 
    36   /* simple dialogs */
    36   /* simple dialogs */
    37 
    37 
    38   def scrollable_text(txt: String, width: Int = 60, editable: Boolean = false): ScrollPane =
    38   def scrollable_text(txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
       
    39     : ScrollPane =
    39   {
    40   {
    40     val text = new TextArea(txt)
    41     val text = new TextArea(txt)
    41     if (width > 0) text.columns = width
    42     if (width > 0) text.columns = width
       
    43     if (height > 0 && split_lines(txt).length > height) text.rows = height
    42     text.editable = editable
    44     text.editable = editable
    43     new ScrollPane(text)
    45     new ScrollPane(text)
    44   }
    46   }
    45 
    47 
    46   private def simple_dialog(kind: Int, default_title: String,
    48   private def simple_dialog(kind: Int, default_title: String,