--- a/src/Tools/jEdit/src/document_model.scala Fri Sep 29 17:28:44 2017 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Fri Sep 29 17:35:09 2017 +0200
@@ -253,7 +253,7 @@
val pending_nodes = for ((node_name, None) <- purged) yield node_name
(open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
}
- val retain = PIDE.resources.thy_info.dependencies(imports).entries.map(_.name).toSet
+ val retain = PIDE.resources.thy_info.dependencies(imports).names.toSet
for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
yield edit