author | wenzelm |
Tue, 30 Jun 2009 00:14:30 +0200 | |
changeset 31856 | 73a8032ea95b |
parent 31844 | 3d5e51dbafe9 |
child 31860 | e49011bb85da |
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 |
|
31844 | 32 |
columns = 40 |
33 |
rows = 15 |
|
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 |
31844 | 46 |
if (Platform.is_windows) { |
47 |
text.append("Cygwin root: " + Cygwin.config()._1 + "\n") |
|
48 |
} |
|
31843 | 49 |
Platform.defaults match { |
50 |
case None => |
|
31844 | 51 |
case Some((name, None)) => text.append("Platform: " + name + "\n") |
31843 | 52 |
case Some((name1, Some(name2))) => |
31844 | 53 |
text.append("Main platform: " + name1 + "\n") |
54 |
text.append("Alternative platform: " + name2 + "\n") |
|
31843 | 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 |