# HG changeset patch
# User wenzelm
# Date 1293021058 -3600
# Node ID d19b8388d4b110727c4c25a98c36d27ec2bbd6af
# Parent  77990a6cd558448bfca57be4366fedcc97ee0f3e
explicit JVM check on startup;

diff -r 77990a6cd558 -r d19b8388d4b1 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()