src/Pure/PIDE/command.scala
changeset 56473 5b5c750e9763
parent 56470 8eda56033203
child 56475 710dee42b3d0
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Apr 08 20:00:53 2014 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Apr 08 20:03:00 2014 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  object Command
     1.5  {
     1.6    type Edit = (Option[Command], Option[Command])
     1.7 -  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Text.Chunk.File)])]
     1.8 +  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Text.Chunk)])]
     1.9  
    1.10  
    1.11  
    1.12 @@ -355,25 +355,21 @@
    1.13  
    1.14    /* source chunks */
    1.15  
    1.16 +  val chunk: Text.Chunk = Text.Chunk(source)
    1.17 +
    1.18 +  val chunks: Map[Text.Chunk.Name, Text.Chunk] =
    1.19 +    ((Text.Chunk.Default -> chunk) ::
    1.20 +      (for (Exn.Res((name, Some((_, file)))) <- blobs)
    1.21 +        yield (Text.Chunk.File(name.node) -> file))).toMap
    1.22 +
    1.23    def length: Int = source.length
    1.24 -  val range: Text.Range = Text.Range(0, length)
    1.25 +  def range: Text.Range = chunk.range
    1.26  
    1.27    val proper_range: Text.Range =
    1.28      Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
    1.29  
    1.30    def source(range: Text.Range): String = source.substring(range.start, range.stop)
    1.31  
    1.32 -  val chunk: Text.Chunk =
    1.33 -    new Text.Chunk {
    1.34 -      def range: Text.Range = Command.this.range
    1.35 -      lazy val symbol_index = Symbol.Index(source)
    1.36 -    }
    1.37 -
    1.38 -  val chunks: Map[Text.Chunk.Name, Text.Chunk] =
    1.39 -    ((Text.Chunk.Default -> chunk) ::
    1.40 -      (for (Exn.Res((name, Some((_, file)))) <- blobs)
    1.41 -        yield (Text.Chunk.File_Name(name.node) -> file))).toMap
    1.42 -
    1.43  
    1.44    /* accumulated results */
    1.45