src/Pure/System/gui_setup.scala
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 31928 2d8e50886558
child 34045 bc71778a327d
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
     1 /*  Title:      Pure/System/gui_setup.scala
     2     Author:     Makarius
     3 
     4 GUI for basic system setup.
     5 */
     6 
     7 package isabelle
     8 
     9 import javax.swing.UIManager
    10 
    11 import scala.swing._
    12 import scala.swing.event._
    13 
    14 
    15 object GUI_Setup extends GUIApplication
    16 {
    17   def main(args: Array[String]) =
    18   {
    19     Swing_Thread.later {
    20       UIManager.setLookAndFeel(Platform.look_and_feel)
    21       top.pack()
    22       top.visible = true
    23     }
    24   }
    25 
    26   def top = new MainFrame {
    27     title = "Isabelle setup"
    28 
    29     // components
    30     val text = new TextArea {
    31       editable = false
    32       columns = 80
    33       rows = 20
    34       xLayoutAlignment = 0.5
    35     }
    36     val ok = new Button {
    37       text = "OK"
    38       xLayoutAlignment = 0.5
    39     }
    40     contents = new BoxPanel(Orientation.Vertical) {
    41       contents += text
    42       contents += ok
    43     }
    44 
    45     // values
    46     Platform.defaults match {
    47       case None =>
    48       case Some((name, None)) => text.append("Platform: " + name + "\n")
    49       case Some((name1, Some(name2))) =>
    50         text.append("Main platform: " + name1 + "\n")
    51         text.append("Alternative platform: " + name2 + "\n")
    52     }
    53     if (Platform.is_windows) {
    54       text.append("Cygwin root: " + Cygwin.config()._1 + "\n")
    55     }
    56     try {
    57       val isabelle_system = new Isabelle_System
    58       text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n")
    59     } catch {
    60       case e: RuntimeException => text.append(e.getMessage + "\n")
    61     }
    62 
    63     // reactions
    64     listenTo(ok)
    65     reactions += {
    66       case ButtonClicked(`ok`) => System.exit(0)
    67     }
    68   }
    69 }
    70