when jEdit is run from Netbeans, activate=defer does not work (why?)
authorimmler@in.tum.de
Sat, 28 Mar 2009 15:40:47 +0100
changeset 34543 b32b20f0692f
parent 34542 e647f063ffad
child 34544 56217d219e27
when jEdit is run from Netbeans, activate=defer does not work (why?)
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