author | wenzelm |
Sun, 08 Jan 2017 13:08:17 +0100 | |
changeset 64833 | 0f410e3b1d20 |
parent 64756 | 3cc892bd8f0f |
child 64874 | e13ff666af96 |
permissions | -rw-r--r-- |
64605 | 1 |
'use strict'; |
2 |
||
3 |
import * as vscode from 'vscode'; |
|
4 |
import * as path from 'path'; |
|
64755 | 5 |
import * as os from 'os'; |
64605 | 6 |
|
7 |
import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind } |
|
8 |
from 'vscode-languageclient'; |
|
9 |
||
10 |
||
11 |
export function activate(context: vscode.ExtensionContext) |
|
12 |
{ |
|
64755 | 13 |
let is_windows = os.type().startsWith("Windows") |
14 |
||
15 |
let cygwin_root = vscode.workspace.getConfiguration("isabelle").get<string>("cygwin_root"); |
|
64734 | 16 |
let isabelle_home = vscode.workspace.getConfiguration("isabelle").get<string>("home"); |
64743 | 17 |
let isabelle_args = vscode.workspace.getConfiguration("isabelle").get<Array<string>>("args"); |
64605 | 18 |
|
64755 | 19 |
if (is_windows && cygwin_root == "") |
20 |
vscode.window.showErrorMessage("Missing user settings: isabelle.cygwin_root") |
|
21 |
else if (isabelle_home == "") |
|
22 |
vscode.window.showErrorMessage("Missing user settings: isabelle.home") |
|
64753 | 23 |
else { |
64755 | 24 |
let isabelle_tool = isabelle_home.concat("/bin/isabelle") |
25 |
let run = |
|
26 |
is_windows ? |
|
27 |
{ command: cygwin_root.concat("/bin/bash"), |
|
28 |
args: ["-l", isabelle_tool, "vscode_server"].concat(isabelle_args) } : |
|
29 |
{ command: isabelle_tool, |
|
30 |
args: ["vscode_server"].concat(isabelle_args) }; |
|
31 |
||
64756
3cc892bd8f0f
avoid hardwired options: use isabelle.args settings instead;
wenzelm
parents:
64755
diff
changeset
|
32 |
let server_options: ServerOptions = { run: run, debug: run }; |
64753 | 33 |
let client_options: LanguageClientOptions = { |
64833 | 34 |
documentSelector: ["isabelle", "isabelle-ml", "bibtex"] |
64753 | 35 |
}; |
64605 | 36 |
|
64753 | 37 |
let disposable = new LanguageClient("Isabelle", server_options, client_options, false).start(); |
38 |
context.subscriptions.push(disposable); |
|
39 |
} |
|
64605 | 40 |
} |
41 |
||
42 |
export function deactivate() { } |