| Mon, 16 Dec 2024 12:55:39 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 15 Dec 2024 20:22:29 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 15 Dec 2024 20:12:45 +0100 |
wenzelm |
clarified signature (see also 2157039256d3);
|
file |
diff |
annotate
|
| Tue, 22 Oct 2024 12:03:46 +0200 |
wenzelm |
clarified markers for syntax consts: avoid overlap with logical consts;
|
file |
diff |
annotate
|
| Sun, 20 Oct 2024 13:41:56 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Sun, 29 Sep 2024 21:03:28 +0200 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Fri, 27 Sep 2024 22:14:40 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 27 Sep 2024 22:08:54 +0200 |
wenzelm |
minor performance tuning: proper table for parsetree list;
|
file |
diff |
annotate
|
| Thu, 26 Sep 2024 11:31:43 +0200 |
wenzelm |
clarified use of Lexicon.dummy;
|
file |
diff |
annotate
|
| Wed, 25 Sep 2024 12:59:43 +0200 |
wenzelm |
clarified persistent datatype: more direct literal_markup, which also serves as a flag;
|
file |
diff |
annotate
|
| Thu, 05 Sep 2024 17:39:45 +0200 |
wenzelm |
clarified signature: type ML_Pretty.pretty coincides with PolyML.pretty;
|
file |
diff |
annotate
|
| Fri, 14 Apr 2023 20:42:17 +0200 |
wenzelm |
more operations, following Isabelle/ML conventions;
|
file |
diff |
annotate
|
| Wed, 27 Jan 2021 14:56:40 +0100 |
wenzelm |
tuned signature (e.g. see HTML.control_block in Isabelle/Scala);
|
file |
diff |
annotate
|
| Tue, 19 Jan 2021 20:23:13 +0100 |
wenzelm |
suppress markup for literal tokens with block control symbols, for better PIDE/HTML output (see also d15fe10593ff);
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 11:01:05 +0200 |
wenzelm |
clarified signature;
|
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, 25 Nov 2018 18:45:10 +0100 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2018 14:33:30 +0100 |
wenzelm |
more comment markup;
|
file |
diff |
annotate
|
| Sun, 23 Sep 2018 19:59:53 +0200 |
wenzelm |
discontinued old-style inner comments;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 14:11:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 14:02:37 +0100 |
wenzelm |
more efficient tokens_match_ord based on token_kind_index;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:49:56 +0100 |
wenzelm |
more abstract type;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:40:26 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:26:50 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:23:53 +0100 |
wenzelm |
explicit dummy token;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:18:36 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:09:05 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 30 Jan 2018 18:38:18 +0100 |
wenzelm |
tuned data structure and operations;
|
file |
diff |
annotate
|
| Tue, 30 Jan 2018 11:48:38 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 28 Jan 2018 19:28:52 +0100 |
wenzelm |
clarified take/drop/chop prefix/suffix;
|
file |
diff |
annotate
|