| Sat, 05 Oct 2024 22:46:21 +0200 | wenzelm | tuned; | file | diff | annotate |
| Mon, 30 Sep 2024 12:59:50 +0200 | wenzelm | clarify comparison of output: ignore token positions, which are somewhat accidental; | file | diff | annotate |
| Mon, 30 Sep 2024 10:50:33 +0200 | wenzelm | misc tuning; | file | diff | annotate |
| Mon, 30 Sep 2024 10:46:26 +0200 | wenzelm | clarified parse tree: always provide root node; | file | diff | annotate |
| Mon, 30 Sep 2024 10:44:25 +0200 | wenzelm | tuned signature; | file | diff | annotate |
| Sun, 29 Sep 2024 21:13:17 +0200 | wenzelm | more parse tree positions; | file | diff | annotate |
| Sun, 29 Sep 2024 19:51:23 +0200 | wenzelm | more accurate parse tree: retain all tokens (and thus positions); | file | diff | annotate |
| Sun, 29 Sep 2024 15:58:28 +0200 | wenzelm | clarified comparison: prefer authentic nonterminal context, instead of somewhat accidental "const"; | file | diff | annotate |
| Sun, 29 Sep 2024 15:24:17 +0200 | wenzelm | more detailed parse tree: retain nonterminal context as well; | file | diff | annotate |
| Sun, 29 Sep 2024 15:08:38 +0200 | wenzelm | clarified persistent data; | file | diff | annotate |
| Sun, 29 Sep 2024 15:00:20 +0200 | wenzelm | clarified input and output: support markup blocks via Bg/En; | file | diff | annotate |
| Sun, 29 Sep 2024 11:18:34 +0200 | wenzelm | clarified output: count Tip entries; | file | diff | annotate |
| Sun, 29 Sep 2024 11:08:43 +0200 | wenzelm | tuned signature; | file | diff | annotate |
| Sat, 28 Sep 2024 23:23:30 +0200 | wenzelm | tuned whitespace; | file | diff | annotate |
| Sat, 28 Sep 2024 21:16:01 +0200 | wenzelm | clarified signature: more explicit type "output"; | file | diff | annotate |
| Sat, 28 Sep 2024 20:28:11 +0200 | wenzelm | clarified signature; | file | diff | annotate |
| Sat, 28 Sep 2024 17:11:51 +0200 | wenzelm | tuned: more uniform; | file | diff | annotate |
| Sat, 28 Sep 2024 16:58:04 +0200 | wenzelm | tuned: more uniform; | file | diff | annotate |
| Sat, 28 Sep 2024 16:19:53 +0200 | wenzelm | tuned; | file | diff | annotate |
| Sat, 28 Sep 2024 16:11:30 +0200 | wenzelm | minor performance tuning; | file | diff | annotate |
| Sat, 28 Sep 2024 16:07:46 +0200 | wenzelm | tuned; | file | diff | annotate |
| Sat, 28 Sep 2024 15:58:09 +0200 | wenzelm | tuned; | file | diff | annotate |
| Sat, 28 Sep 2024 15:41:51 +0200 | wenzelm | minor performance tuning; | file | diff | annotate |
| Fri, 27 Sep 2024 22:44:30 +0200 | wenzelm | tuned signature; | file | diff | annotate |
| Fri, 27 Sep 2024 22:36:00 +0200 | wenzelm | tuned signature; | file | diff | annotate |
| Fri, 27 Sep 2024 22:28:46 +0200 | wenzelm | tuned signature; | 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 |
| Fri, 27 Sep 2024 20:29:38 +0200 | wenzelm | unused (see 954e9d6782ea); | file | diff | annotate |
| Fri, 27 Sep 2024 20:19:38 +0200 | wenzelm | tuned; | file | diff | annotate |
| Fri, 27 Sep 2024 20:12:48 +0200 | wenzelm | unused (see 7c1e73540990); | file | diff | annotate |
| Fri, 27 Sep 2024 20:09:54 +0200 | wenzelm | minor performance tuning (NB: order of prods / states does not matter); | file | diff | annotate |
| Fri, 27 Sep 2024 18:46:58 +0200 | wenzelm | tuned; | file | diff | annotate |
| Fri, 27 Sep 2024 16:52:43 +0200 | wenzelm | tuned; | file | diff | annotate |
| Fri, 27 Sep 2024 13:52:16 +0200 | wenzelm | tuned; | file | diff | annotate |
| Fri, 27 Sep 2024 12:52:55 +0200 | wenzelm | pro-forma support for markup blocks, without any change of result yet; | file | diff | annotate |
| Fri, 27 Sep 2024 11:14:38 +0200 | wenzelm | tuned; | file | diff | annotate |
| Thu, 26 Sep 2024 11:41:51 +0200 | wenzelm | tuned, following make_symbs in src/Pure/Syntax/printer.ML; | file | diff | annotate |
| Thu, 26 Sep 2024 11:31:43 +0200 | wenzelm | clarified use of Lexicon.dummy; | file | diff | annotate |
| Thu, 26 Sep 2024 11:01:41 +0200 | wenzelm | unused (see 584828fa7a97); | file | diff | annotate |
| Thu, 26 Sep 2024 00:06:00 +0200 | wenzelm | tuned; | file | diff | annotate |
| Wed, 25 Sep 2024 23:34:31 +0200 | wenzelm | tuned: prefer ML over prose; | file | diff | annotate |
| Wed, 25 Sep 2024 17:45:15 +0200 | wenzelm | eliminated redundant nt_count: rely on Symtab.size; | file | diff | annotate |
| Wed, 25 Sep 2024 15:06:12 +0200 | wenzelm | eliminate unused prod_count (see also 7afca3218b65); | file | diff | annotate |
| Wed, 25 Sep 2024 14:45:19 +0200 | wenzelm | tuned; | file | diff | annotate |
| Wed, 25 Sep 2024 10:38:46 +0200 | wenzelm | clarified signature; | file | diff | annotate |
| Tue, 24 Sep 2024 21:41:01 +0200 | wenzelm | tuned; | file | diff | annotate |
| Tue, 24 Sep 2024 21:31:20 +0200 | wenzelm | tuned; | file | diff | annotate |
| Tue, 24 Sep 2024 21:24:44 +0200 | wenzelm | tuned; | file | diff | annotate |
| Tue, 24 Sep 2024 20:10:11 +0200 | wenzelm | tuned; | file | diff | annotate |
| Tue, 24 Sep 2024 19:58:24 +0200 | wenzelm | tuned; | file | diff | annotate |
| Mon, 23 Sep 2024 15:01:10 +0200 | wenzelm | misc tuning and clarification; | file | diff | annotate |
| Mon, 23 Sep 2024 12:59:10 +0200 | wenzelm | tuned; | file | diff | annotate |
| Mon, 23 Sep 2024 11:36:03 +0200 | wenzelm | minor performance tuning: more concise tuples; | file | diff | annotate |
| Mon, 23 Sep 2024 11:08:30 +0200 | wenzelm | tuned; | file | diff | annotate |
| Mon, 23 Sep 2024 10:56:25 +0200 | wenzelm | tuned; | file | diff | annotate |
| Mon, 23 Sep 2024 10:45:05 +0200 | wenzelm | tuned; | file | diff | annotate |
| Wed, 29 Nov 2023 15:29:54 +0100 | wenzelm | more compact representation; | file | diff | annotate |
| Tue, 09 May 2023 21:32:03 +0200 | wenzelm | performance tuning: cached non-persistent Parser.gram reduces heap size by approx. 1-4%; | file | diff | annotate |
| Tue, 09 May 2023 19:56:31 +0200 | wenzelm | tuned: more readable ML; | file | diff | annotate |