src/Pure/PIDE/blob.scala
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 45455 4f974c0c5c2f
child 49414 d7b5fb2e9ca2
permissions -rw-r--r--
more official command specifications, including source position;
wenzelm@43715
     1
/*  Title:      Pure/PIDE/blob.scala
wenzelm@43715
     2
    Author:     Makarius
wenzelm@43715
     3
wenzelm@43715
     4
Unidentified text with markup.
wenzelm@43715
     5
*/
wenzelm@43715
     6
wenzelm@43715
     7
package isabelle
wenzelm@43715
     8
wenzelm@43715
     9
wenzelm@43715
    10
object Blob
wenzelm@43715
    11
{
wenzelm@43715
    12
  sealed case class State(val blob: Blob, val markup: Markup_Tree = Markup_Tree.empty)
wenzelm@43715
    13
  {
wenzelm@45455
    14
    def + (info: Text.Markup): State = copy(markup = markup + info)
wenzelm@43715
    15
  }
wenzelm@43715
    16
}
wenzelm@43715
    17
wenzelm@43715
    18
wenzelm@43715
    19
sealed case class Blob(val source: String)
wenzelm@43715
    20
{
wenzelm@43715
    21
  def source(range: Text.Range): String = source.substring(range.start, range.stop)
wenzelm@43715
    22
wenzelm@43715
    23
  lazy val symbol_index = new Symbol.Index(source)
wenzelm@43715
    24
  def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
wenzelm@43715
    25
  def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
wenzelm@43715
    26
wenzelm@43715
    27
  val empty_state: Blob.State = Blob.State(this)
wenzelm@43715
    28
}