tuned;
authorwenzelm
Fri Mar 23 20:45:46 2018 +0100 (14 months ago)
changeset 679345b0636910618
parent 67933 604da273e18d
child 67935 61888dd27f73
tuned;
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Fri Mar 23 17:09:36 2018 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Fri Mar 23 20:45:46 2018 +0100
     1.3 @@ -255,7 +255,7 @@
     1.4              }
     1.5              val retain = PIDE.resources.dependencies(imports).theories.toSet
     1.6  
     1.7 -            for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
     1.8 +            for ((node_name, Some(edits)) <- purged if !retain(node_name); edit <- edits)
     1.9                yield edit
    1.10            }
    1.11            else Nil