| Sun, 24 Mar 2019 17:24:24 +0100 |
wenzelm |
more markup for various text kinds, notably for nested formal comments;
|
file |
diff |
annotate
|
| Tue, 27 Nov 2018 23:41:37 +0100 |
wenzelm |
obsolete (see fc221fa79741);
|
file |
diff |
annotate
|
| Wed, 21 Nov 2018 14:33:30 +0100 |
wenzelm |
more comment markup;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2018 20:20:50 +0200 |
wenzelm |
more explicit status for "canceled" command within theory node;
|
file |
diff |
annotate
|
| Tue, 02 Jan 2018 15:38:22 +0100 |
wenzelm |
clarified terminology of "markdown_bullet";
|
file |
diff |
annotate
|
| Fri, 16 Jun 2017 20:44:36 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 30 May 2017 19:19:39 +0200 |
wenzelm |
clarified event handling;
|
file |
diff |
annotate
|
| Tue, 30 May 2017 15:30:00 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 30 May 2017 11:54:53 +0200 |
wenzelm |
tuned imports;
|
file |
diff |
annotate
|
| Tue, 30 May 2017 11:50:12 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 23 May 2017 20:38:34 +0200 |
wenzelm |
support text overview colors via decorations;
|
file |
diff |
annotate
|
| Tue, 14 Mar 2017 17:32:19 +0100 |
wenzelm |
always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
|
file |
diff |
annotate
|
| Sun, 12 Mar 2017 18:45:53 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 11 Mar 2017 14:03:46 +0100 |
wenzelm |
proper Map operations;
|
file |
diff |
annotate
|
| Sat, 11 Mar 2017 12:24:54 +0100 |
wenzelm |
tuned colors according to Light+ and Dark+ themes;
|
file |
diff |
annotate
|
| Sat, 11 Mar 2017 12:12:55 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 10 Mar 2017 21:47:48 +0100 |
wenzelm |
suppress irrelevant markup for VSCode;
|
file |
diff |
annotate
|
| Fri, 10 Mar 2017 16:07:20 +0100 |
wenzelm |
more compact protocol message;
|
file |
diff |
annotate
|
| Fri, 10 Mar 2017 11:03:46 +0100 |
wenzelm |
prefer type equality;
|
file |
diff |
annotate
|
| Thu, 09 Mar 2017 21:25:01 +0100 |
wenzelm |
prefer immutable bindings;
|
file |
diff |
annotate
|
| Wed, 08 Mar 2017 11:45:41 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 07 Mar 2017 18:50:42 +0100 |
wenzelm |
decorations for text color;
|
file |
diff |
annotate
|
| Tue, 07 Mar 2017 16:06:42 +0100 |
wenzelm |
decorations for spell-checker;
|
file |
diff |
annotate
|
| Tue, 07 Mar 2017 00:06:16 +0100 |
wenzelm |
maintain decorations for document (model) and update it for each editor (view);
|
file |
diff |
annotate
|
| Mon, 06 Mar 2017 18:28:48 +0100 |
wenzelm |
clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover);
|
file |
diff |
annotate
|
| Sun, 05 Mar 2017 22:32:33 +0100 |
wenzelm |
decorations for dotted underline: less intrusive;
|
file |
diff |
annotate
|
| Sat, 04 Mar 2017 21:04:44 +0100 |
wenzelm |
more general hover_message (see also JEdit_Rendering.tooltip_message);
|
file |
diff |
annotate
|
| Sat, 04 Mar 2017 13:36:06 +0100 |
wenzelm |
decorations for background and foreground colors;
|
file |
diff |
annotate
|
| Fri, 03 Mar 2017 23:21:24 +0100 |
wenzelm |
evade odd version conflicts for batch build (e.g. "vsce package");
|
file |
diff |
annotate
|
| Fri, 03 Mar 2017 23:04:12 +0100 |
wenzelm |
more robust Uri comparison, notably on Windows;
|
file |
diff |
annotate
|
| Fri, 03 Mar 2017 21:51:04 +0100 |
wenzelm |
publish decorations like diagnostics;
|
file |
diff |
annotate
|
| Fri, 03 Mar 2017 19:33:52 +0100 |
wenzelm |
support for decorations;
|
file |
diff |
annotate
|