| author | bulwahn | 
| Sat, 24 Oct 2009 16:55:43 +0200 | |
| changeset 33145 | 1a22f7ca1dfc | 
| parent 31928 | 2d8e50886558 | 
| child 34045 | bc71778a327d | 
| permissions | -rw-r--r-- | 
| 31827 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 1 | /* Title: Pure/System/gui_setup.scala | 
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 2 | Author: Makarius | 
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 3 | |
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 4 | GUI for basic system setup. | 
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 5 | */ | 
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 6 | |
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 7 | package isabelle | 
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 8 | |
| 31828 | 9 | import javax.swing.UIManager | 
| 10 | ||
| 31827 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 11 | import scala.swing._ | 
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 12 | import scala.swing.event._ | 
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 13 | |
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 14 | |
| 31828 | 15 | object GUI_Setup extends GUIApplication | 
| 31827 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 16 | {
 | 
| 31828 | 17 | def main(args: Array[String]) = | 
| 18 |   {
 | |
| 31862 
53acb8ec6c51
renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
 wenzelm parents: 
31860diff
changeset | 19 |     Swing_Thread.later {
 | 
| 31828 | 20 | UIManager.setLookAndFeel(Platform.look_and_feel) | 
| 21 | top.pack() | |
| 22 | top.visible = true | |
| 23 | } | |
| 24 | } | |
| 25 | ||
| 31827 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 26 |   def top = new MainFrame {
 | 
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 27 | title = "Isabelle setup" | 
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 28 | |
| 31843 | 29 | // components | 
| 30 |     val text = new TextArea {
 | |
| 31 | editable = false | |
| 31860 | 32 | columns = 80 | 
| 33 | rows = 20 | |
| 31843 | 34 | xLayoutAlignment = 0.5 | 
| 35 | } | |
| 36 |     val ok = new Button {
 | |
| 37 | text = "OK" | |
| 38 | xLayoutAlignment = 0.5 | |
| 39 | } | |
| 31827 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 40 |     contents = new BoxPanel(Orientation.Vertical) {
 | 
| 31843 | 41 | contents += text | 
| 31827 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 42 | contents += ok | 
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 43 | } | 
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 44 | |
| 31843 | 45 | // values | 
| 46 |     Platform.defaults match {
 | |
| 47 | case None => | |
| 31844 | 48 |       case Some((name, None)) => text.append("Platform: " + name + "\n")
 | 
| 31843 | 49 | case Some((name1, Some(name2))) => | 
| 31844 | 50 |         text.append("Main platform: " + name1 + "\n")
 | 
| 51 |         text.append("Alternative platform: " + name2 + "\n")
 | |
| 31843 | 52 | } | 
| 31928 | 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 | } | |
| 31843 | 62 | |
| 63 | // reactions | |
| 31827 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 64 | listenTo(ok) | 
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 65 |     reactions += {
 | 
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 66 | case ButtonClicked(`ok`) => System.exit(0) | 
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 67 | } | 
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 68 | } | 
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 69 | } | 
| 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 wenzelm parents: diff
changeset | 70 |