regular activate=defer -- may debug remotely, no need to run under netbeans;
authorwenzelm
Sun, 13 Sep 2009 23:03:55 +0200
changeset 34726 da2bd88f6cdd
parent 34725 43b02b4c8e0b
child 34727 3ec545c964d5
regular activate=defer -- may debug remotely, no need to run under netbeans;
src/Tools/jEdit/plugin/Isabelle.props
--- a/src/Tools/jEdit/plugin/Isabelle.props	Sun Sep 13 14:34:50 2009 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Sun Sep 13 23:03:55 2009 +0200
@@ -9,12 +9,7 @@
 plugin.isabelle.jedit.Plugin.description=Isabelle/Isar live document editing
 
 #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
-#
-# for some reasons, activate=defer does not work when jEdit is run from Netbeans
-plugin.isabelle.jedit.Plugin.activate=startup
+plugin.isabelle.jedit.Plugin.activate=defer
 plugin.isabelle.jedit.Plugin.usePluginHome=false
 plugin.isabelle.jedit.Plugin.jars=Pure.jar core-renderer.jar scala-library.jar