Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. NEWS;
  3. handle font-size events;
  4. clarified GUI representation of replacement texts with zero or more abbrevs;
  5. handle update events; tuned;
  6. discontinued global etc/abbrevs;
  7. added abbrevs panel;
  8. tuned;
  9. more robust;
  10. maintain abbrevs in canonical reverse order;
  11. tuned;
  12. tuned;
  13. ignore default output directory of 'build_stats' tool
Changeset 63876:fd73c5dbaad2 by wenzelm:
merged
Changeset 63875:2683c3be36eb by wenzelm:
NEWS;
The file was modified NEWS (diff)
Changeset 63874:e2393cfde472 by wenzelm:
handle font-size events;
The file was modified src/Pure/GUI/gui.scala (diff)
The file was modified src/Tools/jEdit/src/symbols_dockable.scala (diff)
Changeset 63873:228a85f1d6af by wenzelm:
clarified GUI representation of replacement texts with zero or more abbrevs;
The file was modified src/Pure/General/completion.scala (diff)
The file was modified src/Tools/jEdit/src/symbols_dockable.scala (diff)
Changeset 63872:7dd5297d87fa by wenzelm:
handle update events;<br>tuned;
The file was modified src/Tools/jEdit/src/symbols_dockable.scala (diff)
Changeset 63871:f745c6e683b7 by wenzelm:
discontinued global etc/abbrevs;
The file was modified NEWS (diff)
The file was modified etc/settings (diff)
The file was modified src/Doc/JEdit/JEdit.thy (diff)
The file was modified src/Pure/General/completion.scala (diff)
The file was modified src/Pure/Pure.thy (diff)
The file was removedetc/abbrevs
Changeset 63870:6db1aac936db by wenzelm:
added abbrevs panel;
The file was modified src/Tools/jEdit/src/symbols_dockable.scala (diff)
Changeset 63869:856d2f74c303 by wenzelm:
tuned;
The file was modified src/Pure/General/completion.scala (diff)
Changeset 63868:22037a819276 by wenzelm:
more robust;
The file was modified src/Tools/jEdit/src/isabelle.scala (diff)
Changeset 63867:fb46c031c841 by wenzelm:
maintain abbrevs in canonical reverse order;
The file was modified src/Pure/Isar/outer_syntax.scala (diff)
The file was modified src/Pure/library.scala (diff)
Changeset 63866:630eaf8fe9f3 by wenzelm:
tuned;
The file was modified src/Pure/General/path.scala (diff)
The file was modified src/Pure/Thy/thy_syntax.scala (diff)
Changeset 63865:ccac33e291b1 by wenzelm:
tuned;
The file was modified src/Pure/Isar/outer_syntax.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Tools/jEdit/src/isabelle.scala (diff)
Changeset 63864:159882dbb339 by lars hupel _lars.hupel@mytum.de_:
ignore default output directory of &#039;build_stats&#039; tool
The file was modified .hgignore (diff)