| Sun, 13 Dec 2020 16:00:52 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 26 Nov 2020 15:18:09 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 26 Nov 2020 14:48:22 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2020 12:53:45 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2020 22:14:11 +0100 |
wenzelm |
clarified modifier: avoid confusion of CS+a as C+a;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2020 22:05:47 +0100 |
wenzelm |
tuned -- avoid deprecated operations;
|
file |
diff |
annotate
|
| Sun, 19 May 2019 18:10:45 +0200 |
wenzelm |
more thorough assignment, e.g. when "purge" removes commands that were not assigned;
|
file |
diff |
annotate
|
| Wed, 28 Nov 2018 12:05:50 +0100 |
wenzelm |
prefer Isabelle_Fonts.sans (not mono) as derived GUI font;
|
file |
diff |
annotate
|
| Tue, 01 May 2018 16:42:14 +0200 |
wenzelm |
avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
|
file |
diff |
annotate
|
| Tue, 30 Jan 2018 23:01:38 +0100 |
wenzelm |
clarified breakgain: keeping it constant avoids margin fluctuation in Pretty_Tooltip vs. Pretty_Text_Area;
|
file |
diff |
annotate
|
| Mon, 19 Jun 2017 17:28:48 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 23 May 2017 13:47:31 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 14 Mar 2017 21:11:04 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 20 Dec 2016 21:35:56 +0100 |
wenzelm |
clarified module name;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2016 19:36:45 +0200 |
wenzelm |
proper noWordSep as in "isabelle" mode (cf. 5024d0c48e02);
|
file |
diff |
annotate
|
| Tue, 19 Apr 2016 14:38:55 +0200 |
wenzelm |
more thorough update;
|
file |
diff |
annotate
|
| Wed, 20 Jan 2016 19:19:33 +0100 |
wenzelm |
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;
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 17:14:17 +0100 |
wenzelm |
dummy input handler to imitate former read-only mode, which has changed its meaning in jedit-5.3.0 as mere hint for saving;
|
file |
diff |
annotate
|
| Tue, 03 Nov 2015 16:49:44 +0100 |
wenzelm |
prefer Isabelle/Scala Future;
|
file |
diff |
annotate
|
| Tue, 03 Nov 2015 13:54:34 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 19 Sep 2015 19:40:09 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 20:21:25 +0200 |
wenzelm |
proper fold painter according to jEdit options, not the hardwired default of JEditEmbeddedTextArea;
|
file |
diff |
annotate
|
| Mon, 05 Jan 2015 14:13:38 +0100 |
wenzelm |
GUI.imitate_font: more explicit result size, e.g. relevant for caching;
|
file |
diff |
annotate
|
| Thu, 01 Jan 2015 14:21:26 +0100 |
wenzelm |
tuned;
|
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
|
| Thu, 30 Oct 2014 15:57:13 +0100 |
wenzelm |
hardwired imitation of copy.shortcut2 default;
|
file |
diff |
annotate
|
| Wed, 22 Oct 2014 17:30:58 +0200 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Wed, 23 Jul 2014 11:19:24 +0200 |
wenzelm |
clarified module name: facilitate alternative GUI frameworks;
|
file |
diff |
annotate
|
| Wed, 21 May 2014 14:42:45 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|