src/Pure/PIDE/blob.scala
author wenzelm
Wed, 04 Apr 2012 14:19:47 +0200
changeset 47336 bed4b2738d8a
parent 45455 4f974c0c5c2f
child 49414 d7b5fb2e9ca2
permissions -rw-r--r--
separate module for prover command execution;

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