src/Tools/jEdit/src/rich_text_area.scala
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;
2013-06-29 wenzelm 2013-06-29 explicit Pretty_Tooltip.dismiss_all due to slightly changed focus mechanics;
2013-06-29 wenzelm 2013-06-29 tuned signature;
2013-03-29 wenzelm 2013-03-29 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
2013-03-29 wenzelm 2013-03-29 improved centering via strikethrough offset;
2013-03-28 wenzelm 2013-03-28 ghost bullet via markup, which is painted as bar under text (normally space);
2013-03-23 wenzelm 2013-03-23 retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;
2013-03-23 wenzelm 2013-03-23 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); separate JEdit_Lib.pretty_metric, with slightly closer imitation of jEdit;
2013-03-21 wenzelm 2013-03-21 eliminated char_width_int to avoid unclear rounding; clarified integer conversion for margin;
2013-03-18 wenzelm 2013-03-18 extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
2013-03-17 wenzelm 2013-03-17 explicit handling of tooltip window stack -- avoid memory leak due to not-so-weak references to disposed windows (via event handlers and other aux. components);
2013-03-16 wenzelm 2013-03-16 more elementary tooltips via mouse events (imitating parts of javax.swing.ToolTipManager) -- avoid abuse of getToolTipText to produce window as side-effect;
2013-01-16 wenzelm 2013-01-16 close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);
2013-01-12 wenzelm 2013-01-12 more uniform Pretty.char_width;
2012-12-31 wenzelm 2012-12-31 tuned imports;
2012-12-30 wenzelm 2012-12-30 tuned;
2012-12-15 wenzelm 2012-12-15 prefer more official getMenuShortcutKeyMask, in deviation to traditional jEdit technique;