author | wenzelm |
Wed, 21 Nov 2018 15:19:11 +0100 | |
changeset 69322 | ce6d43af5bcb |
parent 66395 | 14146fb264d8 |
child 71475 | 7a867a38712a |
permissions | -rw-r--r-- |
64605 | 1 |
'use strict'; |
2 |
||
3 |
import * as path from 'path'; |
|
65172 | 4 |
import * as fs from 'fs'; |
65968 | 5 |
import * as library from './library' |
65094 | 6 |
import * as decorations from './decorations'; |
66098 | 7 |
import * as preview_panel from './preview_panel'; |
65201 | 8 |
import * as protocol from './protocol'; |
66098 | 9 |
import * as state_panel from './state_panel'; |
66052
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65987
diff
changeset
|
10 |
import * as symbol from './symbol'; |
66060
b2bfbefd354f
symbol completion that bypasses the LS protocol, and thus observes the range properly;
wenzelm
parents:
66052
diff
changeset
|
11 |
import * as completion from './completion'; |
66216 | 12 |
import { Uri, TextEditor, ViewColumn, Selection, Position, ExtensionContext, workspace, window, |
13 |
commands, languages } from 'vscode'; |
|
66215
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66211
diff
changeset
|
14 |
import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind, |
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66211
diff
changeset
|
15 |
NotificationType } from 'vscode-languageclient'; |
64605 | 16 |
|
17 |
||
65201 | 18 |
let last_caret_update: protocol.Caret_Update = {} |
65180 | 19 |
|
65969 | 20 |
export function activate(context: ExtensionContext) |
64605 | 21 |
{ |
65968 | 22 |
const isabelle_home = library.get_configuration<string>("home") |
23 |
const isabelle_args = library.get_configuration<Array<string>>("args") |
|
24 |
const cygwin_root = library.get_configuration<string>("cygwin_root") |
|
64605 | 25 |
|
65182 | 26 |
|
27 |
/* server */ |
|
28 |
||
65172 | 29 |
if (isabelle_home === "") |
65969 | 30 |
window.showErrorMessage("Missing user settings: isabelle.home") |
64753 | 31 |
else { |
65168 | 32 |
const isabelle_tool = isabelle_home + "/bin/isabelle" |
33 |
const standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"] |
|
65167 | 34 |
|
65168 | 35 |
const server_options: ServerOptions = |
65970 | 36 |
library.platform_is_windows() ? |
65172 | 37 |
{ command: |
38 |
(cygwin_root === "" ? path.join(isabelle_home, "contrib", "cygwin") : cygwin_root) + |
|
39 |
"/bin/bash", |
|
64874
e13ff666af96
enable vscode_unicode_symbols by default, despite asymmetry of input and output;
wenzelm
parents:
64833
diff
changeset
|
40 |
args: ["-l", isabelle_tool, "vscode_server"].concat(standard_args, isabelle_args) } : |
64755 | 41 |
{ command: isabelle_tool, |
64874
e13ff666af96
enable vscode_unicode_symbols by default, despite asymmetry of input and output;
wenzelm
parents:
64833
diff
changeset
|
42 |
args: ["vscode_server"].concat(standard_args, isabelle_args) }; |
65983 | 43 |
const language_client_options: LanguageClientOptions = { |
69322
ce6d43af5bcb
more robust (see https://code.visualstudio.com/docs/extensionAPI/document-selectors);
wenzelm
parents:
66395
diff
changeset
|
44 |
documentSelector: [ |
ce6d43af5bcb
more robust (see https://code.visualstudio.com/docs/extensionAPI/document-selectors);
wenzelm
parents:
66395
diff
changeset
|
45 |
{ language: "isabelle", scheme: "file" }, |
ce6d43af5bcb
more robust (see https://code.visualstudio.com/docs/extensionAPI/document-selectors);
wenzelm
parents:
66395
diff
changeset
|
46 |
{ language: "isabelle-ml", scheme: "file" }, |
ce6d43af5bcb
more robust (see https://code.visualstudio.com/docs/extensionAPI/document-selectors);
wenzelm
parents:
66395
diff
changeset
|
47 |
{ language: "bibtex", scheme: "file" } |
ce6d43af5bcb
more robust (see https://code.visualstudio.com/docs/extensionAPI/document-selectors);
wenzelm
parents:
66395
diff
changeset
|
48 |
] |
64753 | 49 |
}; |
64605 | 50 |
|
65983 | 51 |
const language_client = |
52 |
new LanguageClient("Isabelle", server_options, language_client_options, false) |
|
65094 | 53 |
|
65182 | 54 |
|
65201 | 55 |
/* decorations */ |
56 |
||
66097 | 57 |
decorations.setup(context) |
65975 | 58 |
context.subscriptions.push( |
66097 | 59 |
workspace.onDidChangeConfiguration(() => decorations.setup(context)), |
65975 | 60 |
workspace.onDidChangeTextDocument(event => decorations.touch_document(event.document)), |
61 |
window.onDidChangeActiveTextEditor(decorations.update_editor), |
|
62 |
workspace.onDidCloseTextDocument(decorations.close_document)) |
|
65201 | 63 |
|
65983 | 64 |
language_client.onReady().then(() => |
65 |
language_client.onNotification(protocol.decoration_type, decorations.apply_decoration)) |
|
65201 | 66 |
|
67 |
||
65978 | 68 |
/* caret handling */ |
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65189
diff
changeset
|
69 |
|
65189 | 70 |
function update_caret() |
71 |
{ |
|
65969 | 72 |
const editor = window.activeTextEditor |
65201 | 73 |
let caret_update: protocol.Caret_Update = {} |
65189 | 74 |
if (editor) { |
75 |
const uri = editor.document.uri |
|
76 |
const cursor = editor.selection.active |
|
65972 | 77 |
if (library.is_file(uri) && cursor) |
65189 | 78 |
caret_update = { uri: uri.toString(), line: cursor.line, character: cursor.character } |
79 |
} |
|
80 |
if (last_caret_update !== caret_update) { |
|
65202 | 81 |
if (caret_update.uri) |
65983 | 82 |
language_client.sendNotification(protocol.caret_update_type, caret_update) |
65189 | 83 |
last_caret_update = caret_update |
84 |
} |
|
85 |
} |
|
86 |
||
66215
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66211
diff
changeset
|
87 |
function goto_file(caret_update: protocol.Caret_Update) |
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66211
diff
changeset
|
88 |
{ |
66216 | 89 |
function move_cursor(editor: TextEditor) |
90 |
{ |
|
91 |
const pos = new Position(caret_update.line || 0, caret_update.character || 0) |
|
92 |
editor.selections = [new Selection(pos, pos)] |
|
93 |
} |
|
94 |
||
66215
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66211
diff
changeset
|
95 |
if (caret_update.uri) { |
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66211
diff
changeset
|
96 |
workspace.openTextDocument(Uri.parse(caret_update.uri)).then(document => |
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66211
diff
changeset
|
97 |
{ |
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66211
diff
changeset
|
98 |
const editor = library.find_file_editor(document.uri) |
66216 | 99 |
const column = editor ? editor.viewColumn : ViewColumn.One |
100 |
window.showTextDocument(document, column, !caret_update.focus).then(move_cursor) |
|
66215
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66211
diff
changeset
|
101 |
}) |
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66211
diff
changeset
|
102 |
} |
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66211
diff
changeset
|
103 |
} |
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66211
diff
changeset
|
104 |
|
65983 | 105 |
language_client.onReady().then(() => |
65189 | 106 |
{ |
65975 | 107 |
context.subscriptions.push( |
108 |
window.onDidChangeActiveTextEditor(_ => update_caret()), |
|
109 |
window.onDidChangeTextEditorSelection(_ => update_caret())) |
|
65189 | 110 |
update_caret() |
66215
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66211
diff
changeset
|
111 |
|
9a8b6b86350c
proper hyperlink_command, notably for locate_query;
wenzelm
parents:
66211
diff
changeset
|
112 |
language_client.onNotification(protocol.caret_update_type, goto_file) |
65189 | 113 |
}) |
114 |
||
115 |
||
65978 | 116 |
/* dynamic output */ |
117 |
||
118 |
const dynamic_output = window.createOutputChannel("Isabelle Output") |
|
119 |
context.subscriptions.push(dynamic_output) |
|
120 |
dynamic_output.show(true) |
|
121 |
dynamic_output.hide() |
|
122 |
||
65983 | 123 |
language_client.onReady().then(() => |
65978 | 124 |
{ |
65983 | 125 |
language_client.onNotification(protocol.dynamic_output_type, |
65979 | 126 |
params => { dynamic_output.clear(); dynamic_output.appendLine(params.content) }) |
65978 | 127 |
}) |
128 |
||
129 |
||
66098 | 130 |
/* state panel */ |
66096 | 131 |
|
132 |
context.subscriptions.push( |
|
66098 | 133 |
commands.registerCommand("isabelle.state", uri => state_panel.init(uri)), |
134 |
commands.registerCommand("_isabelle.state-locate", state_panel.locate), |
|
66211 | 135 |
commands.registerCommand("_isabelle.state-update", state_panel.update), |
66395 | 136 |
commands.registerCommand("_isabelle.state-auto-update", state_panel.auto_update), |
137 |
workspace.onDidCloseTextDocument(document => state_panel.exit_uri(document.uri))) |
|
66096 | 138 |
|
66098 | 139 |
language_client.onReady().then(() => state_panel.setup(context, language_client)) |
66096 | 140 |
|
141 |
||
66098 | 142 |
/* preview panel */ |
65958 | 143 |
|
65984
8e6a833da7db
register commands earlier, before prover startup;
wenzelm
parents:
65983
diff
changeset
|
144 |
context.subscriptions.push( |
66098 | 145 |
commands.registerCommand("isabelle.preview", uri => preview_panel.request(uri, false)), |
146 |
commands.registerCommand("isabelle.preview-split", uri => preview_panel.request(uri, true)), |
|
147 |
commands.registerCommand("isabelle.preview-source", preview_panel.source), |
|
148 |
commands.registerCommand("isabelle.preview-update", preview_panel.update)) |
|
65984
8e6a833da7db
register commands earlier, before prover startup;
wenzelm
parents:
65983
diff
changeset
|
149 |
|
66098 | 150 |
language_client.onReady().then(() => preview_panel.setup(context, language_client)) |
65958 | 151 |
|
152 |
||
66052
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65987
diff
changeset
|
153 |
/* Isabelle symbols */ |
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65987
diff
changeset
|
154 |
|
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65987
diff
changeset
|
155 |
language_client.onReady().then(() => |
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65987
diff
changeset
|
156 |
{ |
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65987
diff
changeset
|
157 |
language_client.onNotification(protocol.symbols_type, |
66097 | 158 |
params => symbol.setup(context, params.entries)) |
66052
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65987
diff
changeset
|
159 |
language_client.sendNotification(protocol.symbols_request_type) |
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65987
diff
changeset
|
160 |
}) |
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65987
diff
changeset
|
161 |
|
39eb61b1fa51
provide information about Isabelle symbols within VSCode;
wenzelm
parents:
65987
diff
changeset
|
162 |
|
66060
b2bfbefd354f
symbol completion that bypasses the LS protocol, and thus observes the range properly;
wenzelm
parents:
66052
diff
changeset
|
163 |
/* completion */ |
b2bfbefd354f
symbol completion that bypasses the LS protocol, and thus observes the range properly;
wenzelm
parents:
66052
diff
changeset
|
164 |
|
b2bfbefd354f
symbol completion that bypasses the LS protocol, and thus observes the range properly;
wenzelm
parents:
66052
diff
changeset
|
165 |
const completion_provider = new completion.Completion_Provider |
b2bfbefd354f
symbol completion that bypasses the LS protocol, and thus observes the range properly;
wenzelm
parents:
66052
diff
changeset
|
166 |
for (const mode of ["isabelle", "isabelle-ml"]) { |
b2bfbefd354f
symbol completion that bypasses the LS protocol, and thus observes the range properly;
wenzelm
parents:
66052
diff
changeset
|
167 |
context.subscriptions.push( |
b2bfbefd354f
symbol completion that bypasses the LS protocol, and thus observes the range properly;
wenzelm
parents:
66052
diff
changeset
|
168 |
languages.registerCompletionItemProvider(mode, completion_provider)) |
b2bfbefd354f
symbol completion that bypasses the LS protocol, and thus observes the range properly;
wenzelm
parents:
66052
diff
changeset
|
169 |
} |
b2bfbefd354f
symbol completion that bypasses the LS protocol, and thus observes the range properly;
wenzelm
parents:
66052
diff
changeset
|
170 |
|
66138 | 171 |
|
172 |
/* spell checker */ |
|
173 |
||
174 |
language_client.onReady().then(() => |
|
175 |
{ |
|
176 |
context.subscriptions.push( |
|
177 |
commands.registerCommand("isabelle.include-word", uri => |
|
178 |
language_client.sendNotification(protocol.include_word_type)), |
|
179 |
commands.registerCommand("isabelle.include-word-permanently", uri => |
|
180 |
language_client.sendNotification(protocol.include_word_permanently_type)), |
|
181 |
commands.registerCommand("isabelle.exclude-word", uri => |
|
182 |
language_client.sendNotification(protocol.exclude_word_type)), |
|
183 |
commands.registerCommand("isabelle.exclude-word-permanently", uri => |
|
184 |
language_client.sendNotification(protocol.exclude_word_permanently_type)), |
|
185 |
commands.registerCommand("isabelle.reset-words", uri => |
|
186 |
language_client.sendNotification(protocol.reset_words_type))) |
|
187 |
}) |
|
188 |
||
189 |
||
65182 | 190 |
/* start server */ |
191 |
||
65986 | 192 |
context.subscriptions.push(language_client.start()) |
65094 | 193 |
} |
64605 | 194 |
} |
195 |
||
196 |
export function deactivate() { } |