simplified Text.Chunk -- eliminated ooddities;
afford strict symbol_index, which is usually empty anyway;

--- a/src/Pure/General/position.scala	Tue Apr 08 20:00:53 2014 +0200
+++ b/src/Pure/General/position.scala	Tue Apr 08 20:03:00 2014 +0200
@@ -88,7 +88,7 @@
         case (Id(id), Range(range)) =>
           val chunk_name =
             pos match {
-              case File(name) => Text.Chunk.File_Name(name)
+              case File(name) => Text.Chunk.File(name)
               case _ => Text.Chunk.Default
             }
           Some((id, chunk_name, range))

--- a/src/Pure/PIDE/command.scala	Tue Apr 08 20:00:53 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Apr 08 20:03:00 2014 +0200
@@ -15,7 +15,7 @@
 object Command
 {
   type Edit = (Option[Command], Option[Command])
-  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Text.Chunk.File)])]
+  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Text.Chunk)])]
 
 
 
@@ -355,25 +355,21 @@
 
   /* source chunks */
 
+  val chunk: Text.Chunk = Text.Chunk(source)
+
+  val chunks: Map[Text.Chunk.Name, Text.Chunk] =
+    ((Text.Chunk.Default -> chunk) ::
+      (for (Exn.Res((name, Some((_, file)))) <- blobs)
+        yield (Text.Chunk.File(name.node) -> file))).toMap
+
   def length: Int = source.length
-  val range: Text.Range = Text.Range(0, length)
+  def range: Text.Range = chunk.range
 
   val proper_range: Text.Range =
     Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
 
   def source(range: Text.Range): String = source.substring(range.start, range.stop)
 
-  val chunk: Text.Chunk =
-    new Text.Chunk {
-      def range: Text.Range = Command.this.range
-      lazy val symbol_index = Symbol.Index(source)
-    }
-
-  val chunks: Map[Text.Chunk.Name, Text.Chunk] =
-    ((Text.Chunk.Default -> chunk) ::
-      (for (Exn.Res((name, Some((_, file)))) <- blobs)
-        yield (Text.Chunk.File_Name(name.node) -> file))).toMap
-
 
   /* accumulated results */
 

--- a/src/Pure/PIDE/document.scala	Tue Apr 08 20:00:53 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Apr 08 20:03:00 2014 +0200
@@ -45,7 +45,7 @@
 
   /* document blobs: auxiliary files */
 
-  sealed case class Blob(bytes: Bytes, file: Text.Chunk.File, changed: Boolean)
+  sealed case class Blob(bytes: Bytes, chunk: Text.Chunk, changed: Boolean)
   {
     def unchanged: Blob = copy(changed = false)
   }
@@ -774,7 +774,7 @@
           val former_range = revert(range)
           val (chunk_name, command_iterator) =
             load_commands match {
-              case command :: _ => (Text.Chunk.File_Name(node_name.node), Iterator((command, 0)))
+              case command :: _ => (Text.Chunk.File(node_name.node), Iterator((command, 0)))
               case _ => (Text.Chunk.Default, node.command_iterator(former_range))
             }
           val markup_index = Command.Markup_Index(status, chunk_name)

--- a/src/Pure/PIDE/text.scala	Tue Apr 08 20:00:53 2014 +0200
+++ b/src/Pure/PIDE/text.scala	Tue Apr 08 20:03:00 2014 +0200
@@ -71,19 +71,25 @@
   }
 
 
-  /* chunks with symbol index */
+  /* named chunks with sparse symbol index */
 
-  abstract class Chunk
+  object Chunk
   {
-    def range: Range
-    def symbol_index: Symbol.Index
+    sealed abstract class Name
+    case object Default extends Name
+    case class Id(id: Document_ID.Generic) extends Name
+    case class File(name: String) extends Name
 
-    private lazy val hash: Int = (range, symbol_index).hashCode
-    override def hashCode: Int = hash
+    def apply(text: CharSequence): Chunk =
+      new Chunk(Range(0, text.length), Symbol.Index(text))
+  }
+
+  final class Chunk private(val range: Range, private val symbol_index: Symbol.Index)
+  {
+    override def hashCode: Int = (range, symbol_index).hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Chunk =>
-          hash == other.hash &&
           range == other.range &&
           symbol_index == other.symbol_index
         case _ => false
@@ -102,20 +108,6 @@
     }
   }
 
-  object Chunk
-  {
-    sealed abstract class Name
-    case object Default extends Name
-    case class Id(id: Document_ID.Generic) extends Name
-    case class File_Name(file_name: String) extends Name
-
-    class File(text: CharSequence) extends Chunk
-    {
-      val range = Range(0, text.length)
-      val symbol_index = Symbol.Index(text)
-    }
-  }
-
 
   /* perspective */
 

--- a/src/Pure/Thy/thy_syntax.scala	Tue Apr 08 20:00:53 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Apr 08 20:03:00 2014 +0200
@@ -271,7 +271,7 @@
       Exn.capture {
         val name =
           Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
-        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.file)))
+        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
         (name, blob)
       })
   }

--- a/src/Tools/jEdit/src/document_model.scala	Tue Apr 08 20:00:53 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Apr 08 20:03:00 2014 +0200
@@ -138,7 +138,7 @@
 
   /* blob */
 
-  private var _blob: Option[(Bytes, Text.Chunk.File)] = None  // owned by Swing thread
+  private var _blob: Option[(Bytes, Text.Chunk)] = None  // owned by Swing thread
 
   private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
 
@@ -146,17 +146,17 @@
     Swing_Thread.require {
       if (is_theory) None
       else {
-        val (bytes, file) =
+        val (bytes, chunk) =
           _blob match {
             case Some(x) => x
             case None =>
               val bytes = PIDE.resources.file_content(buffer)
-              val file = new Text.Chunk.File(buffer.getSegment(0, buffer.getLength))
-              _blob = Some((bytes, file))
-              (bytes, file)
+              val chunk = Text.Chunk(buffer.getSegment(0, buffer.getLength))
+              _blob = Some((bytes, chunk))
+              (bytes, chunk)
           }
         val changed = pending_edits.is_pending()
-        Some(Document.Blob(bytes, file, changed))
+        Some(Document.Blob(bytes, chunk, changed))
       }
     }