src/Pure/GUI/gui.scala
changeset 53848 8d7029eb0c31
parent 53786 064cb0458071
child 53849 a3177973ca5e
equal deleted inserted replaced
53847:104a08c2be9f 53848:8d7029eb0c31
    31       laf("Nimbus") orElse laf("GTK+") getOrElse
    31       laf("Nimbus") orElse laf("GTK+") getOrElse
    32         UIManager.getCrossPlatformLookAndFeelClassName()
    32         UIManager.getCrossPlatformLookAndFeelClassName()
    33   }
    33   }
    34 
    34 
    35   def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
    35   def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
       
    36 
       
    37   def is_macos_laf(): Boolean =
       
    38     UIManager.getSystemLookAndFeelClassName() == UIManager.getLookAndFeel.getClass.getName
    36 
    39 
    37 
    40 
    38   /* simple dialogs */
    41   /* simple dialogs */
    39 
    42 
    40   def scrollable_text(txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
    43   def scrollable_text(txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)