author | wenzelm |
Wed, 27 Mar 2013 16:38:25 +0100 | |
changeset 51553 | 63327f679cff |
parent 50854 | 2b15227b17e8 |
child 51615 | 072a7249e1ac |
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 |
|
47710 | 11 |
import scala.swing.{ScrollPane, Button, FlowPanel, |
12 |
BorderPanel, MainFrame, TextArea, SwingApplication} |
|
36994 | 13 |
import scala.swing.event.ButtonClicked |
31827
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
wenzelm
parents:
diff
changeset
|
14 |
|
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
wenzelm
parents:
diff
changeset
|
15 |
|
36678
49918c180e8c
use SwingApplication instead of deprecated GUIApplication;
wenzelm
parents:
36207
diff
changeset
|
16 |
object GUI_Setup extends SwingApplication |
31827
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
wenzelm
parents:
diff
changeset
|
17 |
{ |
36678
49918c180e8c
use SwingApplication instead of deprecated GUIApplication;
wenzelm
parents:
36207
diff
changeset
|
18 |
def startup(args: Array[String]) = |
31828 | 19 |
{ |
36786 | 20 |
Platform.init_laf() |
36678
49918c180e8c
use SwingApplication instead of deprecated GUIApplication;
wenzelm
parents:
36207
diff
changeset
|
21 |
top.pack() |
49918c180e8c
use SwingApplication instead of deprecated GUIApplication;
wenzelm
parents:
36207
diff
changeset
|
22 |
top.visible = true |
31828 | 23 |
} |
24 |
||
31827
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
wenzelm
parents:
diff
changeset
|
25 |
def top = new MainFrame { |
50854 | 26 |
iconImage = Isabelle_System.get_icon().getImage |
27 |
||
31827
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
wenzelm
parents:
diff
changeset
|
28 |
title = "Isabelle setup" |
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
wenzelm
parents:
diff
changeset
|
29 |
|
31843 | 30 |
// components |
31 |
val text = new TextArea { |
|
32 |
editable = false |
|
31860 | 33 |
columns = 80 |
34 |
rows = 20 |
|
31843 | 35 |
} |
36994 | 36 |
val ok = new Button { text = "OK" } |
37 |
val ok_panel = new FlowPanel(FlowPanel.Alignment.Center)(ok) |
|
38 |
||
39 |
val panel = new BorderPanel |
|
47710 | 40 |
panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center |
36994 | 41 |
panel.layout(ok_panel) = BorderPanel.Position.South |
42 |
contents = panel |
|
31827
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
wenzelm
parents:
diff
changeset
|
43 |
|
31843 | 44 |
// values |
36195
9c098598db2a
system properties determine the JVM platform, not the Isabelle one;
wenzelm
parents:
36193
diff
changeset
|
45 |
if (Platform.is_windows) |
50652
ead5714cc480
tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents:
48192
diff
changeset
|
46 |
text.append("Cygwin root: " + Isabelle_System.cygwin_root() + "\n") |
41381 | 47 |
text.append("JVM name: " + Platform.jvm_name + "\n") |
36207 | 48 |
text.append("JVM platform: " + Platform.jvm_platform + "\n") |
47113
b5a5662528fb
ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
wenzelm
parents:
43661
diff
changeset
|
49 |
text.append("JVM home: " + java.lang.System.getProperty("java.home") + "\n") |
31928 | 50 |
try { |
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43650
diff
changeset
|
51 |
Isabelle_System.init() |
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43650
diff
changeset
|
52 |
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
|
53 |
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
|
54 |
val platform64 = Isabelle_System.getenv("ISABELLE_PLATFORM64") |
36197 | 55 |
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
|
56 |
text.append("Isabelle home: " + Isabelle_System.getenv("ISABELLE_HOME") + "\n") |
47467 | 57 |
val isabelle_home_windows = Isabelle_System.getenv("ISABELLE_HOME_WINDOWS") |
58 |
if (isabelle_home_windows != "") |
|
59 |
text.append("Isabelle home (Windows): " + isabelle_home_windows + "\n") |
|
48017 | 60 |
text.append("Isabelle JDK home: " + Isabelle_System.getenv("ISABELLE_JDK_HOME") + "\n") |
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43650
diff
changeset
|
61 |
} |
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43650
diff
changeset
|
62 |
catch { case ERROR(msg) => text.append(msg + "\n") } |
31843 | 63 |
|
64 |
// reactions |
|
31827
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
wenzelm
parents:
diff
changeset
|
65 |
listenTo(ok) |
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
wenzelm
parents:
diff
changeset
|
66 |
reactions += { |
48192 | 67 |
case ButtonClicked(`ok`) => sys.exit(0) |
31827
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 |
} |
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
wenzelm
parents:
diff
changeset
|
71 |