1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
import * as vscode from 'vscode';
import * as lc from 'vscode-languageclient'
import { Server } from './server';
export interface Decoration {
range: lc.Range,
tag: string,
}
export class Highlighter {
private decorations: { [index: string]: vscode.TextEditorDecorationType };
constructor() {
this.decorations = {};
}
removeHighlights() {
for (let tag in this.decorations) {
this.decorations[tag].dispose();
}
this.decorations = {};
}
setHighlights(
editor: vscode.TextEditor,
highlights: Array<Decoration>
) {
// Initialize decorations if necessary
//
// Note: decoration objects need to be kept around so we can dispose them
// if the user disables syntax highlighting
if (Object.keys(this.decorations).length === 0) {
this.initDecorations();
}
let byTag: Map<string, vscode.Range[]> = new Map()
for (let tag in this.decorations) {
byTag.set(tag, [])
}
for (let d of highlights) {
if (!byTag.get(d.tag)) {
console.log(`unknown tag ${d.tag}`)
continue
}
byTag.get(d.tag)!.push(
Server.client.protocol2CodeConverter.asRange(d.range)
)
}
for (let tag of byTag.keys()) {
let dec: vscode.TextEditorDecorationType = this.decorations[tag]
let ranges = byTag.get(tag)!
editor.setDecorations(dec, ranges)
}
}
private initDecorations() {
const decor = (obj: any) => vscode.window.createTextEditorDecorationType({ color: obj })
this.decorations = {
background: decor("#3F3F3F"),
error: vscode.window.createTextEditorDecorationType({
borderColor: "red",
borderStyle: "none none dashed none",
}),
comment: decor("#7F9F7F"),
string: decor("#CC9393"),
keyword: decor("#F0DFAF"),
function: decor("#93E0E3"),
parameter: decor("#94BFF3"),
builtin: decor("#DD6718"),
text: decor("#DCDCCC"),
attribute: decor("#BFEBBF"),
literal: decor("#DFAF8F"),
}
}
}
|
