1.1 --- a/src/Pure/PIDE/document.scala	Wed Jul 23 11:22:56 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Jul 23 11:53:34 2014 +0200
     1.3 @@ -82,9 +82,6 @@
     1.4  
     1.5    object Node
     1.6    {
     1.7 -    val empty: Node = new Node()
     1.8 -
     1.9 -
    1.10      /* header and name */
    1.11  
    1.12      sealed case class Header(
    1.13 @@ -177,6 +174,9 @@
    1.14      val empty_perspective_text: Perspective_Text =
    1.15        Perspective(false, Text.Perspective.empty, Overlays.empty)
    1.16  
    1.17 +    val empty_perspective_command: Perspective_Command =
    1.18 +      Perspective(false, Command.Perspective.empty, Overlays.empty)
    1.19 +
    1.20  
    1.21      /* commands */
    1.22  
    1.23 @@ -231,13 +231,14 @@
    1.24          else Iterator.empty
    1.25        }
    1.26      }
    1.27 +
    1.28 +    val empty: Node = new Node()
    1.29    }
    1.30  
    1.31    final class Node private(
    1.32      val get_blob: Option[Document.Blob] = None,
    1.33      val header: Node.Header = Node.bad_header("Bad theory header"),
    1.34 -    val perspective: Node.Perspective_Command =
    1.35 -      Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty),
    1.36 +    val perspective: Node.Perspective_Command = Node.empty_perspective_command,
    1.37      _commands: Node.Commands = Node.Commands.empty)
    1.38    {
    1.39      def clear: Node = new Node(header = header)