# HG changeset patch
# User wenzelm
# Date 1496254385 -7200
# Node ID 1be7135917a604abd713847ca1f265ff66ca9d51
# Parent  8e6a833da7dbf6ba9fc1efa9ad7cd2138a399e51
clarified name;
tuned whitespace;

diff -r 8e6a833da7db -r 1be7135917a6 src/Tools/VSCode/extension/package.json
--- 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",
diff -r 8e6a833da7db -r 1be7135917a6 src/Tools/VSCode/extension/src/extension.ts
--- 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))
diff -r 8e6a833da7db -r 1be7135917a6 src/Tools/VSCode/extension/src/preview.ts
--- 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) })
   }
 }