diff -r 3749d1e6dde9 -r 518e44a0ee15 src/Pure/PIDE/blob.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/blob.scala	Sat Jul 09 13:29:33 2011 +0200
@@ -0,0 +1,28 @@
+/*  Title:      Pure/PIDE/blob.scala
+    Author:     Makarius
+
+Unidentified text with markup.
+*/
+
+package isabelle
+
+
+object Blob
+{
+  sealed case class State(val blob: Blob, val markup: Markup_Tree = Markup_Tree.empty)
+  {
+    def + (info: Text.Info[Any]): State = copy(markup = markup + info)
+  }
+}
+
+
+sealed case class Blob(val source: String)
+{
+  def source(range: Text.Range): String = source.substring(range.start, range.stop)
+
+  lazy val symbol_index = new Symbol.Index(source)
+  def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
+  def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
+
+  val empty_state: Blob.State = Blob.State(this)
+}