Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. reactivated other_id reports (see also db929027e701, 8eda56033203);
  3. invisible context similar to interpretation;
  4. avoid massive multiplication of reports due to interpretation;
  5. tuned comments;
  6. more thorough update;
Changeset 63033:b07c9f5d3802 by wenzelm:
merged
Changeset 63032:e0fa59bbc956 by wenzelm:
reactivated other_id reports (see also db929027e701, 8eda56033203);
The file was modified NEWS (diff)
The file was modified src/Pure/PIDE/document.scala (diff)
Changeset 63031:c4d2945c4900 by wenzelm:
invisible context similar to interpretation;
The file was modified src/Pure/Isar/bundle.ML (diff)
Changeset 63030:4e7eff53bee7 by wenzelm:
avoid massive multiplication of reports due to interpretation;
The file was modified src/Pure/Isar/locale.ML (diff)
The file was modified src/Pure/context_position.ML (diff)
Changeset 63029:8b830d2bf94c by wenzelm:
tuned comments;
The file was modified src/Pure/Isar/locale.ML (diff)
Changeset 63028:5fb352275db3 by wenzelm:
more thorough update;
The file was modified src/Tools/jEdit/src/document_view.scala (diff)
The file was modified src/Tools/jEdit/src/pretty_text_area.scala (diff)
The file was modified src/Tools/jEdit/src/rich_text_area.scala (diff)