Thu, 15 Oct 2015 15:06:03 +0200 |
wenzelm |
report Markdown document structure;
|
file |
diff |
annotate
|
Sat, 19 Sep 2015 20:47:11 +0200 |
wenzelm |
eliminated pointless jedit_text_overview_limit;
|
file |
diff |
annotate
|
Tue, 08 Sep 2015 21:57:18 +0200 |
wenzelm |
disable jedit_auto_resolve (again) -- too confusing;
|
file |
diff |
annotate
|
Tue, 25 Aug 2015 13:46:24 +0200 |
wenzelm |
clarified undefined_blobs: already loaded theories are suppressed;
|
file |
diff |
annotate
|
Mon, 24 Aug 2015 00:20:20 +0200 |
wenzelm |
more explicit debugger caret rendering;
|
file |
diff |
annotate
|
Wed, 19 Aug 2015 15:40:59 +0200 |
wenzelm |
disabled auto resolve, until practical consequences are more clear;
|
file |
diff |
annotate
|
Wed, 12 Aug 2015 13:53:51 +0200 |
wenzelm |
resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
|
file |
diff |
annotate
|
Wed, 12 Aug 2015 02:40:39 +0200 |
wenzelm |
tuned colors;
|
file |
diff |
annotate
|
Wed, 12 Aug 2015 02:21:00 +0200 |
wenzelm |
clarified breakpoint rendering;
|
file |
diff |
annotate
|
Mon, 10 Aug 2015 20:25:04 +0200 |
wenzelm |
tuned rendering;
|
file |
diff |
annotate
|
Mon, 10 Aug 2015 17:49:36 +0200 |
wenzelm |
added action to toggle breakpoints (on editor side);
|
file |
diff |
annotate
|
Mon, 10 Aug 2015 16:05:41 +0200 |
wenzelm |
rendering for debugger/breakpoint active state;
|
file |
diff |
annotate
|
Thu, 19 Mar 2015 15:24:40 +0100 |
wenzelm |
tuned;
|
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
|
Tue, 30 Dec 2014 23:45:03 +0100 |
wenzelm |
explicit message channel for "legacy", which is nonetheless a variant of "warning";
|
file |
diff |
annotate
|
Tue, 23 Dec 2014 20:46:42 +0100 |
wenzelm |
explicit message channels for "state", "information";
|
file |
diff |
annotate
|
Wed, 10 Dec 2014 20:51:27 +0100 |
wenzelm |
more informative gutter content: fall-back on background color, e.g. when line numbers are enabled;
|
file |
diff |
annotate
|
Tue, 09 Dec 2014 19:52:26 +0100 |
wenzelm |
proper alt_string markup (cf. 2ceb05ee0331);
|
file |
diff |
annotate
|
Tue, 21 Oct 2014 19:20:48 +0200 |
wenzelm |
added option jedit_structure_limit;
|
file |
diff |
annotate
|
Thu, 31 Jul 2014 21:29:31 +0200 |
wenzelm |
completion popup supports both ENTER and TAB (default);
|
file |
diff |
annotate
|
Sat, 28 Jun 2014 18:02:33 +0200 |
wenzelm |
jedit_completion_immediate is enabled by default: let all users participate in slightly more ambitious symbol insertion;
|
file |
diff |
annotate
|
Tue, 06 May 2014 21:29:17 +0200 |
wenzelm |
common support for search field, which is actually a light-weight Highlighter;
|
file |
diff |
annotate
|
Tue, 06 May 2014 16:08:07 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 03 May 2014 22:47:43 +0200 |
wenzelm |
support for path completion based on file-system content;
|
file |
diff |
annotate
|
Sat, 03 May 2014 20:31:29 +0200 |
wenzelm |
yet another completion option, to imitate old less ambitious behavior;
|
file |
diff |
annotate
|
Tue, 15 Apr 2014 22:19:07 +0200 |
wenzelm |
tuned default: melange of all "en" dialects;
|
file |
diff |
annotate
|
Mon, 14 Apr 2014 09:28:42 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 14 Apr 2014 09:24:47 +0200 |
wenzelm |
eliminated somewhat pointless locale parameter;
|
file |
diff |
annotate
|
Sun, 13 Apr 2014 16:42:44 +0200 |
wenzelm |
added dictionaries_selector GUI;
|
file |
diff |
annotate
|
Sat, 12 Apr 2014 21:58:58 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|