src/Pure/PIDE/blob.scala
changeset 45455 4f974c0c5c2f
parent 43715 518e44a0ee15
child 49414 d7b5fb2e9ca2
equal deleted inserted replaced
45454:388fb71623dd 45455:4f974c0c5c2f
     9 
     9 
    10 object Blob
    10 object Blob
    11 {
    11 {
    12   sealed case class State(val blob: Blob, val markup: Markup_Tree = Markup_Tree.empty)
    12   sealed case class State(val blob: Blob, val markup: Markup_Tree = Markup_Tree.empty)
    13   {
    13   {
    14     def + (info: Text.Info[Any]): State = copy(markup = markup + info)
    14     def + (info: Text.Markup): State = copy(markup = markup + info)
    15   }
    15   }
    16 }
    16 }
    17 
    17 
    18 
    18 
    19 sealed case class Blob(val source: String)
    19 sealed case class Blob(val source: String)