Summary
- performance fine-tuning of hot spot;
- tuned;
- more efficient tokens_match_ord based on token_kind_index; tuned;
- more abstract type;
- tuned;
- clarified signature;
- clarified signature;
- explicit dummy token;
- clarified modules;
- clarified signature;
The file was modified | src/Pure/General/table.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/lexicon.ML (diff) |
The file was modified | src/Pure/Syntax/lexicon.ML (diff) |
The file was modified | src/Pure/Syntax/simple_syntax.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/simple_syntax.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/lexicon.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/lexicon.ML (diff) |
The file was modified | src/Pure/Syntax/simple_syntax.ML (diff) |