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;
     1 /*  Title:      Pure/PIDE/blob.scala
     2     Author:     Makarius
     3 
     4 Unidentified text with markup.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Blob
    11 {
    12   sealed case class State(val blob: Blob, val markup: Markup_Tree = Markup_Tree.empty)
    13   {
    14     def + (info: Text.Markup): State = copy(markup = markup + info)
    15   }
    16 }
    17 
    18 
    19 sealed case class Blob(val source: String)
    20 {
    21   def source(range: Text.Range): String = source.substring(range.start, range.stop)
    22 
    23   lazy val symbol_index = new Symbol.Index(source)
    24   def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
    25   def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
    26 
    27   val empty_state: Blob.State = Blob.State(this)
    28 }