src/Pure/PIDE/blob.scala
author wenzelm
Sat Jul 09 13:29:33 2011 +0200 (2011-07-09)
changeset 43715 518e44a0ee15
child 45455 4f974c0c5c2f
permissions -rw-r--r--
some support for blobs (arbitrary text files) within document nodes;
     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.Info[Any]): 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 }