src/Pure/PIDE/document.scala
changeset 44474 681447a9ffe5
parent 44446 f9334afb6945
child 44475 709e1d671483
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Aug 25 11:27:37 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Aug 25 11:41:48 2011 +0200
     1.3 @@ -60,7 +60,8 @@
     1.4          case exn => exn
     1.5        }
     1.6  
     1.7 -    val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Nil, Map(), Linear_Set())
     1.8 +    val empty: Node =
     1.9 +      Node(Exn.Exn(ERROR("Bad theory header")), Command.Perspective.empty, Map(), Linear_Set())
    1.10  
    1.11      def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
    1.12        : Iterator[(Command, Text.Offset)] =