src/Pure/PIDE/blob.scala
changeset 45455 4f974c0c5c2f
parent 43715 518e44a0ee15
child 49414 d7b5fb2e9ca2
     1.1 --- a/src/Pure/PIDE/blob.scala	Fri Nov 11 14:07:20 2011 +0100
     1.2 +++ b/src/Pure/PIDE/blob.scala	Fri Nov 11 14:24:38 2011 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  {
     1.5    sealed case class State(val blob: Blob, val markup: Markup_Tree = Markup_Tree.empty)
     1.6    {
     1.7 -    def + (info: Text.Info[Any]): State = copy(markup = markup + info)
     1.8 +    def + (info: Text.Markup): State = copy(markup = markup + info)
     1.9    }
    1.10  }
    1.11