# HG changeset patch
# User wenzelm
# Date 1406102539 -7200
# Node ID 518e28a7c74b9ec135c73feb220187931406cfdb
# Parent  943dbbbf7ad5b089aab5810c5a7d7bb11ce96063
tuned signature;

diff -r 943dbbbf7ad5 -r 518e28a7c74b src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Jul 22 22:18:50 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Jul 23 10:02:19 2014 +0200
@@ -167,9 +167,16 @@
     case class Edits[A, B](edits: List[A]) extends Edit[A, B]
     case class Deps[A, B](header: Header) extends Edit[A, B]
     case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
+
+
+    /* perspective */
+
     type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
     type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
 
+    val empty_perspective_text: Perspective_Text =
+      Perspective(false, Text.Perspective.empty, Overlays.empty)
+
 
     /* commands */
 
diff -r 943dbbbf7ad5 -r 518e28a7c74b src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Jul 22 22:18:50 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Jul 23 10:02:19 2014 +0200
@@ -96,9 +96,6 @@
     }
   }
 
-  val empty_perspective: Document.Node.Perspective_Text =
-    Document.Node.Perspective(false, Text.Perspective.empty, Document.Node.Overlays.empty)
-
   def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
   {
     Swing_Thread.require {}
@@ -132,7 +129,7 @@
           Text.Perspective(document_view_ranges ::: load_ranges),
           PIDE.editor.node_overlays(node_name)))
     }
-    else (false, empty_perspective)
+    else (false, Document.Node.empty_perspective_text)
   }
 
 
@@ -191,7 +188,7 @@
   {
     private var pending_clear = false
     private val pending = new mutable.ListBuffer[Text.Edit]
-    private var last_perspective = empty_perspective
+    private var last_perspective = Document.Node.empty_perspective_text
 
     def is_pending(): Boolean = pending_clear || !pending.isEmpty
     def snapshot(): List[Text.Edit] = pending.toList