# HG changeset patch
# User wenzelm
# Date 1396966022 -7200
# Node ID ffc94a2716335b2462ed1ee519a8c32b7647d463
# Parent  30128d1acfbc2be2818db05054b76836e4661eff
avoid data redundancy;

diff -r 30128d1acfbc -r ffc94a271633 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Apr 08 15:12:54 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Apr 08 16:07:02 2014 +0200
@@ -197,8 +197,8 @@
               var st = copy(results = results + (i -> message1))
               if (Protocol.is_inlined(message)) {
                 for {
-                  (chunk_name, chunk) <- command.chunks
-                  range <- Protocol.message_positions(valid_id, chunk, message)
+                  (chunk_name, chunk) <- command.chunks.iterator
+                  range <- Protocol.message_positions(valid_id, chunk_name, chunk, message)
                 } st = st.add_markup(false, chunk_name, Text.Info(range, message2))
               }
               st
@@ -342,7 +342,6 @@
 
   val chunk: Text.Chunk =
     new Text.Chunk {
-      def name: Text.Chunk.Name = Text.Chunk.Default
       def range: Text.Range = Command.this.range
       lazy val symbol_index = Symbol.Index(source)
     }
diff -r 30128d1acfbc -r ffc94a271633 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Apr 08 15:12:54 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Apr 08 16:07:02 2014 +0200
@@ -302,13 +302,14 @@
 
   def message_positions(
     valid_id: Document_ID.Generic => Boolean,
+    chunk_name: Text.Chunk.Name,
     chunk: Text.Chunk,
     message: XML.Elem): Set[Text.Range] =
   {
     def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
       props match {
-        case Position.Reported(id, chunk_name, symbol_range)
-        if valid_id(id) && chunk_name == chunk.name =>
+        case Position.Reported(id, name, symbol_range)
+        if valid_id(id) && name == chunk_name =>
           chunk.incorporate(symbol_range) match {
             case Some(range) => set + range
             case _ => set
diff -r 30128d1acfbc -r ffc94a271633 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Tue Apr 08 15:12:54 2014 +0200
+++ b/src/Pure/PIDE/text.scala	Tue Apr 08 16:07:02 2014 +0200
@@ -71,26 +71,23 @@
   }
 
 
-  /* named chunks */
+  /* chunks with symbol index */
 
   abstract class Chunk
   {
-    def name: Chunk.Name
     def range: Range
     def symbol_index: Symbol.Index
 
-    private lazy val hash: Int = (name, range, symbol_index).hashCode
+    private lazy val hash: Int = (range, symbol_index).hashCode
     override def hashCode: Int = hash
     override def equals(that: Any): Boolean =
       that match {
         case other: Chunk =>
           hash == other.hash &&
-          name == other.name &&
           range == other.range &&
           symbol_index == other.symbol_index
         case _ => false
       }
-    override def toString: String = "Text.Chunk(" + name + ")"
 
     def decode(symbol_offset: Symbol.Offset): Offset = symbol_index.decode(symbol_offset)
     def decode(symbol_range: Symbol.Range): Range = symbol_index.decode(symbol_range)
@@ -111,9 +108,8 @@
     case object Default extends Name
     case class File_Name(file_name: String) extends Name
 
-    class File(file_name: String, text: CharSequence) extends Chunk
+    class File(text: CharSequence) extends Chunk
     {
-      val name = File_Name(file_name)
       val range = Range(0, text.length)
       val symbol_index = Symbol.Index(text)
     }
diff -r 30128d1acfbc -r ffc94a271633 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Apr 08 15:12:54 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Apr 08 16:07:02 2014 +0200
@@ -151,7 +151,7 @@
             case Some(x) => x
             case None =>
               val bytes = PIDE.resources.file_content(buffer)
-              val file = new Text.Chunk.File(node_name.node, buffer.getSegment(0, buffer.getLength))
+              val file = new Text.Chunk.File(buffer.getSegment(0, buffer.getLength))
               _blob = Some((bytes, file))
               (bytes, file)
           }