# HG changeset patch
# User wenzelm
# Date 1260291605 -3600
# Node ID eb0f4a9ec0528c6af627aec048feb942057ef68f
# Parent  0974378d235af787057b2b151dc99903c5ca5a8a
tuned;

diff -r 0974378d235a -r eb0f4a9ec052 src/Tools/jEdit/README_BUILD
--- a/src/Tools/jEdit/README_BUILD	Tue Dec 08 17:56:53 2009 +0100
+++ b/src/Tools/jEdit/README_BUILD	Tue Dec 08 18:00:05 2009 +0100
@@ -19,9 +19,9 @@
   Netbeans Project "jEdit": install official sources as ./contrib/jEdit/.
 
 * jEdit plugins:
-    Netbeans Library "SideKick" = $HOME/.jedit/jars/SideKick.jar
-    Netbeans Library "ErrorList" = $HOME/.jedit/jars/ErrorList.jar
-    Netbeans Library "Hyperlinks" = $HOME/.jedit/jars/Hyperlinks.jar
+  Netbeans Library "SideKick" = $HOME/.jedit/jars/SideKick.jar
+  Netbeans Library "ErrorList" = $HOME/.jedit/jars/ErrorList.jar
+  Netbeans Library "Hyperlinks" = $HOME/.jedit/jars/Hyperlinks.jar
 
 * Cobra Renderer
   http://lobobrowser.org/cobra.jsp
@@ -50,3 +50,24 @@
     (3) or via JVM system properties (cf. "Run / VM Options")
     	e.g. -Disabelle.home=.../Isabelle
 
+
+Misc notes
+==========
+
+- Netbeans config/Editors/Preferences/...-CustomPreferences.xml
+
+    <entry javaType="java.lang.Integer" name="caret-blink-rate" xml:space="preserve">
+        <value><![CDATA[0]]></value>
+    </entry>
+
+-----------------------------------------------------------------------
+To run jedit with remote debugging enabled, I use the following
+command: "java
+-agentlib:jdwp=transport=dt_socket,suspend=y,server=y,address=XXXX
+-jar jedit.jar"
+
+where XXXX is any open port number you wish. The above invocation
+works for Sun's JDK 5.0.  There's an alternate incantation for earlier
+releases. (See
+http://java.sun.com/j2se/1.5.0/docs/guide/jpda/conninv.html)
+-----------------------------------------------------------------------