--- a/src/Pure/PIDE/rendering.scala Tue May 23 14:23:26 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala Tue May 23 20:38:34 2017 +0200
@@ -41,9 +41,9 @@
values -- background_colors -- foreground_colors -- message_underline_colors --
message_background_colors
- // overview
+ // text overview
val unprocessed, running = Value
- val overview_colors = Set(unprocessed, running, error, warning)
+ val text_overview_colors = Set(unprocessed, running, error, warning)
}
--- a/src/Tools/VSCode/extension/package.json Tue May 23 14:23:26 2017 +0200
+++ b/src/Tools/VSCode/extension/package.json Tue May 23 20:38:34 2017 +0200
@@ -68,8 +68,12 @@
"default": "",
"description": "Cygwin installation on Windows (only relevant when running directly from the Isabelle repository)."
},
+ "isabelle.unprocessed_light_color": { "type": "string", "default": "rgba(255, 160, 160, 1.00)" },
+ "isabelle.unprocessed_dark_color": { "type": "string", "default": "rgba(97, 0, 97, 1.00)" },
"isabelle.unprocessed1_light_color": { "type": "string", "default": "rgba(255, 160, 160, 0.20)" },
"isabelle.unprocessed1_dark_color": { "type": "string", "default": "rgba(97, 0, 97, 0.20)" },
+ "isabelle.running_light_color": { "type": "string", "default": "rgba(97, 0, 97, 1.00)" },
+ "isabelle.running_dark_color": { "type": "string", "default": "rgba(255, 160, 160, 1.00)" },
"isabelle.running1_light_color": { "type": "string", "default": "rgba(97, 0, 97, 0.40)" },
"isabelle.running1_dark_color": { "type": "string", "default": "rgba(255, 160, 160, 0.40)" },
"isabelle.bad_light_color": { "type": "string", "default": "rgba(255, 106, 106, 0.40)" },
@@ -94,6 +98,8 @@
"isabelle.information_dark_color": { "type": "string", "default": "rgba(193, 223, 238, 1.0)" },
"isabelle.warning_light_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" },
"isabelle.warning_dark_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" },
+ "isabelle.error_light_color": { "type": "string", "default": "rgba(178, 34, 34, 1.00)" },
+ "isabelle.error_dark_color": { "type": "string", "default": "rgba(178, 34, 34, 1.00)" },
"isabelle.spell_checker_light_color": { "type": "string", "default": "rgba(0, 0, 255, 1.0)" },
"isabelle.spell_checker_dark_color": { "type": "string", "default": "rgba(86, 156, 214, 1.00)" },
"isabelle.main_light_color": { "type": "string", "default": "rgba(0, 0, 0, 1.00)" },
--- a/src/Tools/VSCode/extension/src/decorations.ts Tue May 23 14:23:26 2017 +0200
+++ b/src/Tools/VSCode/extension/src/decorations.ts Tue May 23 20:38:34 2017 +0200
@@ -57,6 +57,13 @@
"antiquote"
]
+const text_overview_colors = [
+ "unprocessed",
+ "running",
+ "error",
+ "warning"
+]
+
/* init */
@@ -85,6 +92,14 @@
dark: { color: get_color(color, false) } })
}
+ function text_overview_color(color: string): TextEditorDecorationType
+ {
+ return decoration(
+ { overviewRulerLane: vscode.OverviewRulerLane.Right,
+ light: { overviewRulerColor: get_color(color, true) },
+ dark: { overviewRulerColor: get_color(color, false) } })
+ }
+
function bottom_border(width: string, style: string, color: string): TextEditorDecorationType
{
const border = `${width} none; border-bottom-style: ${style}; border-color: `
@@ -122,6 +137,9 @@
for (const color of text_colors) {
types.set("text_" + color, text_color(color))
}
+ for (const color of text_overview_colors) {
+ types.set("text_overview_" + color, text_overview_color(color))
+ }
types.set("spell_checker", bottom_border("1px", "solid", "spell_checker"))
--- a/src/Tools/VSCode/src/vscode_rendering.scala Tue May 23 14:23:26 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Tue May 23 20:38:34 2017 +0200
@@ -12,6 +12,8 @@
import java.io.{File => JFile}
+import scala.annotation.tailrec
+
object VSCode_Rendering
{
@@ -128,6 +130,37 @@
}
+ /* text overview color */
+
+ private sealed case class Color_Info(
+ color: Rendering.Color.Value, offset: Text.Offset, end_offset: Text.Offset, end_line: Int)
+
+ def text_overview_color: List[Text.Info[Rendering.Color.Value]] =
+ {
+ @tailrec def loop(offset: Text.Offset, line: Int, lines: List[Line], colors: List[Color_Info])
+ : List[Text.Info[Rendering.Color.Value]] =
+ {
+ if (lines.nonEmpty) {
+ val end_offset = offset + lines.head.text.length
+ val colors1 =
+ (overview_color(Text.Range(offset, end_offset)), colors) match {
+ case (Some(color), old :: rest) if color == old.color && line == old.end_line =>
+ old.copy(end_offset = end_offset, end_line = line + 1) :: rest
+ case (Some(color), _) =>
+ Color_Info(color, offset, end_offset, line + 1) :: colors
+ case (None, _) => colors
+ }
+ loop(end_offset + 1, line + 1, lines.tail, colors1)
+ }
+ else {
+ colors.reverse.map(info =>
+ Text.Info(Text.Range(info.offset, info.end_offset), info.color))
+ }
+ }
+ loop(0, 0, model.content.doc.lines, Nil)
+ }
+
+
/* dotted underline */
def dotted(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
@@ -158,6 +191,8 @@
foreground(model.content.text_range)) :::
VSCode_Rendering.color_decorations("text_", Rendering.Color.text_colors,
text_color(model.content.text_range)) :::
+ VSCode_Rendering.color_decorations("text_overview_", Rendering.Color.text_overview_colors,
+ text_overview_color) :::
VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors,
dotted(model.content.text_range)) :::
List(spell_checker)