decorations for text color;
authorwenzelm
Tue Mar 07 18:50:42 2017 +0100 (2017-03-07)
changeset 6514669ea3f1715be
parent 65145 576d52aa0a78
child 65147 a1aaa18091b0
decorations for text color;
src/Tools/VSCode/extension/package.json
src/Tools/VSCode/extension/src/decorations.ts
src/Tools/VSCode/src/vscode_rendering.scala
     1.1 --- a/src/Tools/VSCode/extension/package.json	Tue Mar 07 18:12:59 2017 +0100
     1.2 +++ b/src/Tools/VSCode/extension/package.json	Tue Mar 07 18:50:42 2017 +0100
     1.3 @@ -101,7 +101,45 @@
     1.4                  "isabelle.warning_light_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" },
     1.5                  "isabelle.warning_dark_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" },
     1.6                  "isabelle.spell_checker_light_color": { "type": "string", "default": "rgba(0, 0, 255, 1.0)" },
     1.7 -                "isabelle.spell_checker_dark_color": { "type": "string", "default": "rgba(0, 0, 255, 1.0)" }
     1.8 +                "isabelle.spell_checker_dark_color": { "type": "string", "default": "rgba(0, 0, 255, 1.0)" },
     1.9 +                "isabelle.keyword1_light_color": { "type": "string", "default": "rgba(0, 102, 153, 1.00)" },
    1.10 +                "isabelle.keyword1_dark_color": { "type": "string", "default": "rgba(0, 102, 153, 1.00)" },
    1.11 +                "isabelle.keyword2_light_color": { "type": "string", "default": "rgba(0, 153, 102, 1.00)" },
    1.12 +                "isabelle.keyword2_dark_color": { "type": "string", "default": "rgba(0, 153, 102, 1.00)" },
    1.13 +                "isabelle.keyword3_light_color": { "type": "string", "default": "rgba(0, 153, 255, 1.00)" },
    1.14 +                "isabelle.keyword3_dark_color": { "type": "string", "default": "rgba(0, 153, 255, 1.00)" },
    1.15 +                "isabelle.quasi_keyword_light_color": { "type": "string", "default": "rgba(153, 102, 255, 1.00)" },
    1.16 +                "isabelle.quasi_keyword_dark_color": { "type": "string", "default": "rgba(153, 102, 255, 1.00)" },
    1.17 +                "isabelle.improper_light_color": { "type": "string", "default": "rgba(255, 80, 80, 1.00)" },
    1.18 +                "isabelle.improper_dark_color": { "type": "string", "default": "rgba(255, 80, 80, 1.00)" },
    1.19 +                "isabelle.operator_light_color": { "type": "string", "default": "rgba(50, 50, 50, 1.00)" },
    1.20 +                "isabelle.operator_dark_color": { "type": "string", "default": "rgba(50, 50, 50, 1.00)" },
    1.21 +                "isabelle.tfree_light_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" },
    1.22 +                "isabelle.tfree_dark_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" },
    1.23 +                "isabelle.tvar_light_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" },
    1.24 +                "isabelle.tvar_dark_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" },
    1.25 +                "isabelle.free_light_color": { "type": "string", "default": "rgba(0, 0, 255, 1.00)" },
    1.26 +                "isabelle.free_dark_color": { "type": "string", "default": "rgba(0, 0, 255, 1.00)" },
    1.27 +                "isabelle.skolem_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
    1.28 +                "isabelle.skolem_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
    1.29 +                "isabelle.bound_light_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" },
    1.30 +                "isabelle.bound_dark_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" },
    1.31 +                "isabelle.var_light_color": { "type": "string", "default": "rgba(0, 0, 155, 1.00)" },
    1.32 +                "isabelle.var_dark_color": { "type": "string", "default": "rgba(0, 0, 155, 1.00)" },
    1.33 +                "isabelle.inner_numeral_light_color": { "type": "string", "default": "rgba(255, 0, 0, 1.00)" },
    1.34 +                "isabelle.inner_numeral_dark_color": { "type": "string", "default": "rgba(255, 0, 0, 1.00)" },
    1.35 +                "isabelle.inner_quoted_light_color": { "type": "string", "default": "rgba(255, 0, 204, 1.00)" },
    1.36 +                "isabelle.inner_quoted_dark_color": { "type": "string", "default": "rgba(255, 0, 204, 1.00)" },
    1.37 +                "isabelle.inner_cartouche_light_color": { "type": "string", "default": "rgba(204, 102, 0, 1.00)" },
    1.38 +                "isabelle.inner_cartouche_dark_color": { "type": "string", "default": "rgba(204, 102, 0, 1.00)" },
    1.39 +                "isabelle.inner_comment_light_color": { "type": "string", "default": "rgba(204, 0, 0, 1.00)" },
    1.40 +                "isabelle.inner_comment_dark_color": { "type": "string", "default": "rgba(204, 0, 0, 1.00)" },
    1.41 +                "isabelle.dynamic_light_color": { "type": "string", "default": "rgba(123, 164, 40, 1.00)" },
    1.42 +                "isabelle.dynamic_dark_color": { "type": "string", "default": "rgba(123, 164, 40, 1.00)" },
    1.43 +                "isabelle.class_parameter_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
    1.44 +                "isabelle.class_parameter_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
    1.45 +                "isabelle.antiquote_light_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" },
    1.46 +                "isabelle.antiquote_dark_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" }
    1.47              }
    1.48          }
    1.49      },
     2.1 --- a/src/Tools/VSCode/extension/src/decorations.ts	Tue Mar 07 18:12:59 2017 +0100
     2.2 +++ b/src/Tools/VSCode/extension/src/decorations.ts	Tue Mar 07 18:50:42 2017 +0100
     2.3 @@ -36,6 +36,28 @@
     2.4    "warning"
     2.5  ]
     2.6  
     2.7 +const text_colors = [
     2.8 +  "keyword1",
     2.9 +  "keyword2",
    2.10 +  "keyword3",
    2.11 +  "quasi_keyword",
    2.12 +  "improper",
    2.13 +  "operator",
    2.14 +  "tfree",
    2.15 +  "tvar",
    2.16 +  "free",
    2.17 +  "skolem",
    2.18 +  "bound",
    2.19 +  "var",
    2.20 +  "inner_numeral",
    2.21 +  "inner_quoted",
    2.22 +  "inner_cartouche",
    2.23 +  "inner_comment",
    2.24 +  "dynamic",
    2.25 +  "class_parameter",
    2.26 +  "antiquote"
    2.27 +]
    2.28 +
    2.29  function get_color(color: string, light: boolean): string
    2.30  {
    2.31    const config = color.concat(light ? "_light" : "_dark").concat("_color")
    2.32 @@ -58,6 +80,13 @@
    2.33          dark: { backgroundColor: get_color(color, false) } })
    2.34    }
    2.35  
    2.36 +  function text_color(color: string): TextEditorDecorationType
    2.37 +  {
    2.38 +    return decoration(
    2.39 +      { light: { color: get_color(color, true) },
    2.40 +        dark: { color: get_color(color, false) } })
    2.41 +  }
    2.42 +
    2.43    function bottom_border(width: string, style: string, color: string): TextEditorDecorationType
    2.44    {
    2.45      const border = `${width} none; border-bottom-style: ${style}; border-color: `
    2.46 @@ -76,6 +105,9 @@
    2.47    for (let color of dotted_colors) {
    2.48      types["dotted_".concat(color)] = bottom_border("2px", "dotted", color)
    2.49    }
    2.50 +  for (let color of text_colors) {
    2.51 +    types["text_".concat(color)] = text_color(color)
    2.52 +  }
    2.53    types["spell_checker"] = bottom_border("1px", "solid", "spell_checker")
    2.54  }
    2.55  
     3.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Mar 07 18:12:59 2017 +0100
     3.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Mar 07 18:50:42 2017 +0100
     3.3 @@ -111,6 +111,17 @@
     3.4    }
     3.5  
     3.6  
     3.7 +  /* text color */
     3.8 +
     3.9 +  def text_color(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
    3.10 +  {
    3.11 +    snapshot.select(range, Rendering.text_color_elements, _ =>
    3.12 +      {
    3.13 +        case Text.Info(_, elem) => Rendering.text_color.get(elem.name)
    3.14 +      })
    3.15 +  }
    3.16 +
    3.17 +
    3.18    /* dotted underline */
    3.19  
    3.20    def dotted(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
    3.21 @@ -139,6 +150,8 @@
    3.22        background(model.content.text_range, Set.empty)) :::
    3.23      VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors,
    3.24        foreground(model.content.text_range)) :::
    3.25 +    VSCode_Rendering.color_decorations("text_", Rendering.Color.text_colors,
    3.26 +      text_color(model.content.text_range)) :::
    3.27      VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors,
    3.28        dotted(model.content.text_range)) :::
    3.29      List(spell_checker)