src/Pure/PIDE/document.scala
changeset 49678 954d1c94f55f
parent 49645 5a0817ec0314
child 50204 daeb1674fb91
     1.1 --- a/src/Pure/PIDE/document.scala	Mon Oct 01 20:17:30 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Mon Oct 01 20:35:09 2012 +0200
     1.3 @@ -110,22 +110,18 @@
     1.4    final class Node private(
     1.5      val header: Node.Header = Node.bad_header("Bad theory header"),
     1.6      val perspective: Command.Perspective = Command.Perspective.empty,
     1.7 -    val blobs: Map[String, Blob] = Map.empty,
     1.8      val commands: Linear_Set[Command] = Linear_Set.empty)
     1.9    {
    1.10      def clear: Node = new Node(header = header)
    1.11  
    1.12      def update_header(new_header: Node.Header): Node =
    1.13 -      new Node(new_header, perspective, blobs, commands)
    1.14 +      new Node(new_header, perspective, commands)
    1.15  
    1.16      def update_perspective(new_perspective: Command.Perspective): Node =
    1.17 -      new Node(header, new_perspective, blobs, commands)
    1.18 -
    1.19 -    def update_blobs(new_blobs: Map[String, Blob]): Node =
    1.20 -      new Node(header, perspective, new_blobs, commands)
    1.21 +      new Node(header, new_perspective, commands)
    1.22  
    1.23      def update_commands(new_commands: Linear_Set[Command]): Node =
    1.24 -      new Node(header, perspective, blobs, new_commands)
    1.25 +      new Node(header, perspective, new_commands)
    1.26  
    1.27  
    1.28      /* commands */