less ambitious preview: discontinued preview-update / preview-source which did not work on the spot via WebviewPanel;
--- a/src/Tools/VSCode/extension/package.json Wed Feb 26 15:34:52 2020 +0100
+++ b/src/Tools/VSCode/extension/package.json Wed Feb 26 15:38:04 2020 +0100
@@ -27,8 +27,7 @@
"onLanguage:isabelle-ml",
"onLanguage:bibtex",
"onCommand:isabelle.preview",
- "onCommand:isabelle.preview-split",
- "onCommand:isabelle.preview-source"
+ "onCommand:isabelle.preview-split"
],
"main": "./out/src/extension",
"contributes": {
@@ -48,15 +47,6 @@
}
},
{
- "command": "isabelle.preview-update",
- "title": "Update Preview",
- "category": "Isabelle",
- "icon": {
- "light": "./media/Preview.svg",
- "dark": "./media/Preview_inverse.svg"
- }
- },
- {
"command": "isabelle.preview-split",
"title": "Open Preview (Split Editor)",
"category": "Isabelle",
@@ -66,15 +56,6 @@
}
},
{
- "command": "isabelle.preview-source",
- "title": "Show Source",
- "category": "Isabelle",
- "icon": {
- "light": "./media/ViewSource.svg",
- "dark": "./media/ViewSource_inverse.svg"
- }
- },
- {
"command": "isabelle.include-word",
"title": "Include word",
"category": "Isabelle"
@@ -131,16 +112,6 @@
"when": "editorLangId == bibtex",
"command": "isabelle.preview-split",
"group": "navigation"
- },
- {
- "when": "resourceScheme == isabelle-preview",
- "command": "isabelle.preview-update",
- "group": "navigation"
- },
- {
- "when": "resourceScheme == isabelle-preview",
- "command": "isabelle.preview-source",
- "group": "navigation"
}
],
"explorer/context": [
--- a/src/Tools/VSCode/extension/src/extension.ts Wed Feb 26 15:34:52 2020 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts Wed Feb 26 15:38:04 2020 +0100
@@ -139,9 +139,7 @@
context.subscriptions.push(
commands.registerCommand("isabelle.preview", uri => preview_panel.request(uri, false)),
- commands.registerCommand("isabelle.preview-split", uri => preview_panel.request(uri, true)),
- commands.registerCommand("isabelle.preview-source", preview_panel.source),
- commands.registerCommand("isabelle.preview-update", preview_panel.update))
+ commands.registerCommand("isabelle.preview-split", uri => preview_panel.request(uri, true)))
language_client.onReady().then(() => preview_panel.setup(context, language_client))
--- a/src/Tools/VSCode/extension/src/preview_panel.ts Wed Feb 26 15:34:52 2020 +0100
+++ b/src/Tools/VSCode/extension/src/preview_panel.ts Wed Feb 26 15:38:04 2020 +0100
@@ -1,94 +1,59 @@
'use strict';
-import * as timers from 'timers'
-import { ViewColumn, TextDocument, TextEditor, TextDocumentContentProvider,
- ExtensionContext, Event, EventEmitter, Uri, Position, workspace,
- window, commands, WebviewPanel } from 'vscode'
+import { ExtensionContext, Uri, workspace,
+ window, commands, ViewColumn, WebviewPanel } from 'vscode'
import { LanguageClient } from 'vscode-languageclient';
import * as library from './library'
import * as protocol from './protocol'
-import { Content_Provider } from './content_provider'
-/* HTML content */
-
-const content_provider = new Content_Provider("isabelle-preview")
-
-function encode_preview(document_uri: Uri | undefined): Uri | undefined
-{
- if (document_uri && library.is_file(document_uri)) {
- return content_provider.uri_template.with({ query: document_uri.fsPath })
- }
- else undefined
-}
-
-function decode_preview(preview_uri: Uri | undefined): Uri | undefined
-{
- if (preview_uri && preview_uri.scheme === content_provider.uri_scheme) {
- return Uri.file(preview_uri.query)
- }
- else undefined
-}
-
-
-/* setup */
-
let language_client: LanguageClient
+class Panel
+{
+ private webview_panel: WebviewPanel
+
+ public set_content(title: string, body: string)
+ {
+ this.webview_panel.title = title
+ this.webview_panel.webview.html = body
+ }
+
+ public reveal(column: ViewColumn)
+ {
+ this.webview_panel.reveal(column)
+ }
+
+ constructor(column: ViewColumn)
+ {
+ this.webview_panel =
+ window.createWebviewPanel("isabelle-preview", "Preview", column,
+ {
+ enableScripts: true
+ });
+ this.webview_panel.onDidDispose(() => { panel = null })
+ }
+}
+
+let panel: Panel
+
export function setup(context: ExtensionContext, client: LanguageClient)
{
- context.subscriptions.push(content_provider.register())
-
- var panel: WebviewPanel
language_client = client
language_client.onNotification(protocol.preview_response_type, params =>
{
- const preview_uri = encode_preview(Uri.parse(params.uri))
- if (!panel) {
- panel = window.createWebviewPanel(
- preview_uri.fsPath,
- params.label,
- params.column,
- {
- enableScripts: true,
- retainContextWhenHidden: true
- }
- );
- }
- panel.webview.html = params.content;
+ if (!panel) { panel = new Panel(params.column) }
+ else panel.reveal(params.column)
+ panel.set_content(params.label, params.content)
})
}
-
-/* commands */
-
export function request(uri?: Uri, split: boolean = false)
{
const document_uri = uri || window.activeTextEditor.document.uri
- const preview_uri = encode_preview(document_uri)
- if (preview_uri && language_client) {
+ if (language_client) {
language_client.sendNotification(protocol.preview_request_type,
{ uri: document_uri.toString(),
column: library.adjacent_editor_column(window.activeTextEditor, split) })
}
}
-
-export function update(preview_uri: Uri)
-{
- const document_uri = decode_preview(preview_uri)
- if (document_uri && language_client) {
- language_client.sendNotification(protocol.preview_request_type,
- { uri: document_uri.toString(), column: 0 })
- }
-}
-
-export function source(preview_uri: Uri)
-{
- const document_uri = decode_preview(preview_uri)
- if (document_uri) {
- const editor = library.find_file_editor(document_uri)
- if (editor) window.showTextDocument(editor.document, editor.viewColumn)
- else workspace.openTextDocument(document_uri).then(window.showTextDocument)
- }
- else commands.executeCommand("workbench.action.navigateBack")
-}