src/Tools/jEdit/src/jedit_lib.scala
2014-07-23 ago clarified module name: facilitate alternative GUI frameworks;
2014-05-09 ago tuned signature;
2014-05-02 ago more frugal access to theory text via Reader, reduced costs for I/O text decoding;
2014-04-28 ago tuned -- fewer aliases of critical operations;
2014-04-24 ago further robustification wrt. unclear ranges;
2014-04-22 ago avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
2014-04-15 ago back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
2014-04-15 ago prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
2014-04-15 ago more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
2014-04-15 ago clarified before_caret_range: prevent continuation on next line;
2014-04-14 ago some actions to maintain spell-checker dictionary;
2014-04-07 ago tuned signature -- prefer static type Document.Node.Name;
2014-02-28 ago more regular buffer_range, despite 47e8c8daccae;
2014-02-26 ago more precise before_caret_range (looking both in space and time);
2014-02-23 ago tuned whitespace;
2014-02-23 ago clarified stretch_point_range wrt. UTF-16 surrogates;
2014-02-18 ago clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for second-last line;
2013-09-22 ago tuned;
2013-09-22 ago completion popup for history text field;
2013-09-18 ago tuned signature;
2013-08-29 ago maintain Completion_Popup.Text_Area as client property like Document_View;
2013-08-28 ago uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
2013-08-27 ago enable jEdit KeyEventWorkaround uniformly;
2013-08-27 ago avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
2013-08-27 ago more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
2013-08-24 ago strict checking of coordinates wrt. inner painter component;
2013-08-13 ago more general window_geometry;
2013-08-13 ago attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
2013-08-05 ago query process animation;
2013-08-05 ago tuned signature;
2013-06-29 ago manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
2013-03-25 ago tuned signature;
2013-03-23 ago more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
2013-03-21 ago eliminated char_width_int to avoid unclear rounding;
2013-02-06 ago more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
2013-01-12 ago more uniform Pretty.char_width;
2012-12-31 ago tuned signature;
2012-12-16 ago tuned signature: use thy_load to adapt to prover/editor specific view on sources;
2012-12-15 ago more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
2012-12-05 ago tuned signature in accordance to document operations;
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;