src/Tools/jEdit/src/jedit_resources.scala
changeset 64797 891a25a87ea1
parent 63022 785a59235a15
child 64813 7283f41d05ab
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Jan 05 09:55:26 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Jan 05 10:10:51 2017 +0100
     1.3 @@ -111,9 +111,6 @@
     1.4  
     1.5    /* theory text edits */
     1.6  
     1.7 -  def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
     1.8 -    nodes.undefined_blobs(node => !loaded_theories(node.theory))
     1.9 -
    1.10    override def commit(change: Session.Change)
    1.11    {
    1.12      if (change.syntax_changed.nonEmpty)