--- a/src/Tools/VSCode/extension/src/decorations.ts Thu Mar 09 21:22:01 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts Thu Mar 09 21:25:01 2017 +0100
@@ -96,16 +96,16 @@
}
types.clear
- for (let color of background_colors) {
+ for (const color of background_colors) {
types["background_" + color] = background(color)
}
- for (let color of foreground_colors) {
+ for (const color of foreground_colors) {
types["foreground_" + color] = background(color) // approximation
}
- for (let color of dotted_colors) {
+ for (const color of dotted_colors) {
types["dotted_" + color] = bottom_border("2px", "dotted", color)
}
- for (let color of text_colors) {
+ for (const color of text_colors) {
types["text_" + color] = text_color(color)
}
types["spell_checker"] = bottom_border("1px", "solid", "spell_checker")
@@ -140,11 +140,11 @@
content: decoration0.content
}
- let document = document_decorations.get(decoration.uri) || new Map<string, Content>()
+ const document = document_decorations.get(decoration.uri) || new Map<string, Content>()
document.set(decoration.type, decoration.content)
document_decorations.set(decoration.uri, document)
- for (let editor of vscode.window.visibleTextEditors) {
+ for (const editor of vscode.window.visibleTextEditors) {
if (decoration.uri == editor.document.uri.toString()) {
editor.setDecorations(typ, decoration.content)
}
@@ -155,9 +155,9 @@
export function update_editor(editor: TextEditor)
{
if (editor) {
- let decorations = document_decorations.get(editor.document.uri.toString())
+ const decorations = document_decorations.get(editor.document.uri.toString())
if (decorations) {
- for (let [typ, content] of decorations) {
+ for (const [typ, content] of decorations) {
editor.setDecorations(types[typ], content)
}
}
--- a/src/Tools/VSCode/extension/src/extension.ts Thu Mar 09 21:22:01 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts Thu Mar 09 21:25:01 2017 +0100
@@ -11,31 +11,31 @@
export function activate(context: vscode.ExtensionContext)
{
- let is_windows = os.type().startsWith("Windows")
+ const is_windows = os.type().startsWith("Windows")
- let cygwin_root = vscode.workspace.getConfiguration("isabelle").get<string>("cygwin_root");
- let isabelle_home = vscode.workspace.getConfiguration("isabelle").get<string>("home");
- let isabelle_args = vscode.workspace.getConfiguration("isabelle").get<Array<string>>("args");
+ const cygwin_root = vscode.workspace.getConfiguration("isabelle").get<string>("cygwin_root");
+ const isabelle_home = vscode.workspace.getConfiguration("isabelle").get<string>("home");
+ const isabelle_args = vscode.workspace.getConfiguration("isabelle").get<Array<string>>("args");
if (is_windows && cygwin_root == "")
vscode.window.showErrorMessage("Missing user settings: isabelle.cygwin_root")
else if (isabelle_home == "")
vscode.window.showErrorMessage("Missing user settings: isabelle.home")
else {
- let isabelle_tool = isabelle_home + "/bin/isabelle"
- let standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"]
+ const isabelle_tool = isabelle_home + "/bin/isabelle"
+ const standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"]
- let server_options: ServerOptions =
+ const server_options: ServerOptions =
is_windows ?
{ command: cygwin_root + "/bin/bash",
args: ["-l", isabelle_tool, "vscode_server"].concat(standard_args, isabelle_args) } :
{ command: isabelle_tool,
args: ["vscode_server"].concat(standard_args, isabelle_args) };
- let client_options: LanguageClientOptions = {
+ const client_options: LanguageClientOptions = {
documentSelector: ["isabelle", "isabelle-ml", "bibtex"]
};
- let client = new LanguageClient("Isabelle", server_options, client_options, false)
+ const client = new LanguageClient("Isabelle", server_options, client_options, false)
decorations.init(context)
vscode.window.onDidChangeActiveTextEditor(decorations.update_editor)