src/Pure/PIDE/blob.scala
author wenzelm
Fri Nov 11 14:24:38 2011 +0100 (2011-11-11)
changeset 45455 4f974c0c5c2f
parent 43715 518e44a0ee15
child 49414 d7b5fb2e9ca2
permissions -rw-r--r--
prefer statically typed Text.Markup;
     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 }