src/Tools/VSCode/extension/src/decorations.ts
author Thomas Lindae <thomas.lindae@in.tum.de>
Fri, 05 Jul 2024 13:15:05 +0200
changeset 81070 de30087b4ff8
parent 75262 ec62c5401522
child 81071 e1bfcc2a2c05
permissions -rw-r--r--
vscode: switched document_decoration map to use strings as keys instead of Uris, because Uri equality check is inconsistent; disabled decoration requests as decoration caching is already done on client-side;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
75234
57de0062dc1c proper file headers;
wenzelm
parents: 75201
diff changeset
     1
/*  Author:     Makarius
57de0062dc1c proper file headers;
wenzelm
parents: 75201
diff changeset
     2
57de0062dc1c proper file headers;
wenzelm
parents: 75201
diff changeset
     3
PIDE document decorations.
57de0062dc1c proper file headers;
wenzelm
parents: 75201
diff changeset
     4
*/
57de0062dc1c proper file headers;
wenzelm
parents: 75201
diff changeset
     5
65094
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
     6
'use strict';
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
     7
65973
wenzelm
parents: 65969
diff changeset
     8
import * as timers from 'timers'
75126
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
     9
import {window, OverviewRulerLane, Uri} from 'vscode';
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
    10
import { Range, DecorationOptions, DecorationRenderOptions,
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
    11
  TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext } from 'vscode'
75201
8f6b8a46f54c clarified modules: more uniform .scala vs. ts (amending 4519eeefe3b5);
wenzelm
parents: 75185
diff changeset
    12
import { Document_Decorations } from './lsp'
75181
98fbc9accb51 clarified module;
wenzelm
parents: 75135
diff changeset
    13
import * as vscode_lib from './vscode_lib'
65094
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    14
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    15
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    16
/* known decoration types */
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    17
65104
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    18
const background_colors = [
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    19
  "unprocessed1",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    20
  "running1",
68871
f5c76072db55 more explicit status for "canceled" command within theory node;
wenzelm
parents: 67322
diff changeset
    21
  "canceled",
65104
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    22
  "bad",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    23
  "intensify",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    24
  "quoted",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    25
  "antiquoted",
67322
734a4e44b159 clarified terminology of "markdown_bullet";
wenzelm
parents: 66097
diff changeset
    26
  "markdown_bullet1",
734a4e44b159 clarified terminology of "markdown_bullet";
wenzelm
parents: 66097
diff changeset
    27
  "markdown_bullet2",
734a4e44b159 clarified terminology of "markdown_bullet";
wenzelm
parents: 66097
diff changeset
    28
  "markdown_bullet3",
734a4e44b159 clarified terminology of "markdown_bullet";
wenzelm
parents: 66097
diff changeset
    29
  "markdown_bullet4"
65104
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    30
]
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
const foreground_colors = [
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    33
  "quoted",
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    34
  "antiquoted"
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    35
]
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    36
65122
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    37
const dotted_colors = [
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    38
  "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
    39
  "information",
511bf19348d3 clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover);
wenzelm
parents: 65122
diff changeset
    40
  "warning"
65122
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    41
]
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    42
75126
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
    43
export const text_colors = [
65181
b4105202751c tuned colors according to Light+ and Dark+ themes;
wenzelm
parents: 65180
diff changeset
    44
  "main",
65146
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    45
  "keyword1",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    46
  "keyword2",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    47
  "keyword3",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    48
  "quasi_keyword",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    49
  "improper",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    50
  "operator",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    51
  "tfree",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    52
  "tvar",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    53
  "free",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    54
  "skolem",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    55
  "bound",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    56
  "var",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    57
  "inner_numeral",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    58
  "inner_quoted",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    59
  "inner_cartouche",
69320
fc221fa79741 more comment markup;
wenzelm
parents: 68871
diff changeset
    60
  "comment1",
fc221fa79741 more comment markup;
wenzelm
parents: 68871
diff changeset
    61
  "comment2",
fc221fa79741 more comment markup;
wenzelm
parents: 68871
diff changeset
    62
  "comment3",
65146
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    63
  "dynamic",
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    64
  "class_parameter",
69965
da5e7278286b more markup for various text kinds, notably for nested formal comments;
wenzelm
parents: 69352
diff changeset
    65
  "antiquote",
da5e7278286b more markup for various text kinds, notably for nested formal comments;
wenzelm
parents: 69352
diff changeset
    66
  "raw_text",
da5e7278286b more markup for various text kinds, notably for nested formal comments;
wenzelm
parents: 69352
diff changeset
    67
  "plain_text"
65146
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    68
]
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    69
65913
f330f538dae6 support text overview colors via decorations;
wenzelm
parents: 65233
diff changeset
    70
const text_overview_colors = [
f330f538dae6 support text overview colors via decorations;
wenzelm
parents: 65233
diff changeset
    71
  "unprocessed",
f330f538dae6 support text overview colors via decorations;
wenzelm
parents: 65233
diff changeset
    72
  "running",
f330f538dae6 support text overview colors via decorations;
wenzelm
parents: 65233
diff changeset
    73
  "error",
f330f538dae6 support text overview colors via decorations;
wenzelm
parents: 65233
diff changeset
    74
  "warning"
f330f538dae6 support text overview colors via decorations;
wenzelm
parents: 65233
diff changeset
    75
]
f330f538dae6 support text overview colors via decorations;
wenzelm
parents: 65233
diff changeset
    76
65182
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
    77
66097
ee4c2d5b650e tuned signature;
wenzelm
parents: 65974
diff changeset
    78
/* setup */
65182
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
    79
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
    80
const types = new Map<string, TextEditorDecorationType>()
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
    81
66097
ee4c2d5b650e tuned signature;
wenzelm
parents: 65974
diff changeset
    82
export function setup(context: ExtensionContext)
65094
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    83
{
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    84
  function decoration(options: DecorationRenderOptions): TextEditorDecorationType
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    85
  {
65969
1f93eb5c3d77 tuned imports;
wenzelm
parents: 65968
diff changeset
    86
    const typ = window.createTextEditorDecorationType(options)
65094
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    87
    context.subscriptions.push(typ)
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    88
    return typ
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    89
  }
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
    90
65104
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    91
  function background(color: string): TextEditorDecorationType
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
    92
  {
65122
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    93
    return decoration(
75181
98fbc9accb51 clarified module;
wenzelm
parents: 75135
diff changeset
    94
      { light: { backgroundColor: vscode_lib.get_color(color, true) },
98fbc9accb51 clarified module;
wenzelm
parents: 75135
diff changeset
    95
        dark: { backgroundColor: vscode_lib.get_color(color, false) } })
65122
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    96
  }
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
    97
65146
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    98
  function text_color(color: string): TextEditorDecorationType
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
    99
  {
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
   100
    return decoration(
75181
98fbc9accb51 clarified module;
wenzelm
parents: 75135
diff changeset
   101
      { light: { color: vscode_lib.get_color(color, true) },
98fbc9accb51 clarified module;
wenzelm
parents: 75135
diff changeset
   102
        dark: { color: vscode_lib.get_color(color, false) } })
65146
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
   103
  }
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
   104
65913
f330f538dae6 support text overview colors via decorations;
wenzelm
parents: 65233
diff changeset
   105
  function text_overview_color(color: string): TextEditorDecorationType
f330f538dae6 support text overview colors via decorations;
wenzelm
parents: 65233
diff changeset
   106
  {
f330f538dae6 support text overview colors via decorations;
wenzelm
parents: 65233
diff changeset
   107
    return decoration(
65969
1f93eb5c3d77 tuned imports;
wenzelm
parents: 65968
diff changeset
   108
      { overviewRulerLane: OverviewRulerLane.Right,
75181
98fbc9accb51 clarified module;
wenzelm
parents: 75135
diff changeset
   109
        light: { overviewRulerColor: vscode_lib.get_color(color, true) },
98fbc9accb51 clarified module;
wenzelm
parents: 75135
diff changeset
   110
        dark: { overviewRulerColor: vscode_lib.get_color(color, false) } })
65913
f330f538dae6 support text overview colors via decorations;
wenzelm
parents: 65233
diff changeset
   111
  }
f330f538dae6 support text overview colors via decorations;
wenzelm
parents: 65233
diff changeset
   112
65142
368004bed323 decorations for spell-checker;
wenzelm
parents: 65135
diff changeset
   113
  function bottom_border(width: string, style: string, color: string): TextEditorDecorationType
65122
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
   114
  {
65142
368004bed323 decorations for spell-checker;
wenzelm
parents: 65135
diff changeset
   115
    const border = `${width} none; border-bottom-style: ${style}; border-color: `
65122
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
   116
    return decoration(
75181
98fbc9accb51 clarified module;
wenzelm
parents: 75135
diff changeset
   117
      { light: { border: border + vscode_lib.get_color(color, true) },
98fbc9accb51 clarified module;
wenzelm
parents: 75135
diff changeset
   118
        dark: { border: border + vscode_lib.get_color(color, false) } })
65104
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
   119
  }
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
   120
65182
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   121
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   122
  /* reset */
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   123
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   124
  types.forEach(typ =>
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   125
  {
65969
1f93eb5c3d77 tuned imports;
wenzelm
parents: 65968
diff changeset
   126
    for (const editor of window.visibleTextEditors) {
65182
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   127
      editor.setDecorations(typ, [])
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   128
    }
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   129
    const i = context.subscriptions.indexOf(typ)
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   130
    if (i >= 0) context.subscriptions.splice(i, 1)
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   131
    typ.dispose()
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   132
  })
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   133
  types.clear()
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   134
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   135
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   136
  /* init */
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   137
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65153
diff changeset
   138
  for (const color of background_colors) {
65182
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   139
    types.set("background_" + color, background(color))
65104
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
   140
  }
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65153
diff changeset
   141
  for (const color of foreground_colors) {
65182
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   142
    types.set("foreground_" + color, background(color)) // approximation
65104
66b19d05dcee decorations for background and foreground colors;
wenzelm
parents: 65098
diff changeset
   143
  }
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65153
diff changeset
   144
  for (const color of dotted_colors) {
65182
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   145
    types.set("dotted_" + color, bottom_border("2px", "dotted", color))
65122
1edb570f5b17 decorations for dotted underline: less intrusive;
wenzelm
parents: 65106
diff changeset
   146
  }
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65153
diff changeset
   147
  for (const color of text_colors) {
65182
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   148
    types.set("text_" + color, text_color(color))
65146
69ea3f1715be decorations for text color;
wenzelm
parents: 65142
diff changeset
   149
  }
65913
f330f538dae6 support text overview colors via decorations;
wenzelm
parents: 65233
diff changeset
   150
  for (const color of text_overview_colors) {
f330f538dae6 support text overview colors via decorations;
wenzelm
parents: 65233
diff changeset
   151
    types.set("text_overview_" + color, text_overview_color(color))
f330f538dae6 support text overview colors via decorations;
wenzelm
parents: 65233
diff changeset
   152
  }
65182
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   153
  types.set("spell_checker", bottom_border("1px", "solid", "spell_checker"))
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   154
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   155
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   156
  /* update editors */
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   157
65969
1f93eb5c3d77 tuned imports;
wenzelm
parents: 65968
diff changeset
   158
  for (const editor of window.visibleTextEditors) {
65182
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   159
    update_editor(editor)
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   160
  }
65094
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   161
}
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   162
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   163
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   164
/* decoration for document node */
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   165
65135
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   166
type Content = Range[] | DecorationOptions[]
81070
de30087b4ff8 vscode: switched document_decoration map to use strings as keys instead of Uris, because Uri equality check is inconsistent;
Thomas Lindae <thomas.lindae@in.tum.de>
parents: 75262
diff changeset
   167
const document_decorations = new Map<string, Map<string, Content>>()
65135
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   168
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   169
export function close_document(document: TextDocument)
65094
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   170
{
81070
de30087b4ff8 vscode: switched document_decoration map to use strings as keys instead of Uris, because Uri equality check is inconsistent;
Thomas Lindae <thomas.lindae@in.tum.de>
parents: 75262
diff changeset
   171
  document_decorations.delete(document.uri.toString())
65135
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   172
}
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   173
75126
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   174
export function apply_decoration(decorations: Document_Decorations)
65135
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   175
{
75262
ec62c5401522 discontinued isabelle_filesystem (superseded by isabelle_encoding), see also da1108a6d249;
wenzelm
parents: 75234
diff changeset
   176
  const uri = Uri.parse(decorations.uri)
75126
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   177
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   178
  for (const decoration of decorations.entries) {
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   179
    const typ = types.get(decoration.type)
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   180
    if (typ) {
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   181
      const content: DecorationOptions[] = decoration.content.map(opt =>
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   182
        {
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   183
          const r = opt.range
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   184
          return {
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   185
            range: new Range(r[0], r[1], r[2], r[3]),
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   186
            hoverMessage: opt.hover_message
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   187
          }
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   188
        })
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   189
81070
de30087b4ff8 vscode: switched document_decoration map to use strings as keys instead of Uris, because Uri equality check is inconsistent;
Thomas Lindae <thomas.lindae@in.tum.de>
parents: 75262
diff changeset
   190
      const document = document_decorations.get(uri.toString()) || new Map<string, Content>()
75126
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   191
      document.set(decoration.type, content)
81070
de30087b4ff8 vscode: switched document_decoration map to use strings as keys instead of Uris, because Uri equality check is inconsistent;
Thomas Lindae <thomas.lindae@in.tum.de>
parents: 75262
diff changeset
   192
      document_decorations.set(uri.toString(), document)
75126
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   193
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   194
      for (const editor of window.visibleTextEditors) {
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   195
        if (uri.toString === editor.document.uri.toString) {
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   196
          editor.setDecorations(typ, content)
65173
3700be571a01 more compact protocol message;
wenzelm
parents: 65171
diff changeset
   197
        }
65135
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   198
      }
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   199
    }
65094
386d9d487f62 support for decorations;
wenzelm
parents:
diff changeset
   200
  }
65135
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   201
}
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   202
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   203
export function update_editor(editor: TextEditor)
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   204
{
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   205
  if (editor) {
81070
de30087b4ff8 vscode: switched document_decoration map to use strings as keys instead of Uris, because Uri equality check is inconsistent;
Thomas Lindae <thomas.lindae@in.tum.de>
parents: 75262
diff changeset
   206
    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
   207
    if (decorations) {
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65153
diff changeset
   208
      for (const [typ, content] of decorations) {
65182
973b7669e7d9 proper Map operations;
wenzelm
parents: 65181
diff changeset
   209
        editor.setDecorations(types.get(typ), content)
65135
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   210
      }
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   211
    }
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   212
  }
158cba86140f maintain decorations for document (model) and update it for each editor (view);
wenzelm
parents: 65134
diff changeset
   213
}
65233
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   214
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   215
65973
wenzelm
parents: 65969
diff changeset
   216
/* handle document changes */
65233
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   217
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   218
const touched_documents = new Set<TextDocument>()
65974
fd5f80ee2de0 clarified event handling;
wenzelm
parents: 65973
diff changeset
   219
let touched_timer: NodeJS.Timer
65233
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   220
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   221
function update_touched_documents()
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   222
{
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   223
  const touched_editors: TextEditor[] = []
65969
1f93eb5c3d77 tuned imports;
wenzelm
parents: 65968
diff changeset
   224
  for (const editor of window.visibleTextEditors) {
65233
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   225
    if (touched_documents.has(editor.document)) {
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   226
      touched_editors.push(editor)
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   227
    }
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   228
  }
75126
da1108a6d249 various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
wenzelm
parents: 69965
diff changeset
   229
  touched_documents.clear()
65233
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   230
  touched_editors.forEach(update_editor)
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   231
}
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   232
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   233
export function touch_document(document: TextDocument)
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   234
{
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   235
  if (touched_timer) timers.clearTimeout(touched_timer)
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   236
  touched_documents.add(document)
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   237
  touched_timer = timers.setTimeout(update_touched_documents, 1000)
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65201
diff changeset
   238
}