Summary
- tuned;
- unused;
- tuned;
- simplified: prod_count is always NONE;
- tuned;
- tuned data structure and operations;
- tuned data structure and operations;
- tuned data structure and operations;
- more operations;
- prefer specific tokens_subtract: subtle change of comparison via tokens_match;
- tuned type: absorb NONE: token option as token_none: token;
- tuned;
- clarified types and operations: potentially more efficient add_prods; tuned data structure;
- clarified modules; tuned;
- tuned: more explicit types;
The file was modified | src/Pure/Syntax/parser.ML (diff) |
The file was modified | src/Pure/Syntax/parser.ML (diff) |
The file was modified | src/Pure/Syntax/parser.ML (diff) |
The file was modified | src/Pure/Syntax/parser.ML (diff) |
The file was modified | src/Pure/Syntax/parser.ML (diff) |
The file was modified | src/Pure/Syntax/parser.ML (diff) |
The file was modified | src/Pure/Syntax/lexicon.ML (diff) |
The file was modified | src/Pure/Syntax/parser.ML (diff) |
The file was modified | src/Pure/Syntax/parser.ML (diff) |
The file was modified | src/Pure/General/table.ML (diff) |
The file was modified | src/Pure/Syntax/parser.ML (diff) |
The file was modified | src/Pure/Syntax/parser.ML (diff) |
The file was modified | src/Pure/Syntax/parser.ML (diff) |
The file was modified | src/Pure/Syntax/parser.ML (diff) |
The file was modified | src/Pure/Syntax/lexicon.ML (diff) |
The file was modified | src/Pure/Syntax/parser.ML (diff) |
The file was modified | src/Pure/Syntax/parser.ML (diff) |