# HG changeset patch
# User wenzelm
# Date 1440182873 -7200
# Node ID ea38a1922a0b10e3f014fb1ad145aa4959769246
# Parent  dd43980dc2c663c1775710c9d27ecd91f654e4d3
more version information;

diff -r dd43980dc2c6 -r ea38a1922a0b src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala	Fri Aug 21 20:18:52 2015 +0200
+++ b/src/Pure/System/platform.scala	Fri Aug 21 20:47:53 2015 +0200
@@ -53,8 +53,17 @@
   }
 
 
+  /* JVM version */
+
+  private val Version = new Regex("""1\.(\d+)\.0_(\d+)""")
+  lazy val jvm_version =
+    System.getProperty("java.version") match {
+      case Version(a, b) => a + "u" + b
+      case a => a
+    }
+
+
   /* JVM name */
 
   val jvm_name: String = System.getProperty("java.vm.name", "")
 }
-
diff -r dd43980dc2c6 -r ea38a1922a0b src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala	Fri Aug 21 20:18:52 2015 +0200
+++ b/src/Pure/Tools/main.scala	Fri Aug 21 20:47:53 2015 +0200
@@ -50,7 +50,10 @@
               dirs = dirs, system_mode = system_mode, sessions = List(session)) == 0)
             system_dialog.return_code(0)
           else {
-            system_dialog.title("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")")
+            system_dialog.title("Isabelle build (" +
+              Isabelle_System.getenv("ML_IDENTIFIER") + " / " +
+              "jdk-" + Platform.jvm_version + "-" +
+              Isabelle_System.getenv("ISABELLE_JAVA_PLATFORM") + ")")
             system_dialog.echo("Build started for Isabelle/" + session + " ...")
 
             val (out, rc) =