--- /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)
+}