src/Pure/Syntax/parser.ML
Mon, 30 Sep 2024 10:46:26 +0200 wenzelm clarified parse tree: always provide root node;
Mon, 30 Sep 2024 10:44:25 +0200 wenzelm tuned signature;
Sun, 29 Sep 2024 21:13:17 +0200 wenzelm more parse tree positions;
Sun, 29 Sep 2024 19:51:23 +0200 wenzelm more accurate parse tree: retain all tokens (and thus positions);
Sun, 29 Sep 2024 15:58:28 +0200 wenzelm clarified comparison: prefer authentic nonterminal context, instead of somewhat accidental "const";
Sun, 29 Sep 2024 15:24:17 +0200 wenzelm more detailed parse tree: retain nonterminal context as well;
less more (0) -100 -30 -10 -6 tip