diff options
author | Pascal Hertleif <[email protected]> | 2019-05-27 10:26:15 +0100 |
---|---|---|
committer | Pascal Hertleif <[email protected]> | 2019-05-27 10:44:46 +0100 |
commit | 1e6ba1901550fb1610a1a464c48ec358cd3c339c (patch) | |
tree | 60ff1f4a42f8ef297c07d5716af67e3057c8e1bd /editors/code/src/highlighting.ts | |
parent | 4ac338b608bb40c5126d019db63232e7834914c2 (diff) |
Make rainbows optional
Diffstat (limited to 'editors/code/src/highlighting.ts')
-rw-r--r-- | editors/code/src/highlighting.ts | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/editors/code/src/highlighting.ts b/editors/code/src/highlighting.ts index 4597db08f..52a0bd4bb 100644 --- a/editors/code/src/highlighting.ts +++ b/editors/code/src/highlighting.ts | |||
@@ -7,7 +7,7 @@ import { Server } from './server'; | |||
7 | export interface Decoration { | 7 | export interface Decoration { |
8 | range: lc.Range; | 8 | range: lc.Range; |
9 | tag: string; | 9 | tag: string; |
10 | id?: string; | 10 | bindingHash?: string; |
11 | } | 11 | } |
12 | 12 | ||
13 | // Based on this HSL-based color generator: https://gist.github.com/bendc/76c48ce53299e6078a76 | 13 | // Based on this HSL-based color generator: https://gist.github.com/bendc/76c48ce53299e6078a76 |
@@ -92,6 +92,7 @@ export class Highlighter { | |||
92 | 92 | ||
93 | const byTag: Map<string, vscode.Range[]> = new Map(); | 93 | const byTag: Map<string, vscode.Range[]> = new Map(); |
94 | const colorfulIdents: Map<string, vscode.Range[]> = new Map(); | 94 | const colorfulIdents: Map<string, vscode.Range[]> = new Map(); |
95 | const rainbowTime = Server.config.rainbowHighlightingOn; | ||
95 | 96 | ||
96 | for (const tag of this.decorations.keys()) { | 97 | for (const tag of this.decorations.keys()) { |
97 | byTag.set(tag, []); | 98 | byTag.set(tag, []); |
@@ -102,12 +103,12 @@ export class Highlighter { | |||
102 | continue; | 103 | continue; |
103 | } | 104 | } |
104 | 105 | ||
105 | if (d.id) { | 106 | if (rainbowTime && d.bindingHash) { |
106 | if (!colorfulIdents.has(d.id)) { | 107 | if (!colorfulIdents.has(d.bindingHash)) { |
107 | colorfulIdents.set(d.id, []); | 108 | colorfulIdents.set(d.bindingHash, []); |
108 | } | 109 | } |
109 | colorfulIdents | 110 | colorfulIdents |
110 | .get(d.id)! | 111 | .get(d.bindingHash)! |
111 | .push( | 112 | .push( |
112 | Server.client.protocol2CodeConverter.asRange(d.range) | 113 | Server.client.protocol2CodeConverter.asRange(d.range) |
113 | ); | 114 | ); |