src/Pure/PIDE/blob.scala
author wenzelm
Tue, 29 Nov 2011 21:50:00 +0100
changeset 45674 eb65c9d17e2f
parent 45455 4f974c0c5c2f
child 49414 d7b5fb2e9ca2
permissions -rw-r--r--
clarified Time vs. Timing;

/*  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.Markup): 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)
}