src/Tools/jEdit/src/rendering.scala
changeset 63347 e344dc82f6c2
parent 63340 29d7ac9bdcb1
child 63441 4c3fa4dba79f
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Jun 22 11:10:18 2016 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Jun 22 16:04:03 2016 +0200
     1.3 @@ -156,7 +156,7 @@
     1.4    private val highlight_elements =
     1.5      Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
     1.6        Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING,
     1.7 -      Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
     1.8 +      Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
     1.9        Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,
    1.10        Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name)
    1.11  
    1.12 @@ -185,9 +185,9 @@
    1.13  
    1.14    private val tooltip_elements =
    1.15      Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
    1.16 -      Markup.SORTING, Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH,
    1.17 -      Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name) ++
    1.18 -    Markup.Elements(tooltip_descriptions.keySet)
    1.19 +      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
    1.20 +      Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
    1.21 +      Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
    1.22  
    1.23    private val gutter_elements =
    1.24      Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
    1.25 @@ -287,6 +287,7 @@
    1.26    val inner_cartouche_color = color_value("inner_cartouche_color")
    1.27    val inner_comment_color = color_value("inner_comment_color")
    1.28    val dynamic_color = color_value("dynamic_color")
    1.29 +  val class_parameter_color = color_value("class_parameter_color")
    1.30  
    1.31    val markdown_item_color1 = color_value("markdown_item_color1")
    1.32    val markdown_item_color2 = color_value("markdown_item_color2")
    1.33 @@ -635,6 +636,9 @@
    1.34            if name == Markup.SORTING || name == Markup.TYPING =>
    1.35              Some(add(prev, r, (true, pretty_typing("::", body))))
    1.36  
    1.37 +          case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
    1.38 +            Some(add(prev, r, (true, Pretty.block(0, body))))
    1.39 +
    1.40            case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
    1.41              Some(add(prev, r, (false, pretty_typing("ML:", body))))
    1.42  
    1.43 @@ -867,6 +871,7 @@
    1.44        Markup.INNER_CARTOUCHE -> inner_cartouche_color,
    1.45        Markup.INNER_COMMENT -> inner_comment_color,
    1.46        Markup.DYNAMIC_FACT -> dynamic_color,
    1.47 +      Markup.CLASS_PARAMETER -> class_parameter_color,
    1.48        Markup.ANTIQUOTE -> antiquote_color,
    1.49        Markup.ML_KEYWORD1 -> keyword1_color,
    1.50        Markup.ML_KEYWORD2 -> keyword2_color,