| Thu, 20 Aug 2015 21:08:47 +0200 |
wenzelm |
clarified modules, like ML version;
|
file |
diff |
annotate
|
| Thu, 20 Aug 2015 19:15:17 +0200 |
wenzelm |
tuned signature, according to ML version;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 00:01:10 +0200 |
wenzelm |
misc tuning, based on warnings by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Sat, 28 Feb 2015 21:51:34 +0100 |
wenzelm |
updated to jedit-5.2.0;
|
file |
diff |
annotate
|
| Tue, 02 Dec 2014 14:16:56 +0100 |
wenzelm |
node-specific syntax, with base_syntax as default;
|
file |
diff |
annotate
|
| Mon, 01 Dec 2014 19:25:20 +0100 |
wenzelm |
clarified token marker / syntax for mode vs. buffer;
|
file |
diff |
annotate
|
| Sun, 03 Aug 2014 17:33:38 +0200 |
wenzelm |
more robust popup geometry vs. formatted margin;
|
file |
diff |
annotate
|
| Wed, 23 Jul 2014 11:19:24 +0200 |
wenzelm |
clarified module name: facilitate alternative GUI frameworks;
|
file |
diff |
annotate
|
| Fri, 09 May 2014 21:02:15 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 02 May 2014 13:52:45 +0200 |
wenzelm |
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
|
file |
diff |
annotate
|
| Mon, 28 Apr 2014 15:29:09 +0200 |
wenzelm |
tuned -- fewer aliases of critical operations;
|
file |
diff |
annotate
|
| Thu, 24 Apr 2014 14:59:46 +0200 |
wenzelm |
further robustification wrt. unclear ranges;
|
file |
diff |
annotate
|
| Tue, 22 Apr 2014 23:49:15 +0200 |
wenzelm |
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2014 19:51:55 +0200 |
wenzelm |
back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
|
file |
diff |
annotate
|
| Tue, 15 Apr 2014 19:27:50 +0200 |
wenzelm |
prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2014 13:07:59 +0200 |
wenzelm |
more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2014 12:34:16 +0200 |
wenzelm |
clarified before_caret_range: prevent continuation on next line;
|
file |
diff |
annotate
|
| Mon, 14 Apr 2014 21:51:41 +0200 |
wenzelm |
some actions to maintain spell-checker dictionary;
|
file |
diff |
annotate
|
| Mon, 07 Apr 2014 21:23:02 +0200 |
wenzelm |
tuned signature -- prefer static type Document.Node.Name;
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 22:11:52 +0100 |
wenzelm |
more regular buffer_range, despite 47e8c8daccae;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 14:59:24 +0100 |
wenzelm |
more precise before_caret_range (looking both in space and time);
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 18:18:40 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 16:08:38 +0100 |
wenzelm |
clarified stretch_point_range wrt. UTF-16 surrogates;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 22 Sep 2013 18:42:18 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 22 Sep 2013 18:07:34 +0200 |
wenzelm |
completion popup for history text field;
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 15:50:59 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 12:38:33 +0200 |
wenzelm |
maintain Completion_Popup.Text_Area as client property like Document_View;
|
file |
diff |
annotate
|
| Wed, 28 Aug 2013 16:36:46 +0200 |
wenzelm |
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 22:23:40 +0200 |
wenzelm |
enable jEdit KeyEventWorkaround 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 12:35:32 +0200 |
wenzelm |
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
|
file |
diff |
annotate
|
| Sat, 24 Aug 2013 17:41:57 +0200 |
wenzelm |
strict checking of coordinates wrt. inner painter component;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:15:31 +0200 |
wenzelm |
more general window_geometry;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Mon, 05 Aug 2013 23:57:29 +0200 |
wenzelm |
query process animation;
|
file |
diff |
annotate
|
| Mon, 05 Aug 2013 22:54:50 +0200 |
wenzelm |
tuned signature;
|
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
|
| Mon, 25 Mar 2013 10:37:38 +0100 |
wenzelm |
tuned signature;
|
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
|
| 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;
|
file |
diff |
annotate
|
| Sat, 12 Jan 2013 19:53:24 +0100 |
wenzelm |
more uniform Pretty.char_width;
|
file |
diff |
annotate
|
| Mon, 31 Dec 2012 21:01:00 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 16 Dec 2012 18:44:27 +0100 |
wenzelm |
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Wed, 05 Dec 2012 12:22:55 +0100 |
wenzelm |
tuned signature in accordance to document operations;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 16:16:47 +0100 |
wenzelm |
more general sendback properties;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2012 19:01:08 +0100 |
wenzelm |
prefer buffer_edit combinator over Java-style boilerplate;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2012 16:24:39 +0100 |
wenzelm |
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
|
file |
diff |
annotate
|
| Sun, 18 Nov 2012 14:24:30 +0100 |
wenzelm |
more accurate pixel_range -- do not round offset here;
|
file |
diff |
annotate
|
| Sun, 18 Nov 2012 13:52:54 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 23:38:48 +0200 |
wenzelm |
further refinement of jEdit line range, avoiding lack of final \n;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2012 14:32:56 +0200 |
wenzelm |
further support for nested tooltips;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2012 13:48:22 +0200 |
wenzelm |
refer to parent frame -- relevant for floating dockables in particular;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 18:14:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 18:06:34 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 17:56:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2012 17:49:11 +0200 |
wenzelm |
somewhat more general JEdit_Lib;
|
file |
diff |
annotate
|