src/Pure/PIDE/document.scala
changeset 56335 8953d4cc060a
parent 56314 9a513737a0b2
child 56336 60434514ec0a
     1.1 --- a/src/Pure/PIDE/document.scala	Mon Mar 31 12:35:39 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Mon Mar 31 15:05:24 2014 +0200
     1.3 @@ -46,20 +46,25 @@
     1.4    /* document blobs: auxiliary files */
     1.5  
     1.6    sealed case class Blob(bytes: Bytes, file: Command.File, changed: Boolean)
     1.7 +  {
     1.8 +    def unchanged: Blob = copy(changed = false)
     1.9 +  }
    1.10  
    1.11    object Blobs
    1.12    {
    1.13 -    def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs)
    1.14 +    def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs, Nodes.empty)
    1.15      val empty: Blobs = apply(Map.empty)
    1.16    }
    1.17  
    1.18 -  final class Blobs private(blobs: Map[Node.Name, Blob])
    1.19 +  final class Blobs private(blobs: Map[Node.Name, Blob], default_nodes: Nodes)
    1.20    {
    1.21      private lazy val digests: Map[SHA1.Digest, Blob] =
    1.22        for ((_, blob) <- blobs) yield (blob.bytes.sha1_digest, blob)
    1.23  
    1.24      def get(digest: SHA1.Digest): Option[Blob] = digests.get(digest)
    1.25 -    def get(name: Node.Name): Option[Blob] = blobs.get(name)
    1.26 +
    1.27 +    def get(name: Node.Name): Option[Blob] =
    1.28 +      blobs.get(name) orElse default_nodes(name).get_blob
    1.29  
    1.30      def changed(name: Node.Name): Boolean =
    1.31        get(name) match {
    1.32 @@ -67,6 +72,8 @@
    1.33          case None => false
    1.34        }
    1.35  
    1.36 +    def default(nodes: Nodes): Blobs = new Blobs(blobs, nodes)
    1.37 +
    1.38      override def toString: String = blobs.mkString("Blobs(", ",", ")")
    1.39    }
    1.40  
    1.41 @@ -157,7 +164,7 @@
    1.42        }
    1.43      }
    1.44      case class Clear[A, B]() extends Edit[A, B]
    1.45 -    case class Blob[A, B]() extends Edit[A, B]
    1.46 +    case class Blob[A, B](blob: Document.Blob) extends Edit[A, B]
    1.47  
    1.48      case class Edits[A, B](edits: List[A]) extends Edit[A, B]
    1.49      case class Deps[A, B](header: Header) extends Edit[A, B]
    1.50 @@ -222,7 +229,7 @@
    1.51    }
    1.52  
    1.53    final class Node private(
    1.54 -    val is_blob: Boolean = false,
    1.55 +    val get_blob: Option[Document.Blob] = None,
    1.56      val header: Node.Header = Node.bad_header("Bad theory header"),
    1.57      val perspective: Node.Perspective_Command =
    1.58        Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty),
    1.59 @@ -230,13 +237,13 @@
    1.60    {
    1.61      def clear: Node = new Node(header = header)
    1.62  
    1.63 -    def init_blob: Node = new Node(is_blob = true)
    1.64 +    def init_blob(blob: Document.Blob): Node = new Node(Some(blob.unchanged))
    1.65  
    1.66      def update_header(new_header: Node.Header): Node =
    1.67 -      new Node(is_blob, new_header, perspective, _commands)
    1.68 +      new Node(get_blob, new_header, perspective, _commands)
    1.69  
    1.70      def update_perspective(new_perspective: Node.Perspective_Command): Node =
    1.71 -      new Node(is_blob, header, new_perspective, _commands)
    1.72 +      new Node(get_blob, header, new_perspective, _commands)
    1.73  
    1.74      def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
    1.75        perspective.required == other_perspective.required &&
    1.76 @@ -248,7 +255,7 @@
    1.77  
    1.78      def update_commands(new_commands: Linear_Set[Command]): Node =
    1.79        if (new_commands eq _commands.commands) this
    1.80 -      else new Node(is_blob, header, perspective, Node.Commands(new_commands))
    1.81 +      else new Node(get_blob, header, perspective, Node.Commands(new_commands))
    1.82  
    1.83      def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
    1.84        _commands.range(i)