--- a/src/Tools/VSCode/extension/package.json Sun Mar 05 22:06:13 2017 +0100
+++ b/src/Tools/VSCode/extension/package.json Sun Mar 05 22:32:33 2017 +0100
@@ -93,7 +93,11 @@
"isabelle.quoted_light_color": { "type": "string", "default": "rgba(139, 139, 139, 0.10)" },
"isabelle.quoted_dark_color": { "type": "string", "default": "rgba(139, 139, 139, 0.10)" },
"isabelle.antiquoted_light_color": { "type": "string", "default": "rgba(255, 200, 50, 0.10)" },
- "isabelle.antiquoted_dark_color": { "type": "string", "default": "rgba(255, 200, 50, 0.10)" }
+ "isabelle.antiquoted_dark_color": { "type": "string", "default": "rgba(255, 200, 50, 0.10)" },
+ "isabelle.writeln_light_color": { "type": "string", "default": "rgba(192, 192, 192, 1.0)" },
+ "isabelle.writeln_dark_color": { "type": "string", "default": "rgba(192, 192, 192, 1.0)" },
+ "isabelle.information_light_color": { "type": "string", "default": "rgba(193, 223, 238, 1.0)" },
+ "isabelle.information_dark_color": { "type": "string", "default": "rgba(193, 223, 238, 1.0)" }
}
}
},
--- a/src/Tools/VSCode/extension/src/decorations.ts Sun Mar 05 22:06:13 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts Sun Mar 05 22:32:33 2017 +0100
@@ -30,11 +30,15 @@
"antiquoted"
]
-function property(prop: string, config: string): Object
+const dotted_colors = [
+ "writeln",
+ "information"
+]
+
+function get_color(color: string, light: boolean): string
{
- let res = {}
- res[prop] = vscode.workspace.getConfiguration("isabelle").get<string>(config)
- return res
+ const config = color.concat(light ? "_light" : "_dark").concat("_color")
+ return vscode.workspace.getConfiguration("isabelle").get<string>(config)
}
export function init(context: ExtensionContext)
@@ -48,10 +52,17 @@
function background(color: string): TextEditorDecorationType
{
- const prop = "backgroundColor"
- const light = property(prop, color.concat("_light_color"))
- const dark = property(prop, color.concat("_dark_color"))
- return decoration({ light: light, dark: dark })
+ return decoration(
+ { light: { backgroundColor: get_color(color, true) },
+ dark: { backgroundColor: get_color(color, false) } })
+ }
+
+ function dotted(color: string): TextEditorDecorationType
+ {
+ const border = "2px none; border-bottom-style: dotted; border-color: "
+ return decoration(
+ { light: { border: border.concat(get_color(color, true)) },
+ dark: { border: border.concat(get_color(color, false)) } })
}
types.clear
@@ -61,6 +72,9 @@
for (let color of foreground_colors) {
types["foreground_".concat(color)] = background(color) // approximation
}
+ for (let color of dotted_colors) {
+ types["dotted_".concat(color)] = dotted(color)
+ }
types["hover_message"] = decoration({})
}
--- a/src/Tools/VSCode/src/vscode_rendering.scala Sun Mar 05 22:06:13 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Sun Mar 05 22:32:33 2017 +0100
@@ -17,7 +17,7 @@
{
/* decorations */
- private def color_decorations(prefix: String, types: Rendering.Color.ValueSet,
+ private def color_decorations(prefix: String, types: Set[Rendering.Color.Value],
colors: List[Text.Info[Rendering.Color.Value]]): List[Document_Model.Decoration] =
{
val color_ranges =
@@ -29,13 +29,16 @@
color_ranges.getOrElse(c, Nil).reverse.map(r => Text.Info(r, Nil: List[XML.Body]))))
}
+ private val dotted_colors =
+ Set(Rendering.Color.writeln, Rendering.Color.information)
+
/* diagnostic messages */
private val message_severity =
Map(
- Markup.WRITELN -> Protocol.DiagnosticSeverity.Information,
- Markup.INFORMATION -> Protocol.DiagnosticSeverity.Information,
+ Markup.WRITELN -> Protocol.DiagnosticSeverity.Hint,
+ Markup.INFORMATION -> Protocol.DiagnosticSeverity.Hint,
Markup.WARNING -> Protocol.DiagnosticSeverity.Warning,
Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning,
Markup.ERROR -> Protocol.DiagnosticSeverity.Error)
@@ -46,6 +49,9 @@
private val diagnostics_elements =
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
+ private val dotted_elements =
+ Markup.Elements(Markup.WRITELN, Markup.INFORMATION)
+
private val hover_message_elements = Markup.Elements(Markup.BAD)
private val hyperlink_elements =
@@ -107,6 +113,12 @@
}
+ /* dotted underline */
+
+ def dotted(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
+ message_underline_color(VSCode_Rendering.dotted_elements, range)
+
+
/* decorations */
def hover_message: Document_Model.Decoration =
@@ -133,7 +145,9 @@
VSCode_Rendering.color_decorations("background_", Rendering.Color.background,
background(model.content.text_range, Set.empty)) :::
VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground,
- foreground(model.content.text_range))
+ foreground(model.content.text_range)) :::
+ VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors,
+ dotted(model.content.text_range))
def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration =
{