src/Pure/PIDE/blob.scala
changeset 43715 518e44a0ee15
child 45455 4f974c0c5c2f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/PIDE/blob.scala	Sat Jul 09 13:29:33 2011 +0200
     1.3 @@ -0,0 +1,28 @@
     1.4 +/*  Title:      Pure/PIDE/blob.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Unidentified text with markup.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +object Blob
    1.14 +{
    1.15 +  sealed case class State(val blob: Blob, val markup: Markup_Tree = Markup_Tree.empty)
    1.16 +  {
    1.17 +    def + (info: Text.Info[Any]): State = copy(markup = markup + info)
    1.18 +  }
    1.19 +}
    1.20 +
    1.21 +
    1.22 +sealed case class Blob(val source: String)
    1.23 +{
    1.24 +  def source(range: Text.Range): String = source.substring(range.start, range.stop)
    1.25 +
    1.26 +  lazy val symbol_index = new Symbol.Index(source)
    1.27 +  def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
    1.28 +  def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
    1.29 +
    1.30 +  val empty_state: Blob.State = Blob.State(this)
    1.31 +}