Summary
- merged
- reactivated other_id reports (see also db929027e701, 8eda56033203);
- invisible context similar to interpretation;
- avoid massive multiplication of reports due to interpretation;
- tuned comments;
- more thorough update;
The file was modified | NEWS (diff) |
The file was modified | src/Pure/PIDE/document.scala (diff) |
The file was modified | src/Pure/Isar/bundle.ML (diff) |
The file was modified | src/Pure/Isar/locale.ML (diff) |
The file was modified | src/Pure/context_position.ML (diff) |
The file was modified | src/Pure/Isar/locale.ML (diff) |
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) |