equal
deleted
inserted
replaced
1 /* Title: Tools/jEdit/src/fold_handler.scala |
1 /* Title: Tools/jEdit/src/fold_handling.scala |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Handling of folds within the text structure. |
4 Handling of folds within the text structure. |
5 */ |
5 */ |
6 |
6 |