src/Pure/System/gui_setup.scala
author wenzelm
Mon, 29 Apr 2013 17:01:13 +0200
changeset 51820 142c69695785
parent 51617 4e49bba9772d
child 53582 8533b4cb8dd7
permissions -rw-r--r--
cygwin_root as optional argument; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
4ced56100757 scrollable text;
wenzelm
parents: 47467
diff changeset
    11
import scala.swing.{ScrollPane, Button, FlowPanel,
4ced56100757 scrollable text;
wenzelm
parents: 47467
diff changeset
    12
  BorderPanel, MainFrame, TextArea, SwingApplication}
36994
797af3ebd5f1 simplified alignment via FlowPanel;
wenzelm
parents: 36786
diff changeset
    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
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31827
diff changeset
    19
  {
51617
4e49bba9772d tuned signature -- concentrate GUI tools;
wenzelm
parents: 51615
diff changeset
    20
    GUI.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
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31827
diff changeset
    23
  }
31584cf201cc sane platform look-and-feel;
wenzelm
parents: 31827
diff changeset
    24
31827
b54362b9fbef minimal GUI_Setup, which is the main class of Pure.jar;
wenzelm
parents:
diff changeset
    25
  def top = new MainFrame {
51615
072a7249e1ac separate module "GUI", to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents: 50854
diff changeset
    26
    iconImage = GUI.isabelle_image()
50854
2b15227b17e8 add icon for toplevel windows;
wenzelm
parents: 50652
diff changeset
    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
f02c6a43f1b3 display some platform information;
wenzelm
parents: 31828
diff changeset
    30
    // components
f02c6a43f1b3 display some platform information;
wenzelm
parents: 31828
diff changeset
    31
    val text = new TextArea {
f02c6a43f1b3 display some platform information;
wenzelm
parents: 31828
diff changeset
    32
      editable = false
31860
e49011bb85da more display;
wenzelm
parents: 31844
diff changeset
    33
      columns = 80
e49011bb85da more display;
wenzelm
parents: 31844
diff changeset
    34
      rows = 20
31843
f02c6a43f1b3 display some platform information;
wenzelm
parents: 31828
diff changeset
    35
    }
36994
797af3ebd5f1 simplified alignment via FlowPanel;
wenzelm
parents: 36786
diff changeset
    36
    val ok = new Button { text = "OK" }
797af3ebd5f1 simplified alignment via FlowPanel;
wenzelm
parents: 36786
diff changeset
    37
    val ok_panel = new FlowPanel(FlowPanel.Alignment.Center)(ok)
797af3ebd5f1 simplified alignment via FlowPanel;
wenzelm
parents: 36786
diff changeset
    38
797af3ebd5f1 simplified alignment via FlowPanel;
wenzelm
parents: 36786
diff changeset
    39
    val panel = new BorderPanel
47710
4ced56100757 scrollable text;
wenzelm
parents: 47467
diff changeset
    40
    panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center
36994
797af3ebd5f1 simplified alignment via FlowPanel;
wenzelm
parents: 36786
diff changeset
    41
    panel.layout(ok_panel) = BorderPanel.Position.South
797af3ebd5f1 simplified alignment via FlowPanel;
wenzelm
parents: 36786
diff changeset
    42
    contents = panel
31827
b54362b9fbef minimal GUI_Setup, which is the main class of Pure.jar;
wenzelm
parents:
diff changeset
    43
31843
f02c6a43f1b3 display some platform information;
wenzelm
parents: 31828
diff changeset
    44
    // values
41381
77990a6cd558 more explicit jvm_name;
wenzelm
parents: 40567
diff changeset
    45
    text.append("JVM name: " + Platform.jvm_name + "\n")
36207
wenzelm
parents: 36206
diff changeset
    46
    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
    47
    text.append("JVM home: " + java.lang.System.getProperty("java.home") + "\n")
31928
2d8e50886558 init/check Isabelle_System;
wenzelm
parents: 31862
diff changeset
    48
    try {
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43650
diff changeset
    49
      Isabelle_System.init()
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51617
diff changeset
    50
      if (Platform.is_windows)
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51617
diff changeset
    51
        text.append("Cygwin root: " + Isabelle_System.get_cygwin_root() + "\n")
43661
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
2e92aca73cab more platform info;
wenzelm
parents: 36195
diff changeset
    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
a0007b769a34 report ISABELLE_HOME_WINDOWS;
wenzelm
parents: 47113
diff changeset
    57
      val isabelle_home_windows = Isabelle_System.getenv("ISABELLE_HOME_WINDOWS")
a0007b769a34 report ISABELLE_HOME_WINDOWS;
wenzelm
parents: 47113
diff changeset
    58
      if (isabelle_home_windows != "")
a0007b769a34 report ISABELLE_HOME_WINDOWS;
wenzelm
parents: 47113
diff changeset
    59
        text.append("Isabelle home (Windows): " + isabelle_home_windows + "\n")
48017
9f7b27635b57 tuned message;
wenzelm
parents: 47998
diff changeset
    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
f02c6a43f1b3 display some platform information;
wenzelm
parents: 31828
diff changeset
    63
f02c6a43f1b3 display some platform information;
wenzelm
parents: 31828
diff changeset
    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
07a32140ce0d prefer sys.exit from scala 2.9;
wenzelm
parents: 48017
diff changeset
    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