added update operation;
authorwenzelm
Wed May 31 20:33:26 2017 +0200 (2017-05-31)
changeset 65986d2b2f08533c5
parent 65985 1be7135917a6
child 65987 44e44bfc738a
added update operation;
src/Tools/VSCode/extension/package.json
src/Tools/VSCode/extension/src/extension.ts
src/Tools/VSCode/extension/src/preview.ts
     1.1 --- a/src/Tools/VSCode/extension/package.json	Wed May 31 20:13:05 2017 +0200
     1.2 +++ b/src/Tools/VSCode/extension/package.json	Wed May 31 20:33:26 2017 +0200
     1.3 @@ -36,6 +36,15 @@
     1.4                  }
     1.5              },
     1.6              {
     1.7 +                "command": "isabelle.preview-update",
     1.8 +                "title": "Update Preview",
     1.9 +                "category": "Isabelle",
    1.10 +                "icon": {
    1.11 +                    "light": "./media/Preview.svg",
    1.12 +                    "dark": "./media/Preview_inverse.svg"
    1.13 +                }
    1.14 +            },
    1.15 +            {
    1.16                  "command": "isabelle.preview-split",
    1.17                  "title": "Open Preview (Split Editor)",
    1.18                  "category": "Isabelle",
    1.19 @@ -64,6 +73,11 @@
    1.20                  },
    1.21                  {
    1.22                      "when": "resourceScheme == isabelle-preview",
    1.23 +                    "command": "isabelle.preview-update",
    1.24 +                    "group": "navigation"
    1.25 +                },
    1.26 +                {
    1.27 +                    "when": "resourceScheme == isabelle-preview",
    1.28                      "command": "isabelle.preview-source",
    1.29                      "group": "navigation"
    1.30                  }
     2.1 --- a/src/Tools/VSCode/extension/src/extension.ts	Wed May 31 20:13:05 2017 +0200
     2.2 +++ b/src/Tools/VSCode/extension/src/extension.ts	Wed May 31 20:33:26 2017 +0200
     2.3 @@ -104,14 +104,15 @@
     2.4      context.subscriptions.push(
     2.5        commands.registerCommand("isabelle.preview", uri => preview.request_preview(uri, false)),
     2.6        commands.registerCommand("isabelle.preview-split", uri => preview.request_preview(uri, true)),
     2.7 -      commands.registerCommand("isabelle.preview-source", preview.show_source))
     2.8 +      commands.registerCommand("isabelle.preview-source", preview.show_source),
     2.9 +      commands.registerCommand("isabelle.preview-update", preview.update_preview))
    2.10  
    2.11      language_client.onReady().then(() => preview.init(context, language_client))
    2.12  
    2.13  
    2.14      /* start server */
    2.15  
    2.16 -    context.subscriptions.push(language_client.start());
    2.17 +    context.subscriptions.push(language_client.start())
    2.18    }
    2.19  }
    2.20  
     3.1 --- a/src/Tools/VSCode/extension/src/preview.ts	Wed May 31 20:13:05 2017 +0200
     3.2 +++ b/src/Tools/VSCode/extension/src/preview.ts	Wed May 31 20:33:26 2017 +0200
     3.3 @@ -91,22 +91,32 @@
     3.4    else return ViewColumn.Three
     3.5  }
     3.6  
     3.7 +export function update_preview(preview_uri: Uri)
     3.8 +{
     3.9 +  const document_uri = decode_preview(preview_uri)
    3.10 +  if (document_uri && language_client) {
    3.11 +    language_client.sendNotification(protocol.preview_request_type,
    3.12 +      { uri: document_uri.toString(), column: 0 })
    3.13 +  }
    3.14 +}
    3.15 +
    3.16  export function request_preview(uri?: Uri, split: boolean = false)
    3.17  {
    3.18    const document_uri = uri || window.activeTextEditor.document.uri
    3.19    const preview_uri = encode_preview(document_uri)
    3.20    if (preview_uri && language_client) {
    3.21      language_client.sendNotification(protocol.preview_request_type,
    3.22 -      {uri: document_uri.toString(), column: preview_column(split) })
    3.23 +      { uri: document_uri.toString(), column: preview_column(split) })
    3.24    }
    3.25  }
    3.26  
    3.27 -export function show_preview(document_uri: Uri, column: ViewColumn, label: string, content: string)
    3.28 +export function show_preview(document_uri: Uri, column: number, label: string, content: string)
    3.29  {
    3.30    const preview_uri = encode_preview(document_uri)
    3.31    if (preview_uri && content_provider) {
    3.32      preview_content.set(preview_uri.toString(), content)
    3.33 -    commands.executeCommand("vscode.previewHtml", preview_uri, column, label)
    3.34 +    if (column == 0) content_provider.update(preview_uri)
    3.35 +    else commands.executeCommand("vscode.previewHtml", preview_uri, column, label)
    3.36    }
    3.37  }
    3.38