1 'use strict'; |
1 'use strict'; |
2 |
2 |
3 import * as library from './library' |
3 import * as library from './library' |
4 import * as protocol from './protocol' |
4 import * as protocol from './protocol' |
5 import { Content_Provider } from './content_provider' |
5 import { Content_Provider } from './content_provider' |
6 import { LanguageClient } from 'vscode-languageclient'; |
6 import { LanguageClient, VersionedTextDocumentIdentifier } from 'vscode-languageclient'; |
7 import { Uri, ExtensionContext, workspace, commands, window } from 'vscode' |
7 import { Uri, ExtensionContext, workspace, commands, window, Webview, WebviewPanel } from 'vscode' |
8 |
8 |
9 |
9 |
10 /* HTML content */ |
10 /* HTML content */ |
11 |
11 |
12 const content_provider = new Content_Provider("isabelle-state") |
12 const content_provider = new Content_Provider("isabelle-state") |
32 |
32 |
33 export function setup(context: ExtensionContext, client: LanguageClient) |
33 export function setup(context: ExtensionContext, client: LanguageClient) |
34 { |
34 { |
35 context.subscriptions.push(content_provider.register()) |
35 context.subscriptions.push(content_provider.register()) |
36 |
36 |
|
37 var panel: WebviewPanel |
37 language_client = client |
38 language_client = client |
38 language_client.onNotification(protocol.state_output_type, params => |
39 language_client.onNotification(protocol.state_output_type, params => |
39 { |
40 { |
40 const uri = encode_state(params.id) |
41 const uri = encode_state(params.id) |
41 if (uri) { |
42 if (!panel) { |
42 content_provider.set_content(uri, params.content) |
43 const column = library.adjacent_editor_column(window.activeTextEditor, true) |
43 content_provider.update(uri) |
44 panel = window.createWebviewPanel( |
44 |
45 uri.fsPath, |
45 const existing_document = |
46 "State", |
46 workspace.textDocuments.find(document => |
47 column, |
47 document.uri.scheme === uri.scheme && |
48 { |
48 document.uri.fragment === uri.fragment) |
49 enableScripts: true, |
49 if (!existing_document) { |
50 retainContextWhenHidden: true |
50 const column = library.adjacent_editor_column(window.activeTextEditor, true) |
51 } |
51 commands.executeCommand("vscode.previewHtml", uri, column, "State") |
52 ); |
52 } |
|
53 } |
53 } |
|
54 panel.webview.html = params.content; |
54 }) |
55 }) |
55 } |
56 } |
56 |
57 |
57 |
58 |
58 /* commands */ |
59 /* commands */ |