# HG changeset patch # User wenzelm # Date 1488630966 -3600 # Node ID 66b19d05dcee4175af2ed2df156e77abf9a5dfb8 # Parent 0bf1836ce4b1602afda179413d3340fa3888ddb2 decorations for background and foreground colors; diff -r 0bf1836ce4b1 -r 66b19d05dcee src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Sat Mar 04 13:33:47 2017 +0100 +++ b/src/Pure/PIDE/rendering.scala Sat Mar 04 13:36:06 2017 +0100 @@ -14,19 +14,24 @@ object Color extends Enumeration { + // background val unprocessed1 = Value("unprocessed1") val running1 = Value("running1") val bad = Value("bad") val intensify = Value("intensify") val entity = Value("entity") - val quoted = Value("quoted") - val antiquoted = Value("antiquoted") val active = Value("active") val active_result = Value("active_result") val markdown_item1 = Value("markdown_item1") val markdown_item2 = Value("markdown_item2") val markdown_item3 = Value("markdown_item3") val markdown_item4 = Value("markdown_item4") + val background = values + + // foreground + val quoted = Value("quoted") + val antiquoted = Value("antiquoted") + val foreground = values -- background } diff -r 0bf1836ce4b1 -r 66b19d05dcee src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Sat Mar 04 13:33:47 2017 +0100 +++ b/src/Tools/VSCode/extension/package.json Sat Mar 04 13:36:06 2017 +0100 @@ -67,7 +67,33 @@ "items": { "type": "string" }, "default": [], "description": "Command-line arguments for isabelle vscode_server process." - } + }, + "isabelle.unprocessed1_light_color": { "type": "string", "default": "rgba(255, 160, 160, 0.20)" }, + "isabelle.unprocessed1_dark_color": { "type": "string", "default": "rgba(255, 160, 160, 0.20)" }, + "isabelle.running1_light_color": { "type": "string", "default": "rgba(97, 0, 97, 0.39)" }, + "isabelle.running1_dark_color": { "type": "string", "default": "rgba(97, 0, 97, 0.39)" }, + "isabelle.bad_light_color": { "type": "string", "default": "rgba(255, 106, 106, 0.39)" }, + "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)" }, + "isabelle.markdown_item2_dark_color": { "type": "string", "default": "rgba(255, 240, 204, 1.00)" }, + "isabelle.markdown_item3_light_color": { "type": "string", "default": "rgba(231, 231, 255, 1.00)" }, + "isabelle.markdown_item3_dark_color": { "type": "string", "default": "rgba(231, 231, 255, 1.00)" }, + "isabelle.markdown_item4_light_color": { "type": "string", "default": "rgba(255, 224, 240, 1.00)" }, + "isabelle.markdown_item4_dark_color": { "type": "string", "default": "rgba(255, 224, 240, 1.00)" }, + "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)" } } } }, diff -r 0bf1836ce4b1 -r 66b19d05dcee src/Tools/VSCode/extension/src/decorations.ts --- a/src/Tools/VSCode/extension/src/decorations.ts Sat Mar 04 13:33:47 2017 +0100 +++ b/src/Tools/VSCode/extension/src/decorations.ts Sat Mar 04 13:36:06 2017 +0100 @@ -7,13 +7,36 @@ /* known decoration types */ -export interface Decorations +export const types = new Map() + +const background_colors = [ + "unprocessed1", + "running1", + "bad", + "intensify", + "entity", + "quoted", + "antiquoted", + "active", + "active_result", + "markdown_item1", + "markdown_item2", + "markdown_item3", + "markdown_item4" +] + +const foreground_colors = [ + "quoted", + "antiquoted" +] + +function property(prop: string, config: string): Object { - bad: TextEditorDecorationType + let res = {} + res[prop] = vscode.workspace.getConfiguration("isabelle").get(config) + return res } -export let types: Decorations - export function init(context: ExtensionContext) { function decoration(options: DecorationRenderOptions): TextEditorDecorationType @@ -23,11 +46,22 @@ return typ } - if (!types) - types = - { - bad: decoration({ backgroundColor: 'rgba(255, 106, 106, 0.4)' }) - } + 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 }) + } + + types.clear + for (let color of background_colors) { + types["background_".concat(color)] = background(color) + } + for (let color of foreground_colors) { + types["foreground_".concat(color)] = background(color) // approximation + } + types["bad"] = decoration({}) } diff -r 0bf1836ce4b1 -r 66b19d05dcee src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Sat Mar 04 13:33:47 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Sat Mar 04 13:36:06 2017 +0100 @@ -15,6 +15,25 @@ object VSCode_Rendering { + /* decorations */ + + def color_decorations(prefix: String, types: Rendering.Color.ValueSet, + colors: List[Text.Info[Rendering.Color.Value]]): List[Document_Model.Decoration] = + { + val color_ranges = + (Map.empty[Rendering.Color.Value, List[Text.Range]] /: colors) { + case (m, Text.Info(range, c)) => m + (c -> (range :: m.getOrElse(c, Nil))) + } + for (c <- types.toList) + yield { + val typ = prefix + c.toString + val content = + color_ranges.getOrElse(c, Nil).reverse.map(r => Text.Info(r, Nil: XML.Body)) + Document_Model.Decoration(typ, content) + } + } + + /* diagnostic messages */ private val message_severity = @@ -97,13 +116,21 @@ /* decorations */ def decorations: List[Document_Model.Decoration] = - List(Document_Model.Decoration(Protocol.Decorations.bad, decorations_bad)) + decorations_bad ::: + 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)) - def decorations_bad: List[Text.Info[XML.Body]] = - snapshot.select(model.content.text_range, VSCode_Rendering.bad_elements, _ => - { - case Text.Info(_, XML.Elem(_, body)) => Some(body) - }) + def decorations_bad: List[Document_Model.Decoration] = + { + val content = + snapshot.select(model.content.text_range, VSCode_Rendering.bad_elements, _ => + { + case Text.Info(_, XML.Elem(_, body)) => Some(body) + }) + List(Document_Model.Decoration(Protocol.Decorations.bad, content)) + } def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration = {