Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. proper Font_Subst.cache for paintScreenLineRange;
  2. more predictable result, avoid slightly odd "lastSubstFont" by jEdit;
  3. tuned;
  4. tuned signature;
  5. tuned;
Changeset 73884:0a12ca4f3e8d by wenzelm:
proper Font_Subst.cache for paintScreenLineRange;
The file was modified src/Tools/jEdit/src/rich_text_area.scala (diff)
Changeset 73883:994c9dacd2f9 by wenzelm:
more predictable result, avoid slightly odd "lastSubstFont" by jEdit;
The file was modified src/Tools/jEdit/src/rich_text_area.scala (diff)
Changeset 73882:01efb7cbf365 by wenzelm:
tuned;
The file was modified src/Tools/jEdit/src/token_markup.scala (diff)
Changeset 73881:b1272ec71568 by wenzelm:
tuned signature;
The file was modified src/Tools/jEdit/src/rich_text_area.scala (diff)
Changeset 73880:9ce206f6e8c6 by wenzelm:
tuned;
The file was modified src/Tools/jEdit/src/rich_text_area.scala (diff)