Summary
- include 'begin' and 'end' structure in text folds;
The file was modified | NEWS (diff) |
The file was modified | src/Pure/Isar/outer_syntax.scala (diff) |
The file was modified | NEWS (diff) |
The file was modified | src/Pure/Isar/outer_syntax.scala (diff) |