equal
deleted
inserted
replaced
33 |
33 |
34 const isabelle_home = get_configuration().get<string>("home") |
34 const isabelle_home = get_configuration().get<string>("home") |
35 const isabelle_args = get_configuration().get<Array<string>>("args") |
35 const isabelle_args = get_configuration().get<Array<string>>("args") |
36 const cygwin_root = get_configuration().get<string>("cygwin_root") |
36 const cygwin_root = get_configuration().get<string>("cygwin_root") |
37 |
37 |
|
38 |
|
39 /* server */ |
|
40 |
38 if (isabelle_home === "") |
41 if (isabelle_home === "") |
39 vscode.window.showErrorMessage("Missing user settings: isabelle.home") |
42 vscode.window.showErrorMessage("Missing user settings: isabelle.home") |
40 else { |
43 else { |
41 const isabelle_tool = isabelle_home + "/bin/isabelle" |
44 const isabelle_tool = isabelle_home + "/bin/isabelle" |
42 const standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"] |
45 const standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"] |
53 documentSelector: ["isabelle", "isabelle-ml", "bibtex"] |
56 documentSelector: ["isabelle", "isabelle-ml", "bibtex"] |
54 }; |
57 }; |
55 |
58 |
56 const client = new LanguageClient("Isabelle", server_options, client_options, false) |
59 const client = new LanguageClient("Isabelle", server_options, client_options, false) |
57 |
60 |
|
61 |
|
62 /* decorations */ |
|
63 |
58 decorations.init(context) |
64 decorations.init(context) |
|
65 vscode.workspace.onDidChangeConfiguration(() => decorations.init(context)) |
59 vscode.window.onDidChangeActiveTextEditor(decorations.update_editor) |
66 vscode.window.onDidChangeActiveTextEditor(decorations.update_editor) |
60 vscode.workspace.onDidCloseTextDocument(decorations.close_document) |
67 vscode.workspace.onDidCloseTextDocument(decorations.close_document) |
|
68 |
61 client.onReady().then(() => |
69 client.onReady().then(() => |
62 client.onNotification( |
70 client.onNotification( |
63 new NotificationType<Decoration, void>("PIDE/decoration"), decorations.apply_decoration)) |
71 new NotificationType<Decoration, void>("PIDE/decoration"), decorations.apply_decoration)) |
|
72 |
|
73 |
|
74 /* start server */ |
64 |
75 |
65 context.subscriptions.push(client.start()); |
76 context.subscriptions.push(client.start()); |
66 } |
77 } |
67 } |
78 } |
68 |
79 |