src/Pure/System/gui_setup.scala
changeset 43661 39fdbd814c7f
parent 43650 f00da558b78e
child 47113 b5a5662528fb
equal deleted inserted replaced
43660:bfc0bb115fa1 43661:39fdbd814c7f
    42     if (Platform.is_windows)
    42     if (Platform.is_windows)
    43       text.append("Cygwin root: " + Cygwin.check_root() + "\n")
    43       text.append("Cygwin root: " + Cygwin.check_root() + "\n")
    44     text.append("JVM name: " + Platform.jvm_name + "\n")
    44     text.append("JVM name: " + Platform.jvm_name + "\n")
    45     text.append("JVM platform: " + Platform.jvm_platform + "\n")
    45     text.append("JVM platform: " + Platform.jvm_platform + "\n")
    46     try {
    46     try {
    47       val isabelle_system = Isabelle_System.default
    47       Isabelle_System.init()
    48       text.append("ML platform: " + isabelle_system.getenv("ML_PLATFORM") + "\n")
    48       text.append("ML platform: " + Isabelle_System.getenv("ML_PLATFORM") + "\n")
    49       text.append("Isabelle platform: " + isabelle_system.getenv("ISABELLE_PLATFORM") + "\n")
    49       text.append("Isabelle platform: " + Isabelle_System.getenv("ISABELLE_PLATFORM") + "\n")
    50       val platform64 = isabelle_system.getenv("ISABELLE_PLATFORM64")
    50       val platform64 = Isabelle_System.getenv("ISABELLE_PLATFORM64")
    51       if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
    51       if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
    52       text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n")
    52       text.append("Isabelle home: " + Isabelle_System.getenv("ISABELLE_HOME") + "\n")
    53       text.append("Isabelle java: " + isabelle_system.this_java() + "\n")
    53       text.append("Isabelle java: " + Isabelle_System.getenv("THIS_JAVA") + "\n")
    54     } catch { case ERROR(msg) => text.append(msg + "\n") }
    54     }
       
    55     catch { case ERROR(msg) => text.append(msg + "\n") }
    55 
    56 
    56     // reactions
    57     // reactions
    57     listenTo(ok)
    58     listenTo(ok)
    58     reactions += {
    59     reactions += {
    59       case ButtonClicked(`ok`) => System.exit(0)
    60       case ButtonClicked(`ok`) => System.exit(0)