equal
deleted
inserted
replaced
26 } |
26 } |
27 types.toList.map(c => |
27 types.toList.map(c => |
28 Document_Model.Decoration.ranges(prefix + c.toString, color_ranges.getOrElse(c, Nil).reverse)) |
28 Document_Model.Decoration.ranges(prefix + c.toString, color_ranges.getOrElse(c, Nil).reverse)) |
29 } |
29 } |
30 |
30 |
|
31 private val background_colors = |
|
32 Rendering.Color.background_colors - Rendering.Color.active - Rendering.Color.active_result - |
|
33 Rendering.Color.entity |
|
34 |
31 private val dotted_colors = |
35 private val dotted_colors = |
32 Set(Rendering.Color.writeln, Rendering.Color.information, Rendering.Color.warning) |
36 Set(Rendering.Color.writeln, Rendering.Color.information, Rendering.Color.warning) |
33 |
37 |
34 |
38 |
35 /* diagnostic messages */ |
39 /* diagnostic messages */ |
42 |
46 |
43 /* markup elements */ |
47 /* markup elements */ |
44 |
48 |
45 private val diagnostics_elements = |
49 private val diagnostics_elements = |
46 Markup.Elements(Markup.LEGACY, Markup.ERROR) |
50 Markup.Elements(Markup.LEGACY, Markup.ERROR) |
|
51 |
|
52 private val background_elements = |
|
53 Rendering.background_elements - Markup.ENTITY -- Rendering.active_elements |
47 |
54 |
48 private val dotted_elements = |
55 private val dotted_elements = |
49 Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING) |
56 Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING) |
50 |
57 |
51 val tooltip_elements = |
58 val tooltip_elements = |
146 |
153 |
147 |
154 |
148 /* decorations */ |
155 /* decorations */ |
149 |
156 |
150 def decorations: List[Document_Model.Decoration] = // list of canonical length and order |
157 def decorations: List[Document_Model.Decoration] = // list of canonical length and order |
151 VSCode_Rendering.color_decorations("background_", Rendering.Color.background_colors, |
158 VSCode_Rendering.color_decorations("background_", VSCode_Rendering.background_colors, |
152 background(model.content.text_range, Set.empty)) ::: |
159 background(VSCode_Rendering.background_elements, model.content.text_range, Set.empty)) ::: |
153 VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors, |
160 VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors, |
154 foreground(model.content.text_range)) ::: |
161 foreground(model.content.text_range)) ::: |
155 VSCode_Rendering.color_decorations("text_", Rendering.Color.text_colors, |
162 VSCode_Rendering.color_decorations("text_", Rendering.Color.text_colors, |
156 text_color(model.content.text_range)) ::: |
163 text_color(model.content.text_range)) ::: |
157 VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors, |
164 VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors, |