Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. performance fine-tuning of hot spot;
  2. tuned;
  3. more efficient tokens_match_ord based on token_kind_index; tuned;
  4. more abstract type;
  5. tuned;
  6. clarified signature;
  7. clarified signature;
  8. explicit dummy token;
  9. clarified modules;
  10. clarified signature;
Changeset 67557:a965ccf7414e by wenzelm:
performance fine-tuning of hot spot;
The file was modified src/Pure/General/table.ML (diff)
Changeset 67556:5f86e2a9c59c by wenzelm:
tuned;
The file was modified src/Pure/Syntax/lexicon.ML (diff)
The file was modified src/Pure/Syntax/parser.ML (diff)
Changeset 67555:c550e38dd131 by wenzelm:
more efficient tokens_match_ord based on token_kind_index;<br>tuned;
The file was modified src/Pure/Syntax/lexicon.ML (diff)
Changeset 67554:c2151a6bfd57 by wenzelm:
more abstract type;
The file was modified src/Pure/Syntax/lexicon.ML (diff)
Changeset 67553:77d497947fc7 by wenzelm:
tuned;
The file was modified src/Pure/Syntax/simple_syntax.ML (diff)
Changeset 67552:679253fef277 by wenzelm:
clarified signature;
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)
Changeset 67551:4a087b9a29c5 by wenzelm:
clarified signature;
The file was modified src/Pure/Syntax/lexicon.ML (diff)
The file was modified src/Pure/Syntax/parser.ML (diff)
Changeset 67550:3b666615e3ce by wenzelm:
explicit dummy token;
The file was modified src/Pure/Syntax/lexicon.ML (diff)
The file was modified src/Pure/Syntax/parser.ML (diff)
Changeset 67549:7b399522d6c1 by wenzelm:
clarified modules;
The file was modified src/Pure/Syntax/lexicon.ML (diff)
The file was modified src/Pure/Syntax/parser.ML (diff)
Changeset 67548:c0f1667c1943 by wenzelm:
clarified signature;
The file was modified src/Pure/Syntax/lexicon.ML (diff)
The file was modified src/Pure/Syntax/simple_syntax.ML (diff)