--- a/src/Tools/VSCode/extension/src/decorations.ts Sat Mar 11 12:12:55 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts Sat Mar 11 12:24:54 2017 +0100
@@ -35,6 +35,7 @@
]
const text_colors = [
+ "main",
"keyword1",
"keyword2",
"keyword3",