author | wenzelm |
Wed, 31 May 2017 20:43:59 +0200 | |
changeset 65987 | 44e44bfc738a |
parent 65986 | d2b2f08533c5 |
child 66052 | 39eb61b1fa51 |
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'; |
65958 | 7 |
import * as preview from './preview'; |
65201 | 8 |
import * as protocol from './protocol'; |
65984
8e6a833da7db
register commands earlier, before prover startup;
wenzelm
parents:
65983
diff
changeset
|
9 |
import { ExtensionContext, workspace, window, commands } from 'vscode'; |
65165 | 10 |
import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind, NotificationType } |
64605 | 11 |
from 'vscode-languageclient'; |
12 |
||
13 |
||
65201 | 14 |
let last_caret_update: protocol.Caret_Update = {} |
65180 | 15 |
|
65969 | 16 |
export function activate(context: ExtensionContext) |
64605 | 17 |
{ |
65968 | 18 |
const isabelle_home = library.get_configuration<string>("home") |
19 |
const isabelle_args = library.get_configuration<Array<string>>("args") |
|
20 |
const cygwin_root = library.get_configuration<string>("cygwin_root") |
|
64605 | 21 |
|
65182 | 22 |
|
23 |
/* server */ |
|
24 |
||
65172 | 25 |
if (isabelle_home === "") |
65969 | 26 |
window.showErrorMessage("Missing user settings: isabelle.home") |
64753 | 27 |
else { |
65168 | 28 |
const isabelle_tool = isabelle_home + "/bin/isabelle" |
29 |
const standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"] |
|
65167 | 30 |
|
65168 | 31 |
const server_options: ServerOptions = |
65970 | 32 |
library.platform_is_windows() ? |
65172 | 33 |
{ command: |
34 |
(cygwin_root === "" ? path.join(isabelle_home, "contrib", "cygwin") : cygwin_root) + |
|
35 |
"/bin/bash", |
|
64874
e13ff666af96
enable vscode_unicode_symbols by default, despite asymmetry of input and output;
wenzelm
parents:
64833
diff
changeset
|
36 |
args: ["-l", isabelle_tool, "vscode_server"].concat(standard_args, isabelle_args) } : |
64755 | 37 |
{ command: isabelle_tool, |
64874
e13ff666af96
enable vscode_unicode_symbols by default, despite asymmetry of input and output;
wenzelm
parents:
64833
diff
changeset
|
38 |
args: ["vscode_server"].concat(standard_args, isabelle_args) }; |
65983 | 39 |
const language_client_options: LanguageClientOptions = { |
64833 | 40 |
documentSelector: ["isabelle", "isabelle-ml", "bibtex"] |
64753 | 41 |
}; |
64605 | 42 |
|
65983 | 43 |
const language_client = |
44 |
new LanguageClient("Isabelle", server_options, language_client_options, false) |
|
65094 | 45 |
|
65182 | 46 |
|
65201 | 47 |
/* decorations */ |
48 |
||
49 |
decorations.init(context) |
|
65975 | 50 |
context.subscriptions.push( |
51 |
workspace.onDidChangeConfiguration(() => decorations.init(context)), |
|
52 |
workspace.onDidChangeTextDocument(event => decorations.touch_document(event.document)), |
|
53 |
window.onDidChangeActiveTextEditor(decorations.update_editor), |
|
54 |
workspace.onDidCloseTextDocument(decorations.close_document)) |
|
65201 | 55 |
|
65983 | 56 |
language_client.onReady().then(() => |
57 |
language_client.onNotification(protocol.decoration_type, decorations.apply_decoration)) |
|
65201 | 58 |
|
59 |
||
65978 | 60 |
/* caret handling */ |
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65189
diff
changeset
|
61 |
|
65189 | 62 |
function update_caret() |
63 |
{ |
|
65969 | 64 |
const editor = window.activeTextEditor |
65201 | 65 |
let caret_update: protocol.Caret_Update = {} |
65189 | 66 |
if (editor) { |
67 |
const uri = editor.document.uri |
|
68 |
const cursor = editor.selection.active |
|
65972 | 69 |
if (library.is_file(uri) && cursor) |
65189 | 70 |
caret_update = { uri: uri.toString(), line: cursor.line, character: cursor.character } |
71 |
} |
|
72 |
if (last_caret_update !== caret_update) { |
|
65202 | 73 |
if (caret_update.uri) |
65983 | 74 |
language_client.sendNotification(protocol.caret_update_type, caret_update) |
65189 | 75 |
last_caret_update = caret_update |
76 |
} |
|
77 |
} |
|
78 |
||
65983 | 79 |
language_client.onReady().then(() => |
65189 | 80 |
{ |
65975 | 81 |
context.subscriptions.push( |
82 |
window.onDidChangeActiveTextEditor(_ => update_caret()), |
|
83 |
window.onDidChangeTextEditorSelection(_ => update_caret())) |
|
65189 | 84 |
update_caret() |
85 |
}) |
|
86 |
||
87 |
||
65978 | 88 |
/* dynamic output */ |
89 |
||
90 |
const dynamic_output = window.createOutputChannel("Isabelle Output") |
|
91 |
context.subscriptions.push(dynamic_output) |
|
92 |
dynamic_output.show(true) |
|
93 |
dynamic_output.hide() |
|
94 |
||
65983 | 95 |
language_client.onReady().then(() => |
65978 | 96 |
{ |
65983 | 97 |
language_client.onNotification(protocol.dynamic_output_type, |
65979 | 98 |
params => { dynamic_output.clear(); dynamic_output.appendLine(params.content) }) |
65978 | 99 |
}) |
100 |
||
101 |
||
65983 | 102 |
/* preview */ |
65958 | 103 |
|
65984
8e6a833da7db
register commands earlier, before prover startup;
wenzelm
parents:
65983
diff
changeset
|
104 |
context.subscriptions.push( |
65987 | 105 |
commands.registerCommand("isabelle.preview", uri => preview.request(uri, false)), |
106 |
commands.registerCommand("isabelle.preview-split", uri => preview.request(uri, true)), |
|
107 |
commands.registerCommand("isabelle.preview-source", preview.source), |
|
108 |
commands.registerCommand("isabelle.preview-update", preview.update)) |
|
65984
8e6a833da7db
register commands earlier, before prover startup;
wenzelm
parents:
65983
diff
changeset
|
109 |
|
65983 | 110 |
language_client.onReady().then(() => preview.init(context, language_client)) |
65958 | 111 |
|
112 |
||
65182 | 113 |
/* start server */ |
114 |
||
65986 | 115 |
context.subscriptions.push(language_client.start()) |
65094 | 116 |
} |
64605 | 117 |
} |
118 |
||
119 |
export function deactivate() { } |