src/Tools/jEdit/src/isabelle_options.scala
2011-09-04 wenzelm 2011-09-04 property "tooltip-dismiss-delay" is edited in ms, not seconds; explicit tooltip_dismiss_delay boundaries for further robustness;
2011-08-07 wenzelm 2011-08-07 workaround for Java 1.7 where javax.swing.JComboBox<E> is generic;
2011-06-08 wenzelm 2011-06-08 moved sources -- eliminated Netbeans artifact of jedit package directory;