# HG changeset patch
# User wenzelm
# Date 1406109214 -7200
# Node ID 416ce9617780ba740bf59fcce55c08ceaff739db
# Parent  4c6d44a3a0791bb2b7bd315cfd6e6b491981bde0
tuned;

diff -r 4c6d44a3a079 -r 416ce9617780 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Jul 23 11:22:56 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Jul 23 11:53:34 2014 +0200
@@ -82,9 +82,6 @@
 
   object Node
   {
-    val empty: Node = new Node()
-
-
     /* header and name */
 
     sealed case class Header(
@@ -177,6 +174,9 @@
     val empty_perspective_text: Perspective_Text =
       Perspective(false, Text.Perspective.empty, Overlays.empty)
 
+    val empty_perspective_command: Perspective_Command =
+      Perspective(false, Command.Perspective.empty, Overlays.empty)
+
 
     /* commands */
 
@@ -231,13 +231,14 @@
         else Iterator.empty
       }
     }
+
+    val empty: Node = new Node()
   }
 
   final class Node private(
     val get_blob: Option[Document.Blob] = None,
     val header: Node.Header = Node.bad_header("Bad theory header"),
-    val perspective: Node.Perspective_Command =
-      Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty),
+    val perspective: Node.Perspective_Command = Node.empty_perspective_command,
     _commands: Node.Commands = Node.Commands.empty)
   {
     def clear: Node = new Node(header = header)