src/Pure/PIDE/rendering.scala
changeset 65121 12c6774a8f65
parent 65107 70b0113fa4ef
child 65124 759c64c39a6f
     1.1 --- a/src/Pure/PIDE/rendering.scala	Sun Mar 05 19:27:39 2017 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Sun Mar 05 22:06:13 2017 +0100
     1.3 @@ -32,6 +32,14 @@
     1.4      val quoted = Value("quoted")
     1.5      val antiquoted = Value("antiquoted")
     1.6      val foreground = values -- background
     1.7 +
     1.8 +    // underline
     1.9 +    val writeln = Value("writeln")
    1.10 +    val information = Value("information")
    1.11 +    val warning = Value("warning")
    1.12 +    val legacy = Value("legacy")
    1.13 +    val error = Value("error")
    1.14 +    val underline = values -- background -- foreground
    1.15    }
    1.16  
    1.17  
    1.18 @@ -61,6 +69,13 @@
    1.19      Markup.ERROR -> error_pri,
    1.20      Markup.ERROR_MESSAGE -> error_pri)
    1.21  
    1.22 +  val message_underline_color = Map(
    1.23 +    writeln_pri -> Color.writeln,
    1.24 +    information_pri -> Color.information,
    1.25 +    warning_pri -> Color.warning,
    1.26 +    legacy_pri -> Color.legacy,
    1.27 +    error_pri -> Color.error)
    1.28 +
    1.29  
    1.30    /* markup elements */
    1.31  
    1.32 @@ -344,4 +359,21 @@
    1.33      }
    1.34      else Nil
    1.35    }
    1.36 +
    1.37 +
    1.38 +  /* message underline color */
    1.39 +
    1.40 +  def message_underline_color(
    1.41 +    elements: Markup.Elements, range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
    1.42 +  {
    1.43 +    val results =
    1.44 +      snapshot.cumulate[Int](range, 0, elements, _ =>
    1.45 +        {
    1.46 +          case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
    1.47 +        })
    1.48 +    for {
    1.49 +      Text.Info(r, pri) <- results
    1.50 +      color <- Rendering.message_underline_color.get(pri)
    1.51 +    } yield Text.Info(r, color)
    1.52 +  }
    1.53  }