2016-12-20 wenzelm 2016-12-20 clarified module name;
2016-06-08 wenzelm 2016-06-08 proper noWordSep as in "isabelle" mode (cf. 5024d0c48e02);
2016-04-19 wenzelm 2016-04-19 more thorough update;
2016-01-20 wenzelm 2016-01-20 bypass input method for better imitation of read-only mode (cf. f26a4d5e82b5): e.g. relevant for composition of ALT-u u on Mac OS X;
2015-11-04 wenzelm 2015-11-04 dummy input handler to imitate former read-only mode, which has changed its meaning in jedit-5.3.0 as mere hint for saving;
2015-11-03 wenzelm 2015-11-03 prefer Isabelle/Scala Future;
2015-11-03 wenzelm 2015-11-03 clarified modules;
2015-09-19 wenzelm 2015-09-19 tuned;
2015-05-03 wenzelm 2015-05-03 proper fold painter according to jEdit options, not the hardwired default of JEditEmbeddedTextArea;
2015-01-05 wenzelm 2015-01-05 GUI.imitate_font: more explicit result size, e.g. relevant for caching; some graphview font options: Helvetica family is important for self-contained PDF; tuned;
2015-01-01 wenzelm 2015-01-01 tuned;
2014-12-02 wenzelm 2014-12-02 node-specific syntax, with base_syntax as default; clarified Document_Model.init: convergence of editor events towards buffer-specific token marker;
2014-12-01 wenzelm 2014-12-01 clarified token marker / syntax for mode vs. buffer;
2014-10-30 wenzelm 2014-10-30 hardwired imitation of copy.shortcut2 default;
2014-10-22 wenzelm 2014-10-22 tuned imports;
2014-07-23 wenzelm 2014-07-23 clarified module name: facilitate alternative GUI frameworks;
2014-05-21 wenzelm 2014-05-21 tuned signature;
2014-05-08 wenzelm 2014-05-08 clarified detach_operation: ignore empty output;
2014-05-08 wenzelm 2014-05-08 enable "PIDE" docking framework by default, and rely on its "Detach" menu item;
2014-05-06 wenzelm 2014-05-06 clarified GUI events, e.g. relevant for insert via completion;
2014-05-06 wenzelm 2014-05-06 common support for search field, which is actually a light-weight Highlighter;
2014-05-06 wenzelm 2014-05-06 more uniform detach button;
2014-05-06 wenzelm 2014-05-06 tuned signature;
2014-05-05 wenzelm 2014-05-05 tuned signature;
2014-04-29 wenzelm 2014-04-29 tuned whitespace;
2014-04-25 wenzelm 2014-04-25 tuned signature -- separate pool for JFuture tasks, which can be canceled;
2014-04-24 wenzelm 2014-04-24 tuned signature;
2014-04-22 wenzelm 2014-04-22 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
2014-04-02 wenzelm 2014-04-02 observe extra line spacing for output as well;
2014-03-29 wenzelm 2014-03-29 do not absorb vacuous copy operation, e.g. relevant when tooltip has focus but no selection, while the main text area has a selection but no focus;
2014-03-01 wenzelm 2014-03-01 tuned;
2014-03-01 wenzelm 2014-03-01 tuned signature -- separate module Font_Info;
2013-08-29 wenzelm 2013-08-29 more uniform configuration of editor modes and token markers;
2013-08-28 wenzelm 2013-08-28 dismiss popups more uniformly;
2013-08-27 wenzelm 2013-08-27 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus; uniform JEdit_Lib.propagate_key;
2013-08-27 wenzelm 2013-08-27 more standard key handling according to jEdit (with workaround); clarified handling of ESCAPE (again): dismiss without second interpretation as select-none;
2013-08-27 wenzelm 2013-08-27 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
2013-08-24 wenzelm 2013-08-24 tuned signature;
2013-08-13 wenzelm 2013-08-13 imitate "noWordSep" of isabelle mode, e.g. relevant for word selection via double-click;
2013-08-13 wenzelm 2013-08-13 support somewhat standard "select all" by default;
2013-08-12 wenzelm 2013-08-12 tuned signature;
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-05 wenzelm 2013-07-05 explicit module Document_ID as source of globally unique identifiers across ML/Scala;
2013-07-04 wenzelm 2013-07-04 separate exec_id assignment for Command.print states, without affecting result of eval; tuned signature; tuned;
2013-06-29 wenzelm 2013-06-29 more aggresive ESCAPE handling, while retaining its regular meaning for jEdit;
2013-06-29 wenzelm 2013-06-29 manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6); more explicit tooltip hierarchy: manage exactly the visible stack -- caching is part of PopupFactory; auxiliary geometry measurement via single hidden window; tuned signature;
2013-03-23 wenzelm 2013-03-23 reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;
2013-03-23 wenzelm 2013-03-23 no censorship of "view.fracFontMetrics", although it often degrades rendering quality;
2013-03-23 wenzelm 2013-03-23 apply small result immediately, to avoid visible delay of text update after window move;
2013-03-23 wenzelm 2013-03-23 allow fractional pretty margin -- avoid premature rounding;
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-18 wenzelm 2013-03-18 recovered special background handling from 8d6e478934dc, particularly relevant for gutter border;
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 precise tooltip window size (NB: dimensions are known after layout pack, before making content visible); more precise margin width based on fractional Pretty.char_width (avoid multiplication of rounding errors); early initialization of gutter to get proper text area painter size (see also 2585c81d840a);
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;
2013-01-05 wenzelm 2013-01-05 propagate keys to enclosing view like org.gjt.sp.jedit.gui.CompletionPopup, but without its KeyEventInterceptor;
2013-01-04 wenzelm 2013-01-04 more elementary key handling: listen to low-level KEY_PRESSED events (without consuming);