| Sat, 01 Oct 2022 20:10:56 +0200 | 
wenzelm | 
tuned signature;
 | 
file |
diff |
annotate
 | 
| Fri, 08 Jul 2022 20:24:05 +0200 | 
wenzelm | 
more robust Scala 3 indentation, for the sake of IntelliJ IDEA;
 | 
file |
diff |
annotate
 | 
| Fri, 01 Apr 2022 17:06:10 +0200 | 
wenzelm | 
clarified formatting, for the sake of scala3;
 | 
file |
diff |
annotate
 | 
| Wed, 09 Mar 2022 16:21:14 +0100 | 
wenzelm | 
inline Isabelle symbols into source text, so that "isabelle vscode" can start up properly without access to process.env or fs;
 | 
file |
diff |
annotate
 | 
| Mon, 07 Mar 2022 16:14:14 +0100 | 
wenzelm | 
clarified char symbols: cover most European languages;
 | 
file |
diff |
annotate
 | 
| Mon, 07 Mar 2022 16:01:54 +0100 | 
wenzelm | 
more elementary Symbol.Matcher without detour via Regex (see also Pure/General/symbol_explode.ML);
 | 
file |
diff |
annotate
 | 
| Thu, 03 Mar 2022 16:05:02 +0100 | 
wenzelm | 
clarified signature;
 | 
file |
diff |
annotate
 | 
| Thu, 03 Mar 2022 15:47:54 +0100 | 
wenzelm | 
tuned signature;
 | 
file |
diff |
annotate
 | 
| Thu, 03 Mar 2022 15:39:51 +0100 | 
wenzelm | 
clarified signature;
 | 
file |
diff |
annotate
 | 
| Thu, 03 Mar 2022 13:08:25 +0100 | 
wenzelm | 
clarified signature;
 | 
file |
diff |
annotate
 | 
| Thu, 03 Mar 2022 12:40:37 +0100 | 
wenzelm | 
clarified signature;
 | 
file |
diff |
annotate
 | 
| Thu, 03 Mar 2022 12:20:27 +0100 | 
wenzelm | 
tuned signature;
 | 
file |
diff |
annotate
 | 
| Thu, 03 Mar 2022 12:08:49 +0100 | 
wenzelm | 
misc tuning, based on suggestions by IntelliJ IDEA;
 | 
file |
diff |
annotate
 | 
| Thu, 04 Mar 2021 15:41:46 +0100 | 
wenzelm | 
tuned --- fewer warnings;
 | 
file |
diff |
annotate
 | 
| Wed, 03 Mar 2021 21:58:29 +0100 | 
wenzelm | 
tuned --- fewer warnings;
 | 
file |
diff |
annotate
 | 
| Mon, 01 Mar 2021 19:41:52 +0100 | 
wenzelm | 
tuned --- fewer warnings;
 | 
file |
diff |
annotate
 | 
| Sat, 30 Jan 2021 19:36:42 +0100 | 
wenzelm | 
tuned signature: more types;
 | 
file |
diff |
annotate
 | 
| Sun, 10 Jan 2021 13:04:29 +0100 | 
wenzelm | 
more informative errors: simplify diagnosis of spurious failures reported by users;
 | 
file |
diff |
annotate
 | 
| Sat, 02 Jan 2021 20:56:08 +0100 | 
wenzelm | 
support more direct hash-consing via XML.Cache;
 | 
file |
diff |
annotate
 | 
| Thu, 10 Dec 2020 15:08:31 +0100 | 
wenzelm | 
tuned signature;
 | 
file |
diff |
annotate
 | 
| Fri, 27 Nov 2020 16:40:31 +0100 | 
wenzelm | 
unused (see 7634d33c1a79);
 | 
file |
diff |
annotate
 | 
| Wed, 01 Apr 2020 20:17:23 +0200 | 
wenzelm | 
pretty formatting as in Isabelle/ML;
 | 
file |
diff |
annotate
 | 
| Fri, 27 Mar 2020 22:01:27 +0100 | 
wenzelm | 
misc tuning based on hints by IntelliJ IDEA;
 | 
file |
diff |
annotate
 | 
| Wed, 15 Jan 2020 19:54:50 +0100 | 
wenzelm | 
misc tuning, following hint by IntelliJ;
 | 
file |
diff |
annotate
 | 
| Sun, 10 Mar 2019 21:12:29 +0100 | 
wenzelm | 
document markers are formal comments, and may thus occur anywhere in the command-span;
 | 
file |
diff |
annotate
 | 
| Sun, 10 Mar 2019 00:21:34 +0100 | 
wenzelm | 
added semantic document markers;
 | 
file |
diff |
annotate
 | 
| Fri, 21 Dec 2018 13:00:59 +0100 | 
wenzelm | 
more Haskell operations;
 | 
file |
diff |
annotate
 | 
| Tue, 11 Dec 2018 19:25:35 +0100 | 
wenzelm | 
more uniform multi-language operations;
 | 
file |
diff |
annotate
 | 
| Tue, 20 Nov 2018 13:44:06 +0100 | 
wenzelm | 
clarified presentation;
 | 
file |
diff |
annotate
 | 
| Tue, 16 Jan 2018 15:53:42 +0100 | 
wenzelm | 
tuned signature;
 | 
file |
diff |
annotate
 | 
| Mon, 15 Jan 2018 14:31:57 +0100 | 
wenzelm | 
clarified modules;
 | 
file |
diff |
annotate
 | 
| Sun, 14 Jan 2018 20:58:41 +0100 | 
wenzelm | 
trim blanks -- more thoroughly than in update_cartouches (for single-line comments);
 | 
file |
diff |
annotate
 | 
| Tue, 09 Jan 2018 17:40:25 +0100 | 
wenzelm | 
show only symbols with code;
 | 
file |
diff |
annotate
 | 
| Mon, 01 Jan 2018 21:17:28 +0100 | 
wenzelm | 
more completion templates;
 | 
file |
diff |
annotate
 | 
| Sat, 30 Dec 2017 20:04:05 +0100 | 
wenzelm | 
more robust treatment of conflicts with existing Unicode text;
 | 
file |
diff |
annotate
 | 
| Fri, 22 Dec 2017 15:49:44 +0100 | 
wenzelm | 
HTML rendering of \<^control> as in Isabelle/jEdit;
 | 
file |
diff |
annotate
 | 
| Mon, 04 Dec 2017 22:54:31 +0100 | 
wenzelm | 
tuned signature;
 | 
file |
diff |
annotate
 | 
| Mon, 04 Dec 2017 17:37:26 +0100 | 
wenzelm | 
font style for literal control symbols, notably for antiquotations;
 | 
file |
diff |
annotate
 | 
| Wed, 25 Oct 2017 14:54:28 +0200 | 
wenzelm | 
more explicit check;
 | 
file |
diff |
annotate
 | 
| Fri, 09 Jun 2017 16:59:14 +0200 | 
wenzelm | 
tuned signature;
 | 
file |
diff |
annotate
 | 
| Mon, 05 Jun 2017 13:19:14 +0200 | 
wenzelm | 
uniform notion of Symbol.is_controllable (see also 265d9300d523);
 | 
file |
diff |
annotate
 | 
| Thu, 01 Jun 2017 21:15:56 +0200 | 
wenzelm | 
output control symbols like ML version, with optionally hidden source;
 | 
file |
diff |
annotate
 | 
| Thu, 20 Apr 2017 11:33:36 +0200 | 
wenzelm | 
tuned whitespace;
 | 
file |
diff |
annotate
 | 
| Sat, 01 Apr 2017 19:17:15 +0200 | 
wenzelm | 
clarified YXML vs. symbol encoding: operate on whole message;
 | 
file |
diff |
annotate
 | 
| Mon, 20 Mar 2017 20:43:26 +0100 | 
wenzelm | 
support to encode/decode command state;
 | 
file |
diff |
annotate
 | 
| Sun, 12 Mar 2017 14:23:38 +0100 | 
wenzelm | 
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
 | 
file |
diff |
annotate
 | 
| Wed, 28 Dec 2016 17:10:09 +0100 | 
wenzelm | 
clarified modules;
 | 
file |
diff |
annotate
 | 
| Tue, 20 Dec 2016 16:08:02 +0100 | 
wenzelm | 
more systematic text length wrt. encoding;
 | 
file |
diff |
annotate
 | 
| Tue, 20 Dec 2016 10:44:36 +0100 | 
wenzelm | 
more systematic text length;
 | 
file |
diff |
annotate
 | 
| Tue, 20 Dec 2016 09:52:01 +0100 | 
wenzelm | 
tuned;
 | 
file |
diff |
annotate
 | 
| Thu, 10 Nov 2016 09:43:15 +0100 | 
wenzelm | 
tuned comment;
 | 
file |
diff |
annotate
 | 
| Thu, 22 Sep 2016 11:25:27 +0200 | 
wenzelm | 
discontinued raw symbols;
 | 
file |
diff |
annotate
 | 
| Wed, 20 Jul 2016 16:02:00 +0200 | 
wenzelm | 
completion templates for commands involving "begin ... end" blocks;
 | 
file |
diff |
annotate
 | 
| Sun, 06 Mar 2016 13:19:19 +0100 | 
wenzelm | 
clarified ML syntax for strings concerning UTF8;
 | 
file |
diff |
annotate
 | 
| Thu, 21 Jan 2016 22:16:48 +0100 | 
wenzelm | 
tuned message;
 | 
file |
diff |
annotate
 | 
| Fri, 08 Jan 2016 18:18:40 +0100 | 
wenzelm | 
clarified symbol insertion, depending on buffer encoding;
 | 
file |
diff |
annotate
 | 
| Fri, 08 Jan 2016 17:17:43 +0100 | 
wenzelm | 
tuned;
 | 
file |
diff |
annotate
 | 
| Tue, 29 Dec 2015 16:23:34 +0100 | 
wenzelm | 
tuned;
 | 
file |
diff |
annotate
 | 
| Sat, 19 Dec 2015 15:14:59 +0100 | 
wenzelm | 
tuned signature;
 | 
file |
diff |
annotate
 | 
| Thu, 05 Nov 2015 00:02:30 +0100 | 
wenzelm | 
symbolic syntax "\<comment> text";
 | 
file |
diff |
annotate
 |