2016-12-20 wenzelm 2016-12-20 clarified module name;
2016-04-25 wenzelm 2016-04-25 clarified rendering;
2016-04-19 wenzelm 2016-04-19 more thorough update;
2016-04-15 wenzelm 2016-04-15 clarified rendering wrt. hyperlinks;
2016-04-15 wenzelm 2016-04-15 tuned rendering;
2016-04-14 wenzelm 2016-04-14 background color for entity def/ref focus;
2016-04-02 wenzelm 2016-04-02 more robust display of bidirectional Unicode text: enforce left-to-right;
2015-08-24 wenzelm 2015-08-24 tuned;
2015-08-24 wenzelm 2015-08-24 maintain per-thread focus context; tuned signature;
2015-08-24 wenzelm 2015-08-24 more explicit debugger caret rendering;
2015-08-12 wenzelm 2015-08-12 clarified breakpoint rendering;
2015-08-11 wenzelm 2015-08-11 tuned;
2015-05-03 wenzelm 2015-05-03 misc tuning, based on warnings by IntelliJ IDEA;
2015-01-08 wenzelm 2015-01-08 tuned;
2014-10-22 wenzelm 2014-10-22 proper line height and text base line, like regular TextAreaPainter.PaintText;
2014-08-04 wenzelm 2014-08-04 even more thorough reset on mouse drag (see also 0c63f3538639, 7e8c11011fdf);
2014-07-23 wenzelm 2014-07-23 clarified module name: facilitate alternative GUI frameworks;
2014-05-06 wenzelm 2014-05-06 more robust line_range, according to usual jEdit confusion at end of last line (see also 71c5d1f516c0);
2014-05-06 wenzelm 2014-05-06 common support for search field, which is actually a light-weight Highlighter;
2014-04-22 wenzelm 2014-04-22 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
2014-04-15 wenzelm 2014-04-15 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing; more robust point_range; tuned;
2014-04-13 wenzelm 2014-04-13 tuned;
2014-04-13 wenzelm 2014-04-13 added spell-checker completion dialog, without counting frequency of items due to empty name; tuned signature;
2014-04-13 wenzelm 2014-04-13 tuned signature;
2014-04-13 wenzelm 2014-04-13 tuned rendering -- avoid overlap with squiggly underline;
2014-04-13 wenzelm 2014-04-13 tuned signature -- explicit Spell_Checker_Variable;
2014-04-12 wenzelm 2014-04-12 more general spell_checker_elements;
2014-04-12 wenzelm 2014-04-12 added spell-checker options; support for rendering bad words;
2014-04-09 wenzelm 2014-04-09 dismiss popups more carefully (amending 7e8c11011fdf), notably allow mouse dragging within some tooltip, e.g. for text selection;
2014-04-09 wenzelm 2014-04-09 clarifed results range;
2014-04-09 wenzelm 2014-04-09 avoid confusion about pointless cursor movement with external links;
2014-04-06 wenzelm 2014-04-06 prepare "back" position for Navigator, before following hyperlink;
2014-04-04 wenzelm 2014-04-04 revert ce37fcb30cf2 for the sake of Mac OS X -- let some event listeners of jEdit reset the cursor;
2014-04-02 wenzelm 2014-04-02 tuned signature -- more explicit iterator terminology;
2014-04-02 wenzelm 2014-04-02 more uniform painting of caret, which also improves visibility in invisible state;
2014-03-31 wenzelm 2014-03-31 clear active areas (notably mouse pointer) before changing context (e.g. via hyperlink);
2014-03-31 wenzelm 2014-03-31 reset mouse pointer more decisively, for the sake of Mac OS X (despite the builtin policie of jEdit);
2014-03-29 wenzelm 2014-03-29 check global mouse status before opening tooltip, e.g. relevant when the mouse has moved outside the window and mouse events are no longer seen by this component;
2014-03-29 wenzelm 2014-03-29 dismiss all popups on mouse drags, e.g. to avoid conflict of C-hover of Isabelle/jEdit and C-selection of jEdit;
2014-03-29 wenzelm 2014-03-29 tuned rendering -- change mouse pointer for active areas;
2014-03-17 wenzelm 2014-03-17 tuned signature;
2014-02-27 wenzelm 2014-02-27 simplified rendering -- no need to over-emphasize "token_range";
2014-02-26 wenzelm 2014-02-26 improved rendering of blinking cursor;
2014-02-25 wenzelm 2014-02-25 more completion rendering: active, semantic, syntactic; tuned;
2014-02-24 wenzelm 2014-02-24 tuned colors;
2014-02-24 wenzelm 2014-02-24 clarified painting of invisible caret, e.g. focus change due to popup;
2014-02-24 wenzelm 2014-02-24 paint completion range of active popup;
2014-02-23 wenzelm 2014-02-23 clarified stretch_point_range wrt. UTF-16 surrogates; tuned;
2014-02-23 wenzelm 2014-02-23 some rendering of completion range; tuned;
2013-08-28 wenzelm 2013-08-28 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
2013-08-24 wenzelm 2013-08-24 more static values;
2013-08-24 wenzelm 2013-08-24 prefer static "control", which is determined when the mouse event happens, not when its action runs;
2013-08-24 wenzelm 2013-08-24 tuned signature;
2013-08-12 wenzelm 2013-08-12 manage hyperlinks via PIDE editor interface;
2013-08-05 wenzelm 2013-08-05 more central Pretty_Tooltip.dismissed_all -- avoid spurious crash of Rich_Text_Area.robust_body in asynchronous mouse_motion_listener;
2013-07-07 wenzelm 2013-07-07 some attempts to avoid sandwiching of actions stemming from single ESCAPE key event, to avoid potential conflict with ongoing text selection;
2013-07-01 wenzelm 2013-07-01 avoid repeated window popup when the mouse is moved over the same content (again, see also cb677987b7e3 and 0a1db0d02628);
2013-07-01 wenzelm 2013-07-01 more robust delayed invocation;
2013-07-01 wenzelm 2013-07-01 clarified tooltip timing of pending event and active state;
2013-06-29 wenzelm 2013-06-29 more direct use of screen location: avoid misplacement if parent component has already disappeared asynchronously;