src/Tools/VSCode/src/vscode_rendering.scala
changeset 65176 908d8be90533
parent 65174 c0388fbd8096
child 65196 e8760a98db78
     1.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 10 18:12:52 2017 +0100
     1.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 10 21:47:48 2017 +0100
     1.3 @@ -28,6 +28,10 @@
     1.4        Document_Model.Decoration.ranges(prefix + c.toString, color_ranges.getOrElse(c, Nil).reverse))
     1.5    }
     1.6  
     1.7 +  private val background_colors =
     1.8 +    Rendering.Color.background_colors - Rendering.Color.active - Rendering.Color.active_result -
     1.9 +      Rendering.Color.entity
    1.10 +
    1.11    private val dotted_colors =
    1.12      Set(Rendering.Color.writeln, Rendering.Color.information, Rendering.Color.warning)
    1.13  
    1.14 @@ -45,6 +49,9 @@
    1.15    private val diagnostics_elements =
    1.16      Markup.Elements(Markup.LEGACY, Markup.ERROR)
    1.17  
    1.18 +  private val background_elements =
    1.19 +    Rendering.background_elements - Markup.ENTITY -- Rendering.active_elements
    1.20 +
    1.21    private val dotted_elements =
    1.22      Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING)
    1.23  
    1.24 @@ -148,8 +155,8 @@
    1.25    /* decorations */
    1.26  
    1.27    def decorations: List[Document_Model.Decoration] = // list of canonical length and order
    1.28 -    VSCode_Rendering.color_decorations("background_", Rendering.Color.background_colors,
    1.29 -      background(model.content.text_range, Set.empty)) :::
    1.30 +    VSCode_Rendering.color_decorations("background_", VSCode_Rendering.background_colors,
    1.31 +      background(VSCode_Rendering.background_elements, model.content.text_range, Set.empty)) :::
    1.32      VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors,
    1.33        foreground(model.content.text_range)) :::
    1.34      VSCode_Rendering.color_decorations("text_", Rendering.Color.text_colors,