src/Tools/VSCode/extension/src/decorations.ts
author wenzelm
Fri, 10 Mar 2017 14:16:45 +0100
changeset 65172 365e97f009ed
parent 65171 63655086649f
child 65173 3700be571a01
permissions -rw-r--r--
default cygwin_root from Isabelle distribution;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65094
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
     1
'use strict';
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
     2
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
     3
import * as vscode from 'vscode'
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
     4
import { Range, MarkedString, DecorationOptions, DecorationRenderOptions,
65135
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
     5
  TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode'
65094
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
     6
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
     7
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
     8
/* known decoration types */
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
     9
65104
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    10
export const types = new Map<string, TextEditorDecorationType>()
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    11
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    12
const background_colors = [
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    13
  "unprocessed1",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    14
  "running1",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    15
  "bad",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    16
  "intensify",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    17
  "entity",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    18
  "quoted",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    19
  "antiquoted",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    20
  "active",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    21
  "active_result",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    22
  "markdown_item1",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    23
  "markdown_item2",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    24
  "markdown_item3",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    25
  "markdown_item4"
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    26
]
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    27
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    28
const foreground_colors = [
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    29
  "quoted",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    30
  "antiquoted"
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    31
]
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    32
65122
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    33
const dotted_colors = [
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    34
  "writeln",
65134
511bf19348d3 clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover);
wenzelm
parents: 65122
diff changeset
    35
  "information",
511bf19348d3 clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover);
wenzelm
parents: 65122
diff changeset
    36
  "warning"
65122
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    37
]
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    38
65146
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    39
const text_colors = [
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    40
  "keyword1",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    41
  "keyword2",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    42
  "keyword3",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    43
  "quasi_keyword",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    44
  "improper",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    45
  "operator",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    46
  "tfree",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    47
  "tvar",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    48
  "free",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    49
  "skolem",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    50
  "bound",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    51
  "var",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    52
  "inner_numeral",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    53
  "inner_quoted",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    54
  "inner_cartouche",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    55
  "inner_comment",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    56
  "dynamic",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    57
  "class_parameter",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    58
  "antiquote"
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    59
]
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    60
65122
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    61
function get_color(color: string, light: boolean): string
65094
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    62
{
65153
wenzelm
parents: 65146
diff changeset
    63
  const config = color + (light ? "_light" : "_dark") + "_color"
65122
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    64
  return vscode.workspace.getConfiguration("isabelle").get<string>(config)
65094
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    65
}
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    66
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    67
export function init(context: ExtensionContext)
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    68
{
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    69
  function decoration(options: DecorationRenderOptions): TextEditorDecorationType
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    70
  {
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    71
    const typ = vscode.window.createTextEditorDecorationType(options)
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    72
    context.subscriptions.push(typ)
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    73
    return typ
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    74
  }
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    75
65104
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    76
  function background(color: string): TextEditorDecorationType
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    77
  {
65122
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    78
    return decoration(
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    79
      { light: { backgroundColor: get_color(color, true) },
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    80
        dark: { backgroundColor: get_color(color, false) } })
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    81
  }
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    82
65146
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    83
  function text_color(color: string): TextEditorDecorationType
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    84
  {
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    85
    return decoration(
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    86
      { light: { color: get_color(color, true) },
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    87
        dark: { color: get_color(color, false) } })
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    88
  }
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    89
65142
368004bed323 decorations for spell-checker;
wenzelm
parents: 65135
diff changeset
    90
  function bottom_border(width: string, style: string, color: string): TextEditorDecorationType
65122
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    91
  {
65142
368004bed323 decorations for spell-checker;
wenzelm
parents: 65135
diff changeset
    92
    const border = `${width} none; border-bottom-style: ${style}; border-color: `
65122
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    93
    return decoration(
65153
wenzelm
parents: 65146
diff changeset
    94
      { light: { border: border + get_color(color, true) },
wenzelm
parents: 65146
diff changeset
    95
        dark: { border: border + get_color(color, false) } })
65104
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    96
  }
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    97
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    98
  types.clear
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65153
diff changeset
    99
  for (const color of background_colors) {
65153
wenzelm
parents: 65146
diff changeset
   100
    types["background_" + color] = background(color)
65104
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
   101
  }
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65153
diff changeset
   102
  for (const color of foreground_colors) {
65153
wenzelm
parents: 65146
diff changeset
   103
    types["foreground_" + color] = background(color) // approximation
65104
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
   104
  }
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65153
diff changeset
   105
  for (const color of dotted_colors) {
65153
wenzelm
parents: 65146
diff changeset
   106
    types["dotted_" + color] = bottom_border("2px", "dotted", color)
65122
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
   107
  }
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65153
diff changeset
   108
  for (const color of text_colors) {
65153
wenzelm
parents: 65146
diff changeset
   109
    types["text_" + color] = text_color(color)
65146
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
   110
  }
65142
368004bed323 decorations for spell-checker;
wenzelm
parents: 65135
diff changeset
   111
  types["spell_checker"] = bottom_border("1px", "solid", "spell_checker")
65094
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   112
}
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   113
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   114
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   115
/* decoration for document node */
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   116
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   117
export interface Decoration
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   118
{
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   119
  uri: string,
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   120
  "type": string,
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   121
  content: DecorationOptions[]
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   122
}
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   123
65135
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   124
type Content = Range[] | DecorationOptions[]
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   125
const document_decorations = new Map<string, Map<string, Content>>()
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   126
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   127
export function close_document(document: TextDocument)
65094
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   128
{
65135
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   129
  document_decorations.delete(document.uri.toString())
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   130
}
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   131
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   132
export function apply_decoration(decoration0: Decoration)
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   133
{
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   134
  const typ = types[decoration0.type]
65094
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   135
  if (typ) {
65135
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   136
    const decoration =
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   137
    {
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   138
      uri: Uri.parse(decoration0.uri).toString(),
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   139
      "type": decoration0.type,
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   140
      content: decoration0.content
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   141
    }
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   142
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65153
diff changeset
   143
    const document = document_decorations.get(decoration.uri) || new Map<string, Content>()
65135
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   144
    document.set(decoration.type, decoration.content)
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   145
    document_decorations.set(decoration.uri, document)
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   146
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65153
diff changeset
   147
    for (const editor of vscode.window.visibleTextEditors) {
65171
63655086649f prefer type equality;
wenzelm
parents: 65168
diff changeset
   148
      if (decoration.uri === editor.document.uri.toString()) {
65135
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   149
        editor.setDecorations(typ, decoration.content)
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   150
      }
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   151
    }
65094
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   152
  }
65135
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   153
}
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   154
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   155
export function update_editor(editor: TextEditor)
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   156
{
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   157
  if (editor) {
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65153
diff changeset
   158
    const decorations = document_decorations.get(editor.document.uri.toString())
65135
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   159
    if (decorations) {
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65153
diff changeset
   160
      for (const [typ, content] of decorations) {
65135
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   161
        editor.setDecorations(types[typ], content)
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   162
      }
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   163
    }
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   164
  }
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   165
}