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