src/Pure/PIDE/rendering.scala
changeset 65176 908d8be90533
parent 65150 fa299b4e50c3
child 65190 0dd2ad9dbfc2
     1.1 --- a/src/Pure/PIDE/rendering.scala	Fri Mar 10 18:12:52 2017 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Fri Mar 10 21:47:48 2017 +0100
     1.3 @@ -253,7 +253,8 @@
     1.4  
     1.5    /* text background */
     1.6  
     1.7 -  def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Rendering.Color.Value]] =
     1.8 +  def background(elements: Markup.Elements, range: Text.Range, focus: Set[Long])
     1.9 +    : List[Text.Info[Rendering.Color.Value]] =
    1.10    {
    1.11      for {
    1.12        Text.Info(r, result) <-