src/Pure/System/gui_setup.scala
author wenzelm
Sun Jun 28 16:46:00 2009 +0200 (2009-06-28)
changeset 31828 31584cf201cc
parent 31827 b54362b9fbef
child 31843 f02c6a43f1b3
permissions -rw-r--r--
sane platform look-and-feel;
wenzelm@31827
     1
/*  Title:      Pure/System/gui_setup.scala
wenzelm@31827
     2
    Author:     Makarius
wenzelm@31827
     3
wenzelm@31827
     4
GUI for basic system setup.
wenzelm@31827
     5
*/
wenzelm@31827
     6
wenzelm@31827
     7
package isabelle
wenzelm@31827
     8
wenzelm@31828
     9
import javax.swing.UIManager
wenzelm@31828
    10
wenzelm@31827
    11
import scala.swing._
wenzelm@31827
    12
import scala.swing.event._
wenzelm@31827
    13
wenzelm@31827
    14
wenzelm@31828
    15
object GUI_Setup extends GUIApplication
wenzelm@31827
    16
{
wenzelm@31828
    17
  def main(args: Array[String]) =
wenzelm@31828
    18
  {
wenzelm@31828
    19
    Swing.later {
wenzelm@31828
    20
      UIManager.setLookAndFeel(Platform.look_and_feel)
wenzelm@31828
    21
      top.pack()
wenzelm@31828
    22
      top.visible = true
wenzelm@31828
    23
    }
wenzelm@31828
    24
  }
wenzelm@31828
    25
wenzelm@31827
    26
  def top = new MainFrame {
wenzelm@31827
    27
    title = "Isabelle setup"
wenzelm@31827
    28
    val ok = new Button { text = "OK" }
wenzelm@31827
    29
wenzelm@31827
    30
    contents = new BoxPanel(Orientation.Vertical) {
wenzelm@31827
    31
      contents += ok
wenzelm@31827
    32
      border = scala.swing.Swing.EmptyBorder(20, 20, 20, 20)
wenzelm@31827
    33
    }
wenzelm@31827
    34
wenzelm@31827
    35
    listenTo(ok)
wenzelm@31827
    36
    reactions += {
wenzelm@31827
    37
      case ButtonClicked(`ok`) => System.exit(0)
wenzelm@31827
    38
    }
wenzelm@31827
    39
  }
wenzelm@31827
    40
}
wenzelm@31827
    41