author | wenzelm |
Mon, 08 Aug 2011 16:38:59 +0200 | |
changeset 44057 | fda143b5c2f5 |
parent 43661 | 39fdbd814c7f |
child 47113 | b5a5662528fb |
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 |
|
43520
cec9b95fa35d
explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents:
43514
diff
changeset
|
9 |
import java.lang.System |
cec9b95fa35d
explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents:
43514
diff
changeset
|
10 |
|
36994 | 11 |
import scala.swing.{Button, FlowPanel, BorderPanel, MainFrame, TextArea, SwingApplication} |
12 |
import scala.swing.event.ButtonClicked |
|
31827
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 |
|
36678
49918c180e8c
use SwingApplication instead of deprecated GUIApplication;
wenzelm
parents:
36207
diff
changeset
|
15 |
object GUI_Setup extends SwingApplication |
31827
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
wenzelm
parents:
diff
changeset
|
16 |
{ |
36678
49918c180e8c
use SwingApplication instead of deprecated GUIApplication;
wenzelm
parents:
36207
diff
changeset
|
17 |
def startup(args: Array[String]) = |
31828 | 18 |
{ |
36786 | 19 |
Platform.init_laf() |
36678
49918c180e8c
use SwingApplication instead of deprecated GUIApplication;
wenzelm
parents:
36207
diff
changeset
|
20 |
top.pack() |
49918c180e8c
use SwingApplication instead of deprecated GUIApplication;
wenzelm
parents:
36207
diff
changeset
|
21 |
top.visible = true |
31828 | 22 |
} |
23 |
||
31827
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
wenzelm
parents:
diff
changeset
|
24 |
def top = new MainFrame { |
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
wenzelm
parents:
diff
changeset
|
25 |
title = "Isabelle setup" |
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
wenzelm
parents:
diff
changeset
|
26 |
|
31843 | 27 |
// components |
28 |
val text = new TextArea { |
|
29 |
editable = false |
|
31860 | 30 |
columns = 80 |
31 |
rows = 20 |
|
31843 | 32 |
} |
36994 | 33 |
val ok = new Button { text = "OK" } |
34 |
val ok_panel = new FlowPanel(FlowPanel.Alignment.Center)(ok) |
|
35 |
||
36 |
val panel = new BorderPanel |
|
37 |
panel.layout(text) = BorderPanel.Position.Center |
|
38 |
panel.layout(ok_panel) = BorderPanel.Position.South |
|
39 |
contents = panel |
|
31827
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
wenzelm
parents:
diff
changeset
|
40 |
|
31843 | 41 |
// values |
36195
9c098598db2a
system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents:
36193
diff
changeset
|
42 |
if (Platform.is_windows) |
34045
bc71778a327d
simplified Cygwin setup, assuming 1.7 registry layout (version 1.5 suffers from upcaseenv problem anyway);
wenzelm
parents:
31928
diff
changeset
|
43 |
text.append("Cygwin root: " + Cygwin.check_root() + "\n") |
41381 | 44 |
text.append("JVM name: " + Platform.jvm_name + "\n") |
36207 | 45 |
text.append("JVM platform: " + Platform.jvm_platform + "\n") |
31928 | 46 |
try { |
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43650
diff
changeset
|
47 |
Isabelle_System.init() |
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43650
diff
changeset
|
48 |
text.append("ML platform: " + Isabelle_System.getenv("ML_PLATFORM") + "\n") |
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43650
diff
changeset
|
49 |
text.append("Isabelle platform: " + Isabelle_System.getenv("ISABELLE_PLATFORM") + "\n") |
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43650
diff
changeset
|
50 |
val platform64 = Isabelle_System.getenv("ISABELLE_PLATFORM64") |
36197 | 51 |
if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n") |
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43650
diff
changeset
|
52 |
text.append("Isabelle home: " + Isabelle_System.getenv("ISABELLE_HOME") + "\n") |
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43650
diff
changeset
|
53 |
text.append("Isabelle java: " + Isabelle_System.getenv("THIS_JAVA") + "\n") |
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43650
diff
changeset
|
54 |
} |
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43650
diff
changeset
|
55 |
catch { case ERROR(msg) => text.append(msg + "\n") } |
31843 | 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 |