src/Tools/jEdit/src/jedit_editor.scala
changeset 57615 df1b3452d71c
parent 57612 990ffb84489b
child 57873 ea94d2aa62be
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Jul 23 11:53:34 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Jul 23 13:01:30 2014 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4      val removed = removed_nodes; removed_nodes = Set.empty
     1.5      val removed_perspective =
     1.6        (removed -- models.iterator.map(_.node_name)).toList.map(
     1.7 -        name => (name, Document.Node.empty_perspective_text))
     1.8 +        name => (name, Document.Node.no_perspective_text))
     1.9  
    1.10      val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective
    1.11      if (!edits.isEmpty) session.update(doc_blobs, edits)