suppress irrelevant markup for VSCode;
authorwenzelm
Fri Mar 10 21:47:48 2017 +0100 (2017-03-10 ago)
changeset 65176908d8be90533
parent 65175 93fb59c68052
child 65177 976938956460
suppress irrelevant markup for VSCode;
src/Pure/PIDE/markup.scala
src/Pure/PIDE/rendering.scala
src/Tools/VSCode/extension/package.json
src/Tools/VSCode/extension/src/decorations.ts
src/Tools/VSCode/src/vscode_rendering.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Pure/PIDE/markup.scala	Fri Mar 10 18:12:52 2017 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Fri Mar 10 21:47:48 2017 +0100
     1.3 @@ -29,6 +29,8 @@
     1.4      def apply(elem: String): Boolean = rep.contains(elem)
     1.5      def + (elem: String): Elements = new Elements(rep + elem)
     1.6      def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
     1.7 +    def - (elem: String): Elements = new Elements(rep - elem)
     1.8 +    def -- (elems: Elements): Elements = new Elements(rep -- elems.rep)
     1.9      override def toString: String = rep.mkString("Elements(", ",", ")")
    1.10    }
    1.11  
     2.1 --- a/src/Pure/PIDE/rendering.scala	Fri Mar 10 18:12:52 2017 +0100
     2.2 +++ b/src/Pure/PIDE/rendering.scala	Fri Mar 10 21:47:48 2017 +0100
     2.3 @@ -253,7 +253,8 @@
     2.4  
     2.5    /* text background */
     2.6  
     2.7 -  def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Rendering.Color.Value]] =
     2.8 +  def background(elements: Markup.Elements, range: Text.Range, focus: Set[Long])
     2.9 +    : List[Text.Info[Rendering.Color.Value]] =
    2.10    {
    2.11      for {
    2.12        Text.Info(r, result) <-
     3.1 --- a/src/Tools/VSCode/extension/package.json	Fri Mar 10 18:12:52 2017 +0100
     3.2 +++ b/src/Tools/VSCode/extension/package.json	Fri Mar 10 21:47:48 2017 +0100
     3.3 @@ -76,12 +76,6 @@
     3.4                  "isabelle.bad_dark_color": { "type": "string", "default": "rgba(255, 106, 106, 0.39)" },
     3.5                  "isabelle.intensify_light_color": { "type": "string", "default": "rgba(255, 204, 102, 0.39)" },
     3.6                  "isabelle.intensify_dark_color": { "type": "string", "default": "rgba(255, 204, 102, 0.39)" },
     3.7 -                "isabelle.entity_light_color": { "type": "string", "default": "rgba(204, 217, 255, 0.50)" },
     3.8 -                "isabelle.entity_dark_color": { "type": "string", "default": "rgba(204, 217, 255, 0.50)" },
     3.9 -                "isabelle.active_light_color": { "type": "string", "default": "rgba(220, 220, 220, 1.00)" },
    3.10 -                "isabelle.active_dark_color": { "type": "string", "default": "rgba(220, 220, 220, 1.00)" },
    3.11 -                "isabelle.active_result_light_color": { "type": "string", "default": "rgba(153, 153, 102, 1.00)" },
    3.12 -                "isabelle.active_result_dark_color": { "type": "string", "default": "rgba(153, 153, 102, 1.00)" },
    3.13                  "isabelle.markdown_item1_light_color": { "type": "string", "default": "rgba(218, 254, 218, 1.00)" },
    3.14                  "isabelle.markdown_item1_dark_color": { "type": "string", "default": "rgba(218, 254, 218, 1.00)" },
    3.15                  "isabelle.markdown_item2_light_color": { "type": "string", "default": "rgba(255, 240, 204, 1.00)" },
     4.1 --- a/src/Tools/VSCode/extension/src/decorations.ts	Fri Mar 10 18:12:52 2017 +0100
     4.2 +++ b/src/Tools/VSCode/extension/src/decorations.ts	Fri Mar 10 21:47:48 2017 +0100
     4.3 @@ -14,11 +14,8 @@
     4.4    "running1",
     4.5    "bad",
     4.6    "intensify",
     4.7 -  "entity",
     4.8    "quoted",
     4.9    "antiquoted",
    4.10 -  "active",
    4.11 -  "active_result",
    4.12    "markdown_item1",
    4.13    "markdown_item2",
    4.14    "markdown_item3",
     5.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 10 18:12:52 2017 +0100
     5.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 10 21:47:48 2017 +0100
     5.3 @@ -28,6 +28,10 @@
     5.4        Document_Model.Decoration.ranges(prefix + c.toString, color_ranges.getOrElse(c, Nil).reverse))
     5.5    }
     5.6  
     5.7 +  private val background_colors =
     5.8 +    Rendering.Color.background_colors - Rendering.Color.active - Rendering.Color.active_result -
     5.9 +      Rendering.Color.entity
    5.10 +
    5.11    private val dotted_colors =
    5.12      Set(Rendering.Color.writeln, Rendering.Color.information, Rendering.Color.warning)
    5.13  
    5.14 @@ -45,6 +49,9 @@
    5.15    private val diagnostics_elements =
    5.16      Markup.Elements(Markup.LEGACY, Markup.ERROR)
    5.17  
    5.18 +  private val background_elements =
    5.19 +    Rendering.background_elements - Markup.ENTITY -- Rendering.active_elements
    5.20 +
    5.21    private val dotted_elements =
    5.22      Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING)
    5.23  
    5.24 @@ -148,8 +155,8 @@
    5.25    /* decorations */
    5.26  
    5.27    def decorations: List[Document_Model.Decoration] = // list of canonical length and order
    5.28 -    VSCode_Rendering.color_decorations("background_", Rendering.Color.background_colors,
    5.29 -      background(model.content.text_range, Set.empty)) :::
    5.30 +    VSCode_Rendering.color_decorations("background_", VSCode_Rendering.background_colors,
    5.31 +      background(VSCode_Rendering.background_elements, model.content.text_range, Set.empty)) :::
    5.32      VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors,
    5.33        foreground(model.content.text_range)) :::
    5.34      VSCode_Rendering.color_decorations("text_", Rendering.Color.text_colors,
     6.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Mar 10 18:12:52 2017 +0100
     6.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Mar 10 21:47:48 2017 +0100
     6.3 @@ -309,7 +309,8 @@
     6.4  
     6.5              // background color
     6.6              for {
     6.7 -              Text.Info(range, c) <- rendering.background(line_range, caret_focus)
     6.8 +              Text.Info(range, c) <-
     6.9 +                rendering.background(Rendering.background_elements, line_range, caret_focus)
    6.10                r <- JEdit_Lib.gfx_range(text_area, range)
    6.11              } {
    6.12                gfx.setColor(rendering.color(c))