--- 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(", ",", ")")
}
--- 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) <-
--- 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)" },
--- 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",
--- 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,
--- 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))