# HG changeset patch
# User wenzelm
# Date 1489178868 -3600
# Node ID 908d8be905330b58bd833990f369527b4ec06ecf
# Parent  93fb59c6805241f5f36f9f8971b78d49843e5000
suppress irrelevant markup for VSCode;

diff -r 93fb59c68052 -r 908d8be90533 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Mar 10 18:12:52 2017 +0100
+++ b/src/Pure/PIDE/markup.scala	Fri Mar 10 21:47:48 2017 +0100
@@ -29,6 +29,8 @@
     def apply(elem: String): Boolean = rep.contains(elem)
     def + (elem: String): Elements = new Elements(rep + elem)
     def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
+    def - (elem: String): Elements = new Elements(rep - elem)
+    def -- (elems: Elements): Elements = new Elements(rep -- elems.rep)
     override def toString: String = rep.mkString("Elements(", ",", ")")
   }
 
diff -r 93fb59c68052 -r 908d8be90533 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Fri Mar 10 18:12:52 2017 +0100
+++ b/src/Pure/PIDE/rendering.scala	Fri Mar 10 21:47:48 2017 +0100
@@ -253,7 +253,8 @@
 
   /* text background */
 
-  def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Rendering.Color.Value]] =
+  def background(elements: Markup.Elements, range: Text.Range, focus: Set[Long])
+    : List[Text.Info[Rendering.Color.Value]] =
   {
     for {
       Text.Info(r, result) <-
diff -r 93fb59c68052 -r 908d8be90533 src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Fri Mar 10 18:12:52 2017 +0100
+++ b/src/Tools/VSCode/extension/package.json	Fri Mar 10 21:47:48 2017 +0100
@@ -76,12 +76,6 @@
                 "isabelle.bad_dark_color": { "type": "string", "default": "rgba(255, 106, 106, 0.39)" },
                 "isabelle.intensify_light_color": { "type": "string", "default": "rgba(255, 204, 102, 0.39)" },
                 "isabelle.intensify_dark_color": { "type": "string", "default": "rgba(255, 204, 102, 0.39)" },
-                "isabelle.entity_light_color": { "type": "string", "default": "rgba(204, 217, 255, 0.50)" },
-                "isabelle.entity_dark_color": { "type": "string", "default": "rgba(204, 217, 255, 0.50)" },
-                "isabelle.active_light_color": { "type": "string", "default": "rgba(220, 220, 220, 1.00)" },
-                "isabelle.active_dark_color": { "type": "string", "default": "rgba(220, 220, 220, 1.00)" },
-                "isabelle.active_result_light_color": { "type": "string", "default": "rgba(153, 153, 102, 1.00)" },
-                "isabelle.active_result_dark_color": { "type": "string", "default": "rgba(153, 153, 102, 1.00)" },
                 "isabelle.markdown_item1_light_color": { "type": "string", "default": "rgba(218, 254, 218, 1.00)" },
                 "isabelle.markdown_item1_dark_color": { "type": "string", "default": "rgba(218, 254, 218, 1.00)" },
                 "isabelle.markdown_item2_light_color": { "type": "string", "default": "rgba(255, 240, 204, 1.00)" },
diff -r 93fb59c68052 -r 908d8be90533 src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Fri Mar 10 18:12:52 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Fri Mar 10 21:47:48 2017 +0100
@@ -14,11 +14,8 @@
   "running1",
   "bad",
   "intensify",
-  "entity",
   "quoted",
   "antiquoted",
-  "active",
-  "active_result",
   "markdown_item1",
   "markdown_item2",
   "markdown_item3",
diff -r 93fb59c68052 -r 908d8be90533 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 10 18:12:52 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Mar 10 21:47:48 2017 +0100
@@ -28,6 +28,10 @@
       Document_Model.Decoration.ranges(prefix + c.toString, color_ranges.getOrElse(c, Nil).reverse))
   }
 
+  private val background_colors =
+    Rendering.Color.background_colors - Rendering.Color.active - Rendering.Color.active_result -
+      Rendering.Color.entity
+
   private val dotted_colors =
     Set(Rendering.Color.writeln, Rendering.Color.information, Rendering.Color.warning)
 
@@ -45,6 +49,9 @@
   private val diagnostics_elements =
     Markup.Elements(Markup.LEGACY, Markup.ERROR)
 
+  private val background_elements =
+    Rendering.background_elements - Markup.ENTITY -- Rendering.active_elements
+
   private val dotted_elements =
     Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING)
 
@@ -148,8 +155,8 @@
   /* decorations */
 
   def decorations: List[Document_Model.Decoration] = // list of canonical length and order
-    VSCode_Rendering.color_decorations("background_", Rendering.Color.background_colors,
-      background(model.content.text_range, Set.empty)) :::
+    VSCode_Rendering.color_decorations("background_", VSCode_Rendering.background_colors,
+      background(VSCode_Rendering.background_elements, model.content.text_range, Set.empty)) :::
     VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors,
       foreground(model.content.text_range)) :::
     VSCode_Rendering.color_decorations("text_", Rendering.Color.text_colors,
diff -r 93fb59c68052 -r 908d8be90533 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Mar 10 18:12:52 2017 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Mar 10 21:47:48 2017 +0100
@@ -309,7 +309,8 @@
 
             // background color
             for {
-              Text.Info(range, c) <- rendering.background(line_range, caret_focus)
+              Text.Info(range, c) <-
+                rendering.background(Rendering.background_elements, line_range, caret_focus)
               r <- JEdit_Lib.gfx_range(text_area, range)
             } {
               gfx.setColor(rendering.color(c))