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
|
Sun, 30 Dec 2012 18:23:07 +0100 |
wenzelm |
more informative error;
|
file |
diff |
annotate
|
Sat, 15 Dec 2012 12:16:16 +0100 |
wenzelm |
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
|
file |
diff |
annotate
|
Fri, 14 Dec 2012 21:26:01 +0100 |
wenzelm |
init gutter according to view properties, which improves symmetry of windows and allows use of folds etc;
|
file |
diff |
annotate
|
Fri, 14 Dec 2012 12:09:08 +0100 |
wenzelm |
more formal class Command.Results;
|
file |
diff |
annotate
|
Thu, 13 Dec 2012 17:29:23 +0100 |
wenzelm |
more careful handling of Dialog_Result, with active area and color feedback;
|
file |
diff |
annotate
|
Sat, 01 Dec 2012 19:51:43 +0100 |
wenzelm |
updated to jedit-5.0.0;
|
file |
diff |
annotate
|
Mon, 26 Nov 2012 16:22:29 +0100 |
wenzelm |
reset active areas on content update;
|
file |
diff |
annotate
|
Sun, 25 Nov 2012 20:59:32 +0100 |
wenzelm |
renamed main plugin object to PIDE;
|
file |
diff |
annotate
|
Sun, 25 Nov 2012 18:47:33 +0100 |
wenzelm |
quasi-abstract module Rendering, with Isabelle-specific implementation;
|
file |
diff |
annotate
|
Sat, 24 Nov 2012 19:01:08 +0100 |
wenzelm |
prefer buffer_edit combinator over Java-style boilerplate;
|
file |
diff |
annotate
|
Thu, 22 Nov 2012 17:01:20 +0100 |
wenzelm |
always refresh font metrics, to help window size calculation (amending 2585c81d840a);
|
file |
diff |
annotate
|
Thu, 22 Nov 2012 15:22:27 +0100 |
wenzelm |
take component width as indication if it is already visible/layed-out, to avoid multiple formatting with minimal margin;
|
file |
diff |
annotate
|
Wed, 21 Nov 2012 21:08:20 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
Thu, 04 Oct 2012 18:28:31 +0200 |
wenzelm |
Rich_Text_Area tooltips via nested Pretty_Text_Area, based on some techniques of FoldViewer plugin;
|
file |
diff |
annotate
|
Fri, 21 Sep 2012 21:24:33 +0200 |
wenzelm |
tighten margin for TextArea instead of Lobo;
|
file |
diff |
annotate
|
Fri, 21 Sep 2012 15:39:51 +0200 |
wenzelm |
some support for hovering and sendback area;
|
file |
diff |
annotate
|
Thu, 20 Sep 2012 22:25:30 +0200 |
wenzelm |
tuned painter;
|
file |
diff |
annotate
|
Thu, 20 Sep 2012 20:27:47 +0200 |
wenzelm |
no caret painting;
|
file |
diff |
annotate
|
Thu, 20 Sep 2012 20:13:42 +0200 |
wenzelm |
text_rendering as managed task, with cancellation;
|
file |
diff |
annotate
|
Wed, 19 Sep 2012 17:27:37 +0200 |
wenzelm |
more direct GUI component;
|
file |
diff |
annotate
|
Tue, 18 Sep 2012 21:04:07 +0200 |
wenzelm |
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
|
file |
diff |
annotate
|
Tue, 18 Sep 2012 19:50:09 +0200 |
wenzelm |
output is read-only;
|
file |
diff |
annotate
|
Tue, 18 Sep 2012 19:42:32 +0200 |
wenzelm |
token marker for extended syntax styles;
|
file |
diff |
annotate
|
Tue, 18 Sep 2012 19:33:45 +0200 |
wenzelm |
pass base_snapshot to enable hyperlinks into other nodes;
|
file |
diff |
annotate
|
Tue, 18 Sep 2012 14:51:12 +0200 |
wenzelm |
some actual rich text markup via XML.content_markup;
|
file |
diff |
annotate
|
Tue, 18 Sep 2012 13:18:45 +0200 |
wenzelm |
some support for inital command markup;
|
file |
diff |
annotate
|
Tue, 18 Sep 2012 11:49:23 +0200 |
wenzelm |
more static rendering state;
|
file |
diff |
annotate
|
Tue, 18 Sep 2012 11:43:05 +0200 |
wenzelm |
Pretty_Text_Area is based on Rich_Text_Area;
|
file |
diff |
annotate
|
Sun, 16 Sep 2012 20:16:28 +0200 |
wenzelm |
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
|
file |
diff |
annotate
|