explicit JVM check on startup;
authorwenzelm
Wed, 22 Dec 2010 13:30:58 +0100
changeset 41382 d19b8388d4b1
parent 41381 77990a6cd558
child 41383 514bb82514df
explicit JVM check on startup;
src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Wed Dec 22 12:05:17 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Wed Dec 22 13:30:58 2010 +0100
@@ -143,6 +143,18 @@
   }
 
 
+  /* check JVM */
+
+  def check_jvm()
+  {
+    if (!Platform.is_hotspot) {
+      Library.warning_dialog(jEdit.getActiveView, "Bad Java Virtual Machine",
+        "This is " + Platform.jvm_name,
+        "Isabelle/jEdit requires Java Hotspot from Sun/Oracle/Apple!")
+    }
+  }
+
+
   /* main jEdit components */
 
   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
@@ -373,6 +385,7 @@
 
   override def start()
   {
+    Isabelle.check_jvm()
     Isabelle.setup_tooltips()
     Isabelle.system = new Isabelle_System
     Isabelle.system.install_fonts()