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