# HG changeset patch
# User immler@in.tum.de
# Date 1238251247 -3600
# Node ID b32b20f0692ff8a87650efbfacfbabe782cd04af
# Parent  e647f063ffad4cadd7f7ef3ec4ceb9851bcc9776
when jEdit is run from Netbeans, activate=defer does not work (why?)

diff -r e647f063ffad -r b32b20f0692f src/Tools/jEdit/plugin/Isabelle.props
--- a/src/Tools/jEdit/plugin/Isabelle.props	Mon Mar 23 21:32:14 2009 +0100
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Sat Mar 28 15:40:47 2009 +0100
@@ -11,7 +11,10 @@
 #system parameters
 # jEdit only needs to load the plugin the first time the user accesses it
 # the presence of this property (activate=defer) also tells jEdit the plugin is using the new API
-plugin.isabelle.jedit.Plugin.activate=defer
+# plugin.isabelle.jedit.Plugin.activate=defer
+#
+# for some reasons, activate=defer does not work when jEdit is run from Netbeans
+plugin.isabelle.jedit.Plugin.activate=startup
 plugin.isabelle.jedit.Plugin.usePluginHome=false
 plugin.isabelle.jedit.Plugin.jars=Pure.jar core-renderer.jar scala-library.jar