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)