src/Tools/jEdit/src/jedit_lib.scala
Tue, 18 Feb 2014 15:38:50 +0100 wenzelm clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for second-last line;
Sun, 22 Sep 2013 18:42:18 +0200 wenzelm tuned;
Sun, 22 Sep 2013 18:07:34 +0200 wenzelm completion popup for history text field;
Wed, 18 Sep 2013 15:50:59 +0200 wenzelm tuned signature;
Thu, 29 Aug 2013 12:38:33 +0200 wenzelm maintain Completion_Popup.Text_Area as client property like Document_View;
Wed, 28 Aug 2013 16:36:46 +0200 wenzelm uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
Tue, 27 Aug 2013 22:23:40 +0200 wenzelm enable jEdit KeyEventWorkaround uniformly;
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;
Tue, 27 Aug 2013 12:35:32 +0200 wenzelm more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
Sat, 24 Aug 2013 17:41:57 +0200 wenzelm strict checking of coordinates wrt. inner painter component;
Tue, 13 Aug 2013 16:15:31 +0200 wenzelm more general window_geometry;
Tue, 13 Aug 2013 13:18:26 +0200 wenzelm attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
Mon, 05 Aug 2013 23:57:29 +0200 wenzelm query process animation;
Mon, 05 Aug 2013 22:54:50 +0200 wenzelm tuned signature;
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);
Mon, 25 Mar 2013 10:37:38 +0100 wenzelm tuned signature;
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);
Thu, 21 Mar 2013 16:35:53 +0100 wenzelm eliminated char_width_int to avoid unclear rounding;
Wed, 06 Feb 2013 21:05:06 +0100 wenzelm more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
Sat, 12 Jan 2013 19:53:24 +0100 wenzelm more uniform Pretty.char_width;
Mon, 31 Dec 2012 21:01:00 +0100 wenzelm tuned signature;
Sun, 16 Dec 2012 18:44:27 +0100 wenzelm tuned signature: use thy_load to adapt to prover/editor specific view on sources;
Sat, 15 Dec 2012 21:07:52 +0100 wenzelm more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
Wed, 05 Dec 2012 12:22:55 +0100 wenzelm tuned signature in accordance to document operations;
Mon, 26 Nov 2012 16:16:47 +0100 wenzelm more general sendback properties;
Sat, 24 Nov 2012 19:01:08 +0100 wenzelm prefer buffer_edit combinator over Java-style boilerplate;
Sat, 24 Nov 2012 16:24:39 +0100 wenzelm recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
Sun, 18 Nov 2012 14:24:30 +0100 wenzelm more accurate pixel_range -- do not round offset here;
Sun, 18 Nov 2012 13:52:54 +0100 wenzelm tuned signature;
Fri, 19 Oct 2012 21:52:45 +0200 wenzelm more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
Fri, 12 Oct 2012 23:38:48 +0200 wenzelm further refinement of jEdit line range, avoiding lack of final \n;
Fri, 05 Oct 2012 14:32:56 +0200 wenzelm further support for nested tooltips;
Fri, 05 Oct 2012 13:48:22 +0200 wenzelm refer to parent frame -- relevant for floating dockables in particular;
Mon, 17 Sep 2012 18:14:54 +0200 wenzelm tuned signature;
Mon, 17 Sep 2012 18:06:34 +0200 wenzelm tuned signature;
Mon, 17 Sep 2012 17:56:10 +0200 wenzelm tuned signature;
Mon, 17 Sep 2012 17:49:11 +0200 wenzelm somewhat more general JEdit_Lib;
less more (0) tip