| Sat, 01 Mar 2014 19:43:35 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 01 Mar 2014 19:39:27 +0100 |
wenzelm |
tuned signature -- separate module Font_Info;
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 13:53:45 +0200 |
wenzelm |
more uniform configuration of editor modes and token markers;
|
file |
diff |
annotate
|
| Wed, 28 Aug 2013 09:36:05 +0200 |
wenzelm |
dismiss popups more uniformly;
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 16:45:32 +0200 |
wenzelm |
avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 13:07:31 +0200 |
wenzelm |
more standard key handling according to jEdit (with workaround);
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 12:35:32 +0200 |
wenzelm |
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
|
file |
diff |
annotate
|
| Sat, 24 Aug 2013 15:30:50 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 12:48:06 +0200 |
wenzelm |
imitate "noWordSep" of isabelle mode, e.g. relevant for word selection via double-click;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 12:19:45 +0200 |
wenzelm |
support somewhat standard "select all" by default;
|
file |
diff |
annotate
|
| Mon, 12 Aug 2013 11:49:58 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 07 Jul 2013 18:04:46 +0200 |
wenzelm |
some attempts to avoid sandwiching of actions stemming from single ESCAPE key event, to avoid potential conflict with ongoing text selection;
|
file |
diff |
annotate
|
| Fri, 05 Jul 2013 15:38:03 +0200 |
wenzelm |
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
|
file |
diff |
annotate
|
| Thu, 04 Jul 2013 23:51:47 +0200 |
wenzelm |
separate exec_id assignment for Command.print states, without affecting result of eval;
|
file |
diff |
annotate
|
| Sat, 29 Jun 2013 17:39:27 +0200 |
wenzelm |
more aggresive ESCAPE handling, while retaining its regular meaning for jEdit;
|
file |
diff |
annotate
|
| Sat, 29 Jun 2013 16:53:19 +0200 |
wenzelm |
manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 21:13:03 +0100 |
wenzelm |
reverted most of 5944b20c41bf -- tends to cause race condition of synchronous vs. asynchronous version;
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 19:54:15 +0100 |
wenzelm |
no censorship of "view.fracFontMetrics", although it often degrades rendering quality;
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 16:46:09 +0100 |
wenzelm |
apply small result immediately, to avoid visible delay of text update after window move;
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 13:57:46 +0100 |
wenzelm |
allow fractional pretty margin -- avoid premature rounding;
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 13:12:39 +0100 |
wenzelm |
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);
|
file |
diff |
annotate
|
| Thu, 21 Mar 2013 16:35:53 +0100 |
wenzelm |
eliminated char_width_int to avoid unclear rounding;
|
file |
diff |
annotate
|
| Mon, 18 Mar 2013 11:29:50 +0100 |
wenzelm |
extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
|
file |
diff |
annotate
|
| Mon, 18 Mar 2013 11:04:59 +0100 |
wenzelm |
recovered special background handling from 8d6e478934dc, particularly relevant for gutter border;
|
file |
diff |
annotate
|
| Sun, 17 Mar 2013 21:04:38 +0100 |
wenzelm |
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);
|
file |
diff |
annotate
|
| Sat, 16 Mar 2013 12:46:22 +0100 |
wenzelm |
more precise tooltip window size (NB: dimensions are known after layout pack, before making content visible);
|
file |
diff |
annotate
|
| Wed, 16 Jan 2013 21:09:29 +0100 |
wenzelm |
close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);
|
file |
diff |
annotate
|
| Sat, 12 Jan 2013 19:53:24 +0100 |
wenzelm |
more uniform Pretty.char_width;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2013 20:06:24 +0100 |
wenzelm |
propagate keys to enclosing view like org.gjt.sp.jedit.gui.CompletionPopup, but without its KeyEventInterceptor;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 17:37:29 +0100 |
wenzelm |
more elementary key handling: listen to low-level KEY_PRESSED events (without consuming);
|
file |
diff |
annotate
|