|
65958
|
1 |
'use strict';
|
|
|
2 |
|
|
65959
|
3 |
import { TextDocumentContentProvider, ExtensionContext, Uri, Position, ViewColumn,
|
|
65958
|
4 |
workspace, window, commands } from 'vscode'
|
|
|
5 |
|
|
|
6 |
|
|
|
7 |
const uri_scheme = 'isabelle-preview';
|
|
|
8 |
|
|
|
9 |
class Provider implements TextDocumentContentProvider
|
|
|
10 |
{
|
|
65959
|
11 |
constructor() { }
|
|
65958
|
12 |
|
|
|
13 |
dispose() { }
|
|
|
14 |
|
|
|
15 |
provideTextDocumentContent(uri: Uri): string | Thenable<string>
|
|
|
16 |
{
|
|
|
17 |
const [name, pos] = decode_location(uri)
|
|
65960
|
18 |
return `
|
|
|
19 |
<html>
|
|
|
20 |
<head>
|
|
|
21 |
<meta http-equiv="Content-type" content="text/html; charset=UTF-8">
|
|
|
22 |
</head>
|
|
|
23 |
<body>
|
|
|
24 |
<h1>Isabelle Preview</h1>
|
|
|
25 |
<p>${JSON.stringify([name, pos])}</p>
|
|
|
26 |
</body>
|
|
|
27 |
</html>`
|
|
65958
|
28 |
}
|
|
|
29 |
}
|
|
|
30 |
|
|
|
31 |
export function encode_location(uri: Uri, pos: Position): Uri
|
|
|
32 |
{
|
|
|
33 |
const query = JSON.stringify([uri.toString(), pos.line, pos.character])
|
|
|
34 |
return Uri.parse(uri_scheme + ":Preview?" + query)
|
|
|
35 |
}
|
|
|
36 |
|
|
|
37 |
export function decode_location(uri: Uri): [Uri, Position]
|
|
|
38 |
{
|
|
65959
|
39 |
let [name, line, character] = <[string, number, number]>JSON.parse(uri.query)
|
|
|
40 |
return [Uri.parse(name), new Position(line, character)]
|
|
|
41 |
}
|
|
|
42 |
|
|
|
43 |
function view_column(side_by_side: boolean = true): ViewColumn | undefined
|
|
|
44 |
{
|
|
|
45 |
const active = window.activeTextEditor
|
|
|
46 |
if (!active) { return ViewColumn.One }
|
|
|
47 |
if (!side_by_side) { return active.viewColumn }
|
|
|
48 |
|
|
|
49 |
if (active.viewColumn == ViewColumn.One) return ViewColumn.Two
|
|
|
50 |
else if (active.viewColumn == ViewColumn.Two) return ViewColumn.Three
|
|
|
51 |
else return ViewColumn.One
|
|
65958
|
52 |
}
|
|
|
53 |
|
|
|
54 |
export function init(context: ExtensionContext)
|
|
|
55 |
{
|
|
|
56 |
const provider = new Provider()
|
|
|
57 |
|
|
|
58 |
const provider_registration =
|
|
|
59 |
workspace.registerTextDocumentContentProvider(uri_scheme, provider)
|
|
|
60 |
|
|
65959
|
61 |
const command_registration =
|
|
65958
|
62 |
commands.registerTextEditorCommand("isabelle.preview", editor =>
|
|
|
63 |
{
|
|
|
64 |
const uri = encode_location(editor.document.uri, editor.selection.active)
|
|
65960
|
65 |
return workspace.openTextDocument(uri).then(doc =>
|
|
|
66 |
commands.executeCommand("vscode.previewHtml", uri, view_column(), "Isabelle Preview"))
|
|
65959
|
67 |
})
|
|
65958
|
68 |
|
|
|
69 |
context.subscriptions.push(provider, provider_registration, command_registration)
|
|
|
70 |
}
|