--- a/src/Tools/VSCode/extension/package.json Wed May 31 17:32:01 2017 +0200
+++ b/src/Tools/VSCode/extension/package.json Wed May 31 20:13:05 2017 +0200
@@ -20,62 +20,62 @@
"onLanguage:isabelle",
"onLanguage:isabelle-ml",
"onCommand:isabelle.preview",
- "onCommand:isabelle.preview-side",
+ "onCommand:isabelle.preview-split",
"onCommand:isabelle.preview-source"
],
"main": "./out/src/extension",
"contributes": {
"commands": [
{
- "command": "isabelle.preview",
- "title": "Open Preview",
- "category": "Isabelle",
- "icon": {
- "light": "./media/Preview.svg",
- "dark": "./media/Preview_inverse.svg"
- }
- },
- {
- "command": "isabelle.preview-side",
- "title": "Open Preview to the Side",
- "category": "Isabelle",
- "icon": {
- "light": "./media/PreviewOnRightPane_16x.svg",
- "dark": "./media/PreviewOnRightPane_16x_dark.svg"
- }
- },
- {
- "command": "isabelle.preview-source",
- "title": "Show Source",
- "category": "Isabelle",
- "icon": {
- "light": "./media/ViewSource.svg",
- "dark": "./media/ViewSource_inverse.svg"
- }
+ "command": "isabelle.preview",
+ "title": "Open Preview",
+ "category": "Isabelle",
+ "icon": {
+ "light": "./media/Preview.svg",
+ "dark": "./media/Preview_inverse.svg"
+ }
+ },
+ {
+ "command": "isabelle.preview-split",
+ "title": "Open Preview (Split Editor)",
+ "category": "Isabelle",
+ "icon": {
+ "light": "./media/PreviewOnRightPane_16x.svg",
+ "dark": "./media/PreviewOnRightPane_16x_dark.svg"
+ }
+ },
+ {
+ "command": "isabelle.preview-source",
+ "title": "Show Source",
+ "category": "Isabelle",
+ "icon": {
+ "light": "./media/ViewSource.svg",
+ "dark": "./media/ViewSource_inverse.svg"
+ }
}
],
"menus": {
- "editor/title": [
- {
- "when": "editorLangId == isabelle",
- "command": "isabelle.preview-side",
- "alt": "isabelle.preview",
- "group": "navigation"
- },
- {
- "when": "resourceScheme == isabelle-preview",
- "command": "isabelle.preview-source",
- "group": "navigation"
- }
- ],
- "explorer/context": [
- {
- "when": "resourceLangId == isabelle",
- "command": "isabelle.preview",
- "group": "navigation"
- }
- ]
- },
+ "editor/title": [
+ {
+ "when": "editorLangId == isabelle",
+ "command": "isabelle.preview-split",
+ "alt": "isabelle.preview",
+ "group": "navigation"
+ },
+ {
+ "when": "resourceScheme == isabelle-preview",
+ "command": "isabelle.preview-source",
+ "group": "navigation"
+ }
+ ],
+ "explorer/context": [
+ {
+ "when": "resourceLangId == isabelle",
+ "command": "isabelle.preview",
+ "group": "navigation"
+ }
+ ]
+ },
"languages": [
{
"id": "isabelle",
--- a/src/Tools/VSCode/extension/src/extension.ts Wed May 31 17:32:01 2017 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts Wed May 31 20:13:05 2017 +0200
@@ -103,7 +103,7 @@
context.subscriptions.push(
commands.registerCommand("isabelle.preview", uri => preview.request_preview(uri, false)),
- commands.registerCommand("isabelle.preview-side", uri => preview.request_preview(uri, true)),
+ commands.registerCommand("isabelle.preview-split", uri => preview.request_preview(uri, true)),
commands.registerCommand("isabelle.preview-source", preview.show_source))
language_client.onReady().then(() => preview.init(context, language_client))
--- a/src/Tools/VSCode/extension/src/preview.ts Wed May 31 17:32:01 2017 +0200
+++ b/src/Tools/VSCode/extension/src/preview.ts Wed May 31 20:13:05 2017 +0200
@@ -81,23 +81,23 @@
/* commands */
-function preview_column(side: boolean): ViewColumn
+function preview_column(split: boolean): ViewColumn
{
const active_editor = window.activeTextEditor
if (!active_editor) return ViewColumn.One
- else if (!side) return active_editor.viewColumn
+ else if (!split) return active_editor.viewColumn
else if (active_editor.viewColumn === ViewColumn.One) return ViewColumn.Two
else return ViewColumn.Three
}
-export function request_preview(uri?: Uri, side: boolean = false)
+export function request_preview(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) {
language_client.sendNotification(protocol.preview_request_type,
- {uri: document_uri.toString(), column: preview_column(side) })
+ {uri: document_uri.toString(), column: preview_column(split) })
}
}