|
65958
|
1 |
'use strict';
|
|
|
2 |
|
|
65961
|
3 |
import { TextDocumentContentProvider, ExtensionContext, Event, EventEmitter, Uri, Position,
|
|
|
4 |
ViewColumn, workspace, window, commands } from 'vscode'
|
|
65958
|
5 |
|
|
|
6 |
|
|
|
7 |
const uri_scheme = 'isabelle-preview';
|
|
|
8 |
|
|
|
9 |
class Provider implements TextDocumentContentProvider
|
|
|
10 |
{
|
|
65959
|
11 |
constructor() { }
|
|
65958
|
12 |
dispose() { }
|
|
|
13 |
|
|
65961
|
14 |
private emitter = new EventEmitter<Uri>()
|
|
|
15 |
private waiting: boolean = false;
|
|
|
16 |
|
|
|
17 |
get onDidChange(): Event<Uri> { return this.emitter.event }
|
|
|
18 |
|
|
|
19 |
public update(document_uri: Uri)
|
|
65958
|
20 |
{
|
|
65961
|
21 |
if (!this.waiting) {
|
|
|
22 |
this.waiting = true
|
|
|
23 |
setTimeout(() =>
|
|
|
24 |
{
|
|
|
25 |
this.waiting = false
|
|
|
26 |
this.emitter.fire(encode_name(document_uri))
|
|
|
27 |
}, 300)
|
|
|
28 |
}
|
|
|
29 |
}
|
|
|
30 |
|
|
|
31 |
provideTextDocumentContent(preview_uri: Uri): string | Thenable<string>
|
|
|
32 |
{
|
|
|
33 |
const document_uri = decode_name(preview_uri)
|
|
|
34 |
const editor =
|
|
|
35 |
window.visibleTextEditors.find(editor =>
|
|
|
36 |
document_uri.toString() === editor.document.uri.toString())
|
|
65960
|
37 |
return `
|
|
|
38 |
<html>
|
|
|
39 |
<head>
|
|
|
40 |
<meta http-equiv="Content-type" content="text/html; charset=UTF-8">
|
|
|
41 |
</head>
|
|
|
42 |
<body>
|
|
|
43 |
<h1>Isabelle Preview</h1>
|
|
65961
|
44 |
<ul>
|
|
|
45 |
<li><b>file</b> = <code>${document_uri.fsPath}</code></li>` +
|
|
|
46 |
(editor ? `<li><b>line count</b> = ${editor.document.lineCount}</li>` : "") +
|
|
|
47 |
`</ul>
|
|
65960
|
48 |
</body>
|
|
|
49 |
</html>`
|
|
65958
|
50 |
}
|
|
|
51 |
}
|
|
|
52 |
|
|
65961
|
53 |
export function encode_name(document_uri: Uri): Uri
|
|
65958
|
54 |
{
|
|
65961
|
55 |
return Uri.parse(uri_scheme + ":Preview?" + JSON.stringify([document_uri.toString()]))
|
|
65958
|
56 |
}
|
|
|
57 |
|
|
65961
|
58 |
export function decode_name(preview_uri: Uri): Uri
|
|
65958
|
59 |
{
|
|
65961
|
60 |
const [name] = <[string]>JSON.parse(preview_uri.query)
|
|
|
61 |
return Uri.parse(name)
|
|
65959
|
62 |
}
|
|
|
63 |
|
|
65961
|
64 |
function other_column(): ViewColumn
|
|
65959
|
65 |
{
|
|
|
66 |
const active = window.activeTextEditor
|
|
65961
|
67 |
if (!active || active.viewColumn === ViewColumn.Three) return ViewColumn.One
|
|
|
68 |
else if (active.viewColumn === ViewColumn.One) return ViewColumn.Two
|
|
|
69 |
else return ViewColumn.Three
|
|
65958
|
70 |
}
|
|
|
71 |
|
|
|
72 |
export function init(context: ExtensionContext)
|
|
|
73 |
{
|
|
|
74 |
const provider = new Provider()
|
|
65961
|
75 |
context.subscriptions.push(workspace.registerTextDocumentContentProvider(uri_scheme, provider))
|
|
|
76 |
context.subscriptions.push(provider)
|
|
65958
|
77 |
|
|
65961
|
78 |
context.subscriptions.push(
|
|
65958
|
79 |
commands.registerTextEditorCommand("isabelle.preview", editor =>
|
|
|
80 |
{
|
|
65961
|
81 |
const preview_uri = encode_name(editor.document.uri)
|
|
|
82 |
return workspace.openTextDocument(preview_uri).then(doc =>
|
|
|
83 |
commands.executeCommand("vscode.previewHtml", preview_uri, other_column(), "Isabelle Preview"))
|
|
|
84 |
}))
|
|
65958
|
85 |
|
|
65961
|
86 |
context.subscriptions.push(
|
|
|
87 |
workspace.onDidChangeTextDocument(event =>
|
|
|
88 |
{
|
|
|
89 |
if (event.document.languageId === 'isabelle') {
|
|
|
90 |
provider.update(event.document.uri)
|
|
|
91 |
}
|
|
|
92 |
}))
|
|
65958
|
93 |
}
|