5 TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode' |
5 TextDocument, TextEditor, TextEditorDecorationType, ExtensionContext, Uri } from 'vscode' |
6 import { get_color } from './extension' |
6 import { get_color } from './extension' |
7 |
7 |
8 |
8 |
9 /* known decoration types */ |
9 /* known decoration types */ |
10 |
|
11 export const types = new Map<string, TextEditorDecorationType>() |
|
12 |
10 |
13 const background_colors = [ |
11 const background_colors = [ |
14 "unprocessed1", |
12 "unprocessed1", |
15 "running1", |
13 "running1", |
16 "bad", |
14 "bad", |
86 return decoration( |
89 return decoration( |
87 { light: { border: border + get_color(color, true) }, |
90 { light: { border: border + get_color(color, true) }, |
88 dark: { border: border + get_color(color, false) } }) |
91 dark: { border: border + get_color(color, false) } }) |
89 } |
92 } |
90 |
93 |
91 types.clear |
94 |
|
95 /* reset */ |
|
96 |
|
97 types.forEach(typ => |
|
98 { |
|
99 for (const editor of vscode.window.visibleTextEditors) { |
|
100 editor.setDecorations(typ, []) |
|
101 } |
|
102 const i = context.subscriptions.indexOf(typ) |
|
103 if (i >= 0) context.subscriptions.splice(i, 1) |
|
104 typ.dispose() |
|
105 }) |
|
106 types.clear() |
|
107 |
|
108 |
|
109 /* init */ |
|
110 |
92 for (const color of background_colors) { |
111 for (const color of background_colors) { |
93 types["background_" + color] = background(color) |
112 types.set("background_" + color, background(color)) |
94 } |
113 } |
95 for (const color of foreground_colors) { |
114 for (const color of foreground_colors) { |
96 types["foreground_" + color] = background(color) // approximation |
115 types.set("foreground_" + color, background(color)) // approximation |
97 } |
116 } |
98 for (const color of dotted_colors) { |
117 for (const color of dotted_colors) { |
99 types["dotted_" + color] = bottom_border("2px", "dotted", color) |
118 types.set("dotted_" + color, bottom_border("2px", "dotted", color)) |
100 } |
119 } |
101 for (const color of text_colors) { |
120 for (const color of text_colors) { |
102 types["text_" + color] = text_color(color) |
121 types.set("text_" + color, text_color(color)) |
103 } |
122 } |
104 types["spell_checker"] = bottom_border("1px", "solid", "spell_checker") |
123 types.set("spell_checker", bottom_border("1px", "solid", "spell_checker")) |
|
124 |
|
125 |
|
126 /* update editors */ |
|
127 |
|
128 for (const editor of vscode.window.visibleTextEditors) { |
|
129 update_editor(editor) |
|
130 } |
105 } |
131 } |
106 |
132 |
107 |
133 |
108 /* decoration for document node */ |
134 /* decoration for document node */ |
109 |
135 |
127 document_decorations.delete(document.uri.toString()) |
153 document_decorations.delete(document.uri.toString()) |
128 } |
154 } |
129 |
155 |
130 export function apply_decoration(decoration: Decoration) |
156 export function apply_decoration(decoration: Decoration) |
131 { |
157 { |
132 const typ = types[decoration.type] |
158 const typ = types.get(decoration.type) |
133 if (typ) { |
159 if (typ) { |
134 const uri = Uri.parse(decoration.uri).toString() |
160 const uri = Uri.parse(decoration.uri).toString() |
135 const content: DecorationOptions[] = decoration.content.map(opt => |
161 const content: DecorationOptions[] = decoration.content.map(opt => |
136 { |
162 { |
137 const r = opt.range |
163 const r = opt.range |