# HG changeset patch # User wenzelm # Date 1521834346 -3600 # Node ID 5b063691061861195126b897b62da1b8a99d3802 # Parent 604da273e18d076bc87a33d45ca8046fd6f4bcde tuned; diff -r 604da273e18d -r 5b0636910618 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Fri Mar 23 17:09:36 2018 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Fri Mar 23 20:45:46 2018 +0100 @@ -255,7 +255,7 @@ } val retain = PIDE.resources.dependencies(imports).theories.toSet - for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits) + for ((node_name, Some(edits)) <- purged if !retain(node_name); edit <- edits) yield edit } else Nil