Summary
- clarified menu actions;
- purge history more thoroughly (see also 3156faac30a7);
The file was modified | NEWS (diff) |
The file was modified | src/Doc/JEdit/JEdit.thy (diff) |
The file was modified | src/Tools/jEdit/src/Isabelle.props (diff) |
The file was modified | src/Tools/jEdit/src/jEdit.props (diff) |
The file was modified | src/Pure/PIDE/document.scala (diff) |