| author | wenzelm | 
| Sun, 28 Jun 2009 22:35:23 +0200 | |
| changeset 31843 | f02c6a43f1b3 | 
| parent 31828 | 31584cf201cc | 
| child 31844 | 3d5e51dbafe9 | 
| 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  | 
  {
 | 
|
19  | 
    Swing.later {
 | 
|
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  | 
|
32  | 
columns = 20  | 
|
33  | 
rows = 10  | 
|
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 =>  | 
|
48  | 
      case Some((name, None)) => text.append("platform: " + name + "\n")
 | 
|
49  | 
case Some((name1, Some(name2))) =>  | 
|
50  | 
        text.append("main platform: " + name2 + "\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  | 
||
57  | 
// reactions  | 
|
| 
31827
 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 
wenzelm 
parents:  
diff
changeset
 | 
58  | 
listenTo(ok)  | 
| 
 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 
wenzelm 
parents:  
diff
changeset
 | 
59  | 
    reactions += {
 | 
| 
 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 
wenzelm 
parents:  
diff
changeset
 | 
60  | 
case ButtonClicked(`ok`) => System.exit(0)  | 
| 
 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 
wenzelm 
parents:  
diff
changeset
 | 
61  | 
}  | 
| 
 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 
wenzelm 
parents:  
diff
changeset
 | 
62  | 
}  | 
| 
 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 
wenzelm 
parents:  
diff
changeset
 | 
63  | 
}  | 
| 
 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 
wenzelm 
parents:  
diff
changeset
 | 
64  |