src/Pure/PIDE/blob.scala

more direct message header: eliminated historic encoding via single letter;

/*  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 init_state: Blob.State = Blob.State(this)
}