| author | wenzelm | 
| Mon, 19 Apr 2010 17:27:41 +0200 | |
| changeset 36205 | e86d9a10e982 | 
| parent 36197 | 2e92aca73cab | 
| child 36206 | a7d7f928d8b8 | 
| 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  | 
  {
 | 
|
| 
31862
 
53acb8ec6c51
renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing;
 
wenzelm 
parents: 
31860 
diff
changeset
 | 
19  | 
    Swing_Thread.later {
 | 
| 31828 | 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  | 
|
| 31860 | 32  | 
columns = 80  | 
33  | 
rows = 20  | 
|
| 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  | 
| 
36205
 
e86d9a10e982
check JVM platform at most once -- still non-strict to prevent potential failure during initialization of object Platform;
 
wenzelm 
parents: 
36197 
diff
changeset
 | 
46  | 
    text.append("JVM platform: " + Platform.jvm_platform + "\n")
 | 
| 
36195
 
9c098598db2a
system properties determine the JVM platform, not the Isabelle one;
 
wenzelm 
parents: 
36193 
diff
changeset
 | 
47  | 
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
 | 
48  | 
      text.append("Cygwin root: " + Cygwin.check_root() + "\n")
 | 
| 31928 | 49  | 
    try {
 | 
50  | 
val isabelle_system = new Isabelle_System  | 
|
51  | 
      text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n")
 | 
|
| 36197 | 52  | 
      text.append("Isabelle platform: " + isabelle_system.getenv("ISABELLE_PLATFORM") + "\n")
 | 
53  | 
      val platform64 = isabelle_system.getenv("ISABELLE_PLATFORM64")
 | 
|
54  | 
      if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
 | 
|
55  | 
      text.append("Isabelle java: " + isabelle_system.this_java() + "\n")
 | 
|
| 31928 | 56  | 
    } catch {
 | 
57  | 
case e: RuntimeException => text.append(e.getMessage + "\n")  | 
|
58  | 
}  | 
|
| 31843 | 59  | 
|
60  | 
// reactions  | 
|
| 
31827
 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 
wenzelm 
parents:  
diff
changeset
 | 
61  | 
listenTo(ok)  | 
| 
 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 
wenzelm 
parents:  
diff
changeset
 | 
62  | 
    reactions += {
 | 
| 
 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 
wenzelm 
parents:  
diff
changeset
 | 
63  | 
case ButtonClicked(`ok`) => System.exit(0)  | 
| 
 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 
wenzelm 
parents:  
diff
changeset
 | 
64  | 
}  | 
| 
 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 
wenzelm 
parents:  
diff
changeset
 | 
65  | 
}  | 
| 
 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 
wenzelm 
parents:  
diff
changeset
 | 
66  | 
}  | 
| 
 
b54362b9fbef
minimal GUI_Setup, which is the main class of Pure.jar;
 
wenzelm 
parents:  
diff
changeset
 | 
67  |