src/Tools/VSCode/extension/src/decorations.ts
author wenzelm
Sat Sep 01 20:20:50 2018 +0200 (10 months ago)
changeset 68871 f5c76072db55
parent 67322 734a4e44b159
child 69320 fc221fa79741
permissions -rw-r--r--
more explicit status for "canceled" command within theory node;
     1 'use strict';
     2 
     3 import * as timers from 'timers'
     4 import { window, OverviewRulerLane } from 'vscode'
     5 import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions,
     6   TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
     7 import { Decoration } from './protocol'
     8 import * as library from './library'
     9 
    10 
    11 /* known decoration types */
    12 
    13 const background_colors = [
    14   "unprocessed1",
    15   "running1",
    16   "canceled",
    17   "bad",
    18   "intensify",
    19   "quoted",
    20   "antiquoted",
    21   "markdown_bullet1",
    22   "markdown_bullet2",
    23   "markdown_bullet3",
    24   "markdown_bullet4"
    25 ]
    26 
    27 const foreground_colors = [
    28   "quoted",
    29   "antiquoted"
    30 ]
    31 
    32 const dotted_colors = [
    33   "writeln",
    34   "information",
    35   "warning"
    36 ]
    37 
    38 const text_colors = [
    39   "main",
    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 const text_overview_colors = [
    62   "unprocessed",
    63   "running",
    64   "error",
    65   "warning"
    66 ]
    67 
    68 
    69 /* setup */
    70 
    71 const types = new Map<string, TextEditorDecorationType>()
    72 
    73 export function setup(context: ExtensionContext)
    74 {
    75   function decoration(options: DecorationRenderOptions): TextEditorDecorationType
    76   {
    77     const typ = window.createTextEditorDecorationType(options)
    78     context.subscriptions.push(typ)
    79     return typ
    80   }
    81 
    82   function background(color: string): TextEditorDecorationType
    83   {
    84     return decoration(
    85       { light: { backgroundColor: library.get_color(color, true) },
    86         dark: { backgroundColor: library.get_color(color, false) } })
    87   }
    88 
    89   function text_color(color: string): TextEditorDecorationType
    90   {
    91     return decoration(
    92       { light: { color: library.get_color(color, true) },
    93         dark: { color: library.get_color(color, false) } })
    94   }
    95 
    96   function text_overview_color(color: string): TextEditorDecorationType
    97   {
    98     return decoration(
    99       { overviewRulerLane: OverviewRulerLane.Right,
   100         light: { overviewRulerColor: library.get_color(color, true) },
   101         dark: { overviewRulerColor: library.get_color(color, false) } })
   102   }
   103 
   104   function bottom_border(width: string, style: string, color: string): TextEditorDecorationType
   105   {
   106     const border = `${width} none; border-bottom-style: ${style}; border-color: `
   107     return decoration(
   108       { light: { border: border + library.get_color(color, true) },
   109         dark: { border: border + library.get_color(color, false) } })
   110   }
   111 
   112 
   113   /* reset */
   114 
   115   types.forEach(typ =>
   116   {
   117     for (const editor of window.visibleTextEditors) {
   118       editor.setDecorations(typ, [])
   119     }
   120     const i = context.subscriptions.indexOf(typ)
   121     if (i >= 0) context.subscriptions.splice(i, 1)
   122     typ.dispose()
   123   })
   124   types.clear()
   125 
   126 
   127   /* init */
   128 
   129   for (const color of background_colors) {
   130     types.set("background_" + color, background(color))
   131   }
   132   for (const color of foreground_colors) {
   133     types.set("foreground_" + color, background(color)) // approximation
   134   }
   135   for (const color of dotted_colors) {
   136     types.set("dotted_" + color, bottom_border("2px", "dotted", color))
   137   }
   138   for (const color of text_colors) {
   139     types.set("text_" + color, text_color(color))
   140   }
   141   for (const color of text_overview_colors) {
   142     types.set("text_overview_" + color, text_overview_color(color))
   143   }
   144   types.set("spell_checker", bottom_border("1px", "solid", "spell_checker"))
   145 
   146 
   147   /* update editors */
   148 
   149   for (const editor of window.visibleTextEditors) {
   150     update_editor(editor)
   151   }
   152 }
   153 
   154 
   155 /* decoration for document node */
   156 
   157 type Content = Range[] | DecorationOptions[]
   158 const document_decorations = new Map<string, Map<string, Content>>()
   159 
   160 export function close_document(document: TextDocument)
   161 {
   162   document_decorations.delete(document.uri.toString())
   163 }
   164 
   165 export function apply_decoration(decoration: Decoration)
   166 {
   167   const typ = types.get(decoration.type)
   168   if (typ) {
   169     const uri = Uri.parse(decoration.uri).toString()
   170     const content: DecorationOptions[] = decoration.content.map(opt =>
   171       {
   172         const r = opt.range
   173         return {
   174           range: new Range(new Position(r[0], r[1]), new Position(r[2], r[3])),
   175           hoverMessage: opt.hover_message
   176         }
   177       })
   178 
   179     const document = document_decorations.get(uri) || new Map<string, Content>()
   180     document.set(decoration.type, content)
   181     document_decorations.set(uri, document)
   182 
   183     for (const editor of window.visibleTextEditors) {
   184       if (uri === editor.document.uri.toString()) {
   185         editor.setDecorations(typ, content)
   186       }
   187     }
   188   }
   189 }
   190 
   191 export function update_editor(editor: TextEditor)
   192 {
   193   if (editor) {
   194     const decorations = document_decorations.get(editor.document.uri.toString())
   195     if (decorations) {
   196       for (const [typ, content] of decorations) {
   197         editor.setDecorations(types.get(typ), content)
   198       }
   199     }
   200   }
   201 }
   202 
   203 
   204 /* handle document changes */
   205 
   206 const touched_documents = new Set<TextDocument>()
   207 let touched_timer: NodeJS.Timer
   208 
   209 function update_touched_documents()
   210 {
   211   const touched_editors: TextEditor[] = []
   212   for (const editor of window.visibleTextEditors) {
   213     if (touched_documents.has(editor.document)) {
   214       touched_editors.push(editor)
   215     }
   216   }
   217   touched_documents.clear
   218   touched_editors.forEach(update_editor)
   219 }
   220 
   221 export function touch_document(document: TextDocument)
   222 {
   223   if (touched_timer) timers.clearTimeout(touched_timer)
   224   touched_documents.add(document)
   225   touched_timer = timers.setTimeout(update_touched_documents, 1000)
   226 }