src/Tools/jEdit/src/jedit_lib.scala
2012-11-26 ago more general sendback properties;
2012-11-24 ago prefer buffer_edit combinator over Java-style boilerplate;
2012-11-24 ago recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
2012-11-18 ago more accurate pixel_range -- do not round offset here;
2012-11-18 ago tuned signature;
2012-10-19 ago more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
2012-10-12 ago further refinement of jEdit line range, avoiding lack of final \n;
2012-10-05 ago further support for nested tooltips;
2012-10-05 ago refer to parent frame -- relevant for floating dockables in particular;
2012-09-17 ago tuned signature;
2012-09-17 ago tuned signature;
2012-09-17 ago tuned signature;
2012-09-17 ago somewhat more general JEdit_Lib;