equal
deleted
inserted
replaced
4 GUI for basic system setup. |
4 GUI for basic system setup. |
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 import scala.swing._ |
9 import scala.swing.{Button, FlowPanel, BorderPanel, MainFrame, TextArea, SwingApplication} |
10 import scala.swing.event._ |
10 import scala.swing.event.ButtonClicked |
11 |
11 |
12 |
12 |
13 object GUI_Setup extends SwingApplication |
13 object GUI_Setup extends SwingApplication |
14 { |
14 { |
15 def startup(args: Array[String]) = |
15 def startup(args: Array[String]) = |
25 // components |
25 // components |
26 val text = new TextArea { |
26 val text = new TextArea { |
27 editable = false |
27 editable = false |
28 columns = 80 |
28 columns = 80 |
29 rows = 20 |
29 rows = 20 |
30 xLayoutAlignment = 0.5 |
|
31 } |
30 } |
32 val ok = new Button { |
31 val ok = new Button { text = "OK" } |
33 text = "OK" |
32 val ok_panel = new FlowPanel(FlowPanel.Alignment.Center)(ok) |
34 xLayoutAlignment = 0.5 |
33 |
35 } |
34 val panel = new BorderPanel |
36 contents = new BoxPanel(Orientation.Vertical) { |
35 panel.layout(text) = BorderPanel.Position.Center |
37 contents += text |
36 panel.layout(ok_panel) = BorderPanel.Position.South |
38 contents += ok |
37 contents = panel |
39 } |
|
40 |
38 |
41 // values |
39 // values |
42 if (Platform.is_windows) |
40 if (Platform.is_windows) |
43 text.append("Cygwin root: " + Cygwin.check_root() + "\n") |
41 text.append("Cygwin root: " + Cygwin.check_root() + "\n") |
44 text.append("JVM platform: " + Platform.jvm_platform + "\n") |
42 text.append("JVM platform: " + Platform.jvm_platform + "\n") |