| author | wenzelm |
| Wed, 31 May 2017 20:13:05 +0200 | |
| changeset 65985 | 1be7135917a6 |
| parent 65984 | 8e6a833da7db |
| child 65986 | d2b2f08533c5 |
| permissions | -rw-r--r-- |
| 65958 | 1 |
'use strict'; |
2 |
||
| 65974 | 3 |
import * as timers from 'timers' |
| 65983 | 4 |
import { ViewColumn, TextDocument, TextEditor, TextDocumentContentProvider,
|
5 |
ExtensionContext, Event, EventEmitter, Uri, Position, workspace, |
|
6 |
window, commands } from 'vscode' |
|
7 |
import { LanguageClient } from 'vscode-languageclient';
|
|
| 65966 | 8 |
import * as library from './library' |
| 65983 | 9 |
import * as protocol from './protocol'; |
10 |
||
11 |
||
12 |
/* Uri information */ |
|
13 |
||
14 |
const preview_uri_template = Uri.parse("isabelle-preview:Preview")
|
|
15 |
const preview_uri_scheme = preview_uri_template.scheme |
|
16 |
||
17 |
function encode_preview(document_uri: Uri | undefined): Uri | undefined |
|
18 |
{
|
|
19 |
if (document_uri && library.is_file(document_uri)) {
|
|
20 |
return preview_uri_template.with({ query: document_uri.fsPath })
|
|
21 |
} |
|
22 |
else undefined |
|
23 |
} |
|
24 |
||
25 |
function decode_preview(preview_uri: Uri | undefined): Uri | undefined |
|
26 |
{
|
|
27 |
if (preview_uri && preview_uri.scheme === preview_uri_scheme) {
|
|
28 |
return Uri.file(preview_uri.query) |
|
29 |
} |
|
30 |
else undefined |
|
31 |
} |
|
| 65958 | 32 |
|
33 |
||
|
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65974
diff
changeset
|
34 |
/* HTML content */ |
| 65971 | 35 |
|
| 65983 | 36 |
const preview_content = new Map<string, string>() |
| 65958 | 37 |
|
|
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65974
diff
changeset
|
38 |
const default_preview_content = |
|
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65974
diff
changeset
|
39 |
`<html> |
|
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65974
diff
changeset
|
40 |
<head> |
|
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65974
diff
changeset
|
41 |
<meta http-equiv="Content-type" content="text/html; charset=UTF-8"> |
|
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65974
diff
changeset
|
42 |
</head> |
|
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65974
diff
changeset
|
43 |
<body> |
|
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65974
diff
changeset
|
44 |
<h1>Isabelle Preview</h1> |
|
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65974
diff
changeset
|
45 |
</body> |
|
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
65974
diff
changeset
|
46 |
</html>` |
| 65971 | 47 |
|
|
65984
8e6a833da7db
register commands earlier, before prover startup;
wenzelm
parents:
65983
diff
changeset
|
48 |
class Content_Provider implements TextDocumentContentProvider |
| 65958 | 49 |
{
|
50 |
dispose() { }
|
|
51 |
||
| 65961 | 52 |
private emitter = new EventEmitter<Uri>() |
| 65983 | 53 |
public update(preview_uri: Uri) { this.emitter.fire(preview_uri) }
|
| 65961 | 54 |
get onDidChange(): Event<Uri> { return this.emitter.event }
|
55 |
||
| 65983 | 56 |
provideTextDocumentContent(preview_uri: Uri): string |
57 |
{
|
|
58 |
return preview_content.get(preview_uri.toString()) || default_preview_content |
|
59 |
} |
|
| 65958 | 60 |
} |
61 |
||
62 |
||
| 65971 | 63 |
/* init */ |
| 65959 | 64 |
|
| 65983 | 65 |
let language_client: LanguageClient |
|
65984
8e6a833da7db
register commands earlier, before prover startup;
wenzelm
parents:
65983
diff
changeset
|
66 |
let content_provider: Content_Provider |
| 65974 | 67 |
|
| 65983 | 68 |
export function init(context: ExtensionContext, client: LanguageClient) |
| 65958 | 69 |
{
|
| 65983 | 70 |
language_client = client |
71 |
||
|
65984
8e6a833da7db
register commands earlier, before prover startup;
wenzelm
parents:
65983
diff
changeset
|
72 |
content_provider = new Content_Provider() |
| 65983 | 73 |
context.subscriptions.push( |
|
65984
8e6a833da7db
register commands earlier, before prover startup;
wenzelm
parents:
65983
diff
changeset
|
74 |
workspace.registerTextDocumentContentProvider(preview_uri_scheme, content_provider), |
|
8e6a833da7db
register commands earlier, before prover startup;
wenzelm
parents:
65983
diff
changeset
|
75 |
content_provider) |
| 65983 | 76 |
|
77 |
language_client.onNotification(protocol.preview_response_type, |
|
78 |
params => show_preview(Uri.parse(params.uri), params.column, params.label, params.content)) |
|
79 |
} |
|
80 |
||
81 |
||
82 |
/* commands */ |
|
83 |
||
| 65985 | 84 |
function preview_column(split: boolean): ViewColumn |
| 65983 | 85 |
{
|
86 |
const active_editor = window.activeTextEditor |
|
87 |
||
88 |
if (!active_editor) return ViewColumn.One |
|
| 65985 | 89 |
else if (!split) return active_editor.viewColumn |
| 65983 | 90 |
else if (active_editor.viewColumn === ViewColumn.One) return ViewColumn.Two |
91 |
else return ViewColumn.Three |
|
| 65974 | 92 |
} |
| 65983 | 93 |
|
| 65985 | 94 |
export function request_preview(uri?: Uri, split: boolean = false) |
| 65983 | 95 |
{
|
96 |
const document_uri = uri || window.activeTextEditor.document.uri |
|
97 |
const preview_uri = encode_preview(document_uri) |
|
|
65984
8e6a833da7db
register commands earlier, before prover startup;
wenzelm
parents:
65983
diff
changeset
|
98 |
if (preview_uri && language_client) {
|
| 65983 | 99 |
language_client.sendNotification(protocol.preview_request_type, |
| 65985 | 100 |
{uri: document_uri.toString(), column: preview_column(split) })
|
| 65983 | 101 |
} |
102 |
} |
|
103 |
||
|
65984
8e6a833da7db
register commands earlier, before prover startup;
wenzelm
parents:
65983
diff
changeset
|
104 |
export function show_preview(document_uri: Uri, column: ViewColumn, label: string, content: string) |
| 65983 | 105 |
{
|
106 |
const preview_uri = encode_preview(document_uri) |
|
|
65984
8e6a833da7db
register commands earlier, before prover startup;
wenzelm
parents:
65983
diff
changeset
|
107 |
if (preview_uri && content_provider) {
|
| 65983 | 108 |
preview_content.set(preview_uri.toString(), content) |
109 |
commands.executeCommand("vscode.previewHtml", preview_uri, column, label)
|
|
110 |
} |
|
111 |
} |
|
112 |
||
|
65984
8e6a833da7db
register commands earlier, before prover startup;
wenzelm
parents:
65983
diff
changeset
|
113 |
export function show_source(preview_uri: Uri) |
| 65983 | 114 |
{
|
115 |
const document_uri = decode_preview(preview_uri) |
|
116 |
if (document_uri) {
|
|
117 |
const editor = |
|
118 |
window.visibleTextEditors.find(editor => |
|
119 |
editor.document.uri.scheme === document_uri.scheme && |
|
120 |
editor.document.uri.fsPath === document_uri.fsPath) |
|
121 |
if (editor) window.showTextDocument(editor.document, editor.viewColumn) |
|
122 |
else workspace.openTextDocument(document_uri).then(window.showTextDocument) |
|
123 |
} |
|
124 |
else commands.executeCommand("workbench.action.navigateBack")
|
|
125 |
} |