author | wenzelm |
Mon, 29 May 2017 15:16:32 +0200 | |
changeset 65958 | 6338355b2a88 |
parent 65233 | e37209c0a42a |
child 65968 | 44e703278dfd |
permissions | -rw-r--r-- |
64605 | 1 |
'use strict'; |
2 |
||
3 |
import * as vscode from 'vscode'; |
|
4 |
import * as path from 'path'; |
|
65172 | 5 |
import * as fs from 'fs'; |
64755 | 6 |
import * as os from 'os'; |
65094 | 7 |
import * as decorations from './decorations'; |
65958 | 8 |
import * as preview from './preview'; |
65201 | 9 |
import * as protocol from './protocol'; |
65165 | 10 |
import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind, NotificationType } |
64605 | 11 |
from 'vscode-languageclient'; |
12 |
||
13 |
||
65180 | 14 |
/* Isabelle configuration */ |
15 |
||
65186 | 16 |
export function get_configuration<T>(name: string): T |
65180 | 17 |
{ |
65186 | 18 |
return vscode.workspace.getConfiguration("isabelle").get<T>(name) |
65180 | 19 |
} |
20 |
||
21 |
export function get_color(color: string, light: boolean): string |
|
22 |
{ |
|
23 |
const config = color + (light ? "_light" : "_dark") + "_color" |
|
65186 | 24 |
return get_configuration<string>(config) |
65180 | 25 |
} |
26 |
||
27 |
||
65201 | 28 |
/* activate extension */ |
65200
1227a68fac7a
more explicit message type: allows body to become empty;
wenzelm
parents:
65191
diff
changeset
|
29 |
|
65201 | 30 |
let last_caret_update: protocol.Caret_Update = {} |
65180 | 31 |
|
64605 | 32 |
export function activate(context: vscode.ExtensionContext) |
33 |
{ |
|
65168 | 34 |
const is_windows = os.type().startsWith("Windows") |
64755 | 35 |
|
65186 | 36 |
const isabelle_home = get_configuration<string>("home") |
37 |
const isabelle_args = get_configuration<Array<string>>("args") |
|
38 |
const cygwin_root = get_configuration<string>("cygwin_root") |
|
64605 | 39 |
|
65182 | 40 |
|
41 |
/* server */ |
|
42 |
||
65172 | 43 |
if (isabelle_home === "") |
64755 | 44 |
vscode.window.showErrorMessage("Missing user settings: isabelle.home") |
64753 | 45 |
else { |
65168 | 46 |
const isabelle_tool = isabelle_home + "/bin/isabelle" |
47 |
const standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"] |
|
65167 | 48 |
|
65168 | 49 |
const server_options: ServerOptions = |
64755 | 50 |
is_windows ? |
65172 | 51 |
{ command: |
52 |
(cygwin_root === "" ? path.join(isabelle_home, "contrib", "cygwin") : cygwin_root) + |
|
53 |
"/bin/bash", |
|
64874
e13ff666af96
enable vscode_unicode_symbols by default, despite asymmetry of input and output;
wenzelm
parents:
64833
diff
changeset
|
54 |
args: ["-l", isabelle_tool, "vscode_server"].concat(standard_args, isabelle_args) } : |
64755 | 55 |
{ command: isabelle_tool, |
64874
e13ff666af96
enable vscode_unicode_symbols by default, despite asymmetry of input and output;
wenzelm
parents:
64833
diff
changeset
|
56 |
args: ["vscode_server"].concat(standard_args, isabelle_args) }; |
65168 | 57 |
const client_options: LanguageClientOptions = { |
64833 | 58 |
documentSelector: ["isabelle", "isabelle-ml", "bibtex"] |
64753 | 59 |
}; |
64605 | 60 |
|
65168 | 61 |
const client = new LanguageClient("Isabelle", server_options, client_options, false) |
65094 | 62 |
|
65182 | 63 |
|
65201 | 64 |
/* decorations */ |
65 |
||
66 |
decorations.init(context) |
|
67 |
vscode.workspace.onDidChangeConfiguration(() => decorations.init(context)) |
|
65233
e37209c0a42a
always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents:
65202
diff
changeset
|
68 |
vscode.workspace.onDidChangeTextDocument(event => decorations.touch_document(event.document)) |
65201 | 69 |
vscode.window.onDidChangeActiveTextEditor(decorations.update_editor) |
70 |
vscode.workspace.onDidCloseTextDocument(decorations.close_document) |
|
71 |
||
72 |
client.onReady().then(() => |
|
73 |
client.onNotification(protocol.decoration_type, decorations.apply_decoration)) |
|
74 |
||
75 |
||
65189 | 76 |
/* caret handling and dynamic output */ |
77 |
||
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65189
diff
changeset
|
78 |
const dynamic_output = vscode.window.createOutputChannel("Isabelle Output") |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65189
diff
changeset
|
79 |
context.subscriptions.push(dynamic_output) |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65189
diff
changeset
|
80 |
dynamic_output.show(true) |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65189
diff
changeset
|
81 |
dynamic_output.hide() |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
65189
diff
changeset
|
82 |
|
65189 | 83 |
function update_caret() |
84 |
{ |
|
85 |
const editor = vscode.window.activeTextEditor |
|
65201 | 86 |
let caret_update: protocol.Caret_Update = {} |
65189 | 87 |
if (editor) { |
88 |
const uri = editor.document.uri |
|
89 |
const cursor = editor.selection.active |
|
90 |
if (uri.scheme === "file" && cursor) |
|
91 |
caret_update = { uri: uri.toString(), line: cursor.line, character: cursor.character } |
|
92 |
} |
|
93 |
if (last_caret_update !== caret_update) { |
|
65202 | 94 |
if (caret_update.uri) |
95 |
client.sendNotification(protocol.caret_update_type, caret_update) |
|
65189 | 96 |
last_caret_update = caret_update |
97 |
} |
|
98 |
} |
|
99 |
||
100 |
client.onReady().then(() => |
|
101 |
{ |
|
65201 | 102 |
client.onNotification(protocol.dynamic_output_type, |
65200
1227a68fac7a
more explicit message type: allows body to become empty;
wenzelm
parents:
65191
diff
changeset
|
103 |
params => { dynamic_output.clear(); dynamic_output.appendLine(params.body) }) |
65189 | 104 |
vscode.window.onDidChangeActiveTextEditor(_ => update_caret()) |
105 |
vscode.window.onDidChangeTextEditorSelection(_ => update_caret()) |
|
106 |
update_caret() |
|
107 |
}) |
|
108 |
||
109 |
||
65958 | 110 |
/* preview */ |
111 |
||
112 |
preview.init(context) |
|
113 |
||
114 |
||
65182 | 115 |
/* start server */ |
116 |
||
65094 | 117 |
context.subscriptions.push(client.start()); |
118 |
} |
|
64605 | 119 |
} |
120 |
||
121 |
export function deactivate() { } |