src/Tools/VSCode/extension/src/decorations.ts
author wenzelm
Fri Mar 10 16:07:20 2017 +0100 (2017-03-10)
changeset 65173 3700be571a01
parent 65171 63655086649f
child 65176 908d8be90533
permissions -rw-r--r--
more compact protocol message;
     1 'use strict';
     2 
     3 import * as vscode from 'vscode'
     4 import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions,
     5   TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
     6 
     7 
     8 /* known decoration types */
     9 
    10 export const types = new Map<string, TextEditorDecorationType>()
    11 
    12 const background_colors = [
    13   "unprocessed1",
    14   "running1",
    15   "bad",
    16   "intensify",
    17   "entity",
    18   "quoted",
    19   "antiquoted",
    20   "active",
    21   "active_result",
    22   "markdown_item1",
    23   "markdown_item2",
    24   "markdown_item3",
    25   "markdown_item4"
    26 ]
    27 
    28 const foreground_colors = [
    29   "quoted",
    30   "antiquoted"
    31 ]
    32 
    33 const dotted_colors = [
    34   "writeln",
    35   "information",
    36   "warning"
    37 ]
    38 
    39 const text_colors = [
    40   "keyword1",
    41   "keyword2",
    42   "keyword3",
    43   "quasi_keyword",
    44   "improper",
    45   "operator",
    46   "tfree",
    47   "tvar",
    48   "free",
    49   "skolem",
    50   "bound",
    51   "var",
    52   "inner_numeral",
    53   "inner_quoted",
    54   "inner_cartouche",
    55   "inner_comment",
    56   "dynamic",
    57   "class_parameter",
    58   "antiquote"
    59 ]
    60 
    61 function get_color(color: string, light: boolean): string
    62 {
    63   const config = color + (light ? "_light" : "_dark") + "_color"
    64   return vscode.workspace.getConfiguration("isabelle").get<string>(config)
    65 }
    66 
    67 export function init(context: ExtensionContext)
    68 {
    69   function decoration(options: DecorationRenderOptions): TextEditorDecorationType
    70   {
    71     const typ = vscode.window.createTextEditorDecorationType(options)
    72     context.subscriptions.push(typ)
    73     return typ
    74   }
    75 
    76   function background(color: string): TextEditorDecorationType
    77   {
    78     return decoration(
    79       { light: { backgroundColor: get_color(color, true) },
    80         dark: { backgroundColor: get_color(color, false) } })
    81   }
    82 
    83   function text_color(color: string): TextEditorDecorationType
    84   {
    85     return decoration(
    86       { light: { color: get_color(color, true) },
    87         dark: { color: get_color(color, false) } })
    88   }
    89 
    90   function bottom_border(width: string, style: string, color: string): TextEditorDecorationType
    91   {
    92     const border = `${width} none; border-bottom-style: ${style}; border-color: `
    93     return decoration(
    94       { light: { border: border + get_color(color, true) },
    95         dark: { border: border + get_color(color, false) } })
    96   }
    97 
    98   types.clear
    99   for (const color of background_colors) {
   100     types["background_" + color] = background(color)
   101   }
   102   for (const color of foreground_colors) {
   103     types["foreground_" + color] = background(color) // approximation
   104   }
   105   for (const color of dotted_colors) {
   106     types["dotted_" + color] = bottom_border("2px", "dotted", color)
   107   }
   108   for (const color of text_colors) {
   109     types["text_" + color] = text_color(color)
   110   }
   111   types["spell_checker"] = bottom_border("1px", "solid", "spell_checker")
   112 }
   113 
   114 
   115 /* decoration for document node */
   116 
   117 interface DecorationOpts {
   118   range: number[],
   119   hover_message?: MarkedString | MarkedString[]
   120 }
   121 
   122 export interface Decoration
   123 {
   124   uri: string,
   125   "type": string,
   126   content: DecorationOpts[]
   127 }
   128 
   129 type Content = Range[] | DecorationOptions[]
   130 const document_decorations = new Map<string, Map<string, Content>>()
   131 
   132 export function close_document(document: TextDocument)
   133 {
   134   document_decorations.delete(document.uri.toString())
   135 }
   136 
   137 export function apply_decoration(decoration: Decoration)
   138 {
   139   const typ = types[decoration.type]
   140   if (typ) {
   141     const uri = Uri.parse(decoration.uri).toString()
   142     const content: DecorationOptions[] = decoration.content.map(opt =>
   143       {
   144         const r = opt.range
   145         return {
   146           range: new Range(new Position(r[0], r[1]), new Position(r[2], r[3])),
   147           hoverMessage: opt.hover_message
   148         }
   149       })
   150 
   151     const document = document_decorations.get(uri) || new Map<string, Content>()
   152     document.set(decoration.type, content)
   153     document_decorations.set(uri, document)
   154 
   155     for (const editor of vscode.window.visibleTextEditors) {
   156       if (uri === editor.document.uri.toString()) {
   157         editor.setDecorations(typ, content)
   158       }
   159     }
   160   }
   161 }
   162 
   163 export function update_editor(editor: TextEditor)
   164 {
   165   if (editor) {
   166     const decorations = document_decorations.get(editor.document.uri.toString())
   167     if (decorations) {
   168       for (const [typ, content] of decorations) {
   169         editor.setDecorations(types[typ], content)
   170       }
   171     }
   172   }
   173 }