src/Pure/System/gui_setup.scala
author wenzelm
Wed Jun 02 11:09:26 2010 +0200 (2010-06-02 ago)
changeset 37251 72c7e636067b
parent 36994 797af3ebd5f1
child 40567 a87a6b90e900
permissions -rw-r--r--
normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
wenzelm@31827
     1
/*  Title:      Pure/System/gui_setup.scala
wenzelm@31827
     2
    Author:     Makarius
wenzelm@31827
     3
wenzelm@31827
     4
GUI for basic system setup.
wenzelm@31827
     5
*/
wenzelm@31827
     6
wenzelm@31827
     7
package isabelle
wenzelm@31827
     8
wenzelm@36994
     9
import scala.swing.{Button, FlowPanel, BorderPanel, MainFrame, TextArea, SwingApplication}
wenzelm@36994
    10
import scala.swing.event.ButtonClicked
wenzelm@31827
    11
wenzelm@31827
    12
wenzelm@36678
    13
object GUI_Setup extends SwingApplication
wenzelm@31827
    14
{
wenzelm@36678
    15
  def startup(args: Array[String]) =
wenzelm@31828
    16
  {
wenzelm@36786
    17
    Platform.init_laf()
wenzelm@36678
    18
    top.pack()
wenzelm@36678
    19
    top.visible = true
wenzelm@31828
    20
  }
wenzelm@31828
    21
wenzelm@31827
    22
  def top = new MainFrame {
wenzelm@31827
    23
    title = "Isabelle setup"
wenzelm@31827
    24
wenzelm@31843
    25
    // components
wenzelm@31843
    26
    val text = new TextArea {
wenzelm@31843
    27
      editable = false
wenzelm@31860
    28
      columns = 80
wenzelm@31860
    29
      rows = 20
wenzelm@31843
    30
    }
wenzelm@36994
    31
    val ok = new Button { text = "OK" }
wenzelm@36994
    32
    val ok_panel = new FlowPanel(FlowPanel.Alignment.Center)(ok)
wenzelm@36994
    33
wenzelm@36994
    34
    val panel = new BorderPanel
wenzelm@36994
    35
    panel.layout(text) = BorderPanel.Position.Center
wenzelm@36994
    36
    panel.layout(ok_panel) = BorderPanel.Position.South
wenzelm@36994
    37
    contents = panel
wenzelm@31827
    38
wenzelm@31843
    39
    // values
wenzelm@36195
    40
    if (Platform.is_windows)
wenzelm@34045
    41
      text.append("Cygwin root: " + Cygwin.check_root() + "\n")
wenzelm@36207
    42
    text.append("JVM platform: " + Platform.jvm_platform + "\n")
wenzelm@31928
    43
    try {
wenzelm@31928
    44
      val isabelle_system = new Isabelle_System
wenzelm@36206
    45
      text.append("ML platform: " + isabelle_system.getenv("ML_PLATFORM") + "\n")
wenzelm@36197
    46
      text.append("Isabelle platform: " + isabelle_system.getenv("ISABELLE_PLATFORM") + "\n")
wenzelm@36197
    47
      val platform64 = isabelle_system.getenv("ISABELLE_PLATFORM64")
wenzelm@36197
    48
      if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
wenzelm@36206
    49
      text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n")
wenzelm@36197
    50
      text.append("Isabelle java: " + isabelle_system.this_java() + "\n")
wenzelm@31928
    51
    } catch {
wenzelm@31928
    52
      case e: RuntimeException => text.append(e.getMessage + "\n")
wenzelm@31928
    53
    }
wenzelm@31843
    54
wenzelm@31843
    55
    // reactions
wenzelm@31827
    56
    listenTo(ok)
wenzelm@31827
    57
    reactions += {
wenzelm@31827
    58
      case ButtonClicked(`ok`) => System.exit(0)
wenzelm@31827
    59
    }
wenzelm@31827
    60
  }
wenzelm@31827
    61
}
wenzelm@31827
    62