equal
deleted
inserted
replaced
13 dispose() { } |
13 dispose() { } |
14 |
14 |
15 provideTextDocumentContent(uri: Uri): string | Thenable<string> |
15 provideTextDocumentContent(uri: Uri): string | Thenable<string> |
16 { |
16 { |
17 const [name, pos] = decode_location(uri) |
17 const [name, pos] = decode_location(uri) |
18 return "Isabelle Preview: " + JSON.stringify([name, pos]) |
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>` |
19 } |
28 } |
20 } |
29 } |
21 |
30 |
22 export function encode_location(uri: Uri, pos: Position): Uri |
31 export function encode_location(uri: Uri, pos: Position): Uri |
23 { |
32 { |
51 |
60 |
52 const command_registration = |
61 const command_registration = |
53 commands.registerTextEditorCommand("isabelle.preview", editor => |
62 commands.registerTextEditorCommand("isabelle.preview", editor => |
54 { |
63 { |
55 const uri = encode_location(editor.document.uri, editor.selection.active) |
64 const uri = encode_location(editor.document.uri, editor.selection.active) |
56 return workspace.openTextDocument(uri).then(doc => window.showTextDocument(doc, view_column())) |
65 return workspace.openTextDocument(uri).then(doc => |
|
66 commands.executeCommand("vscode.previewHtml", uri, view_column(), "Isabelle Preview")) |
57 }) |
67 }) |
58 |
68 |
59 context.subscriptions.push(provider, provider_registration, command_registration) |
69 context.subscriptions.push(provider, provider_registration, command_registration) |
60 } |
70 } |