src/Tools/VSCode/extension/src/preview.ts
author wenzelm
Wed, 07 Jun 2017 15:52:18 +0200
changeset 66027 396785562768
parent 65994 46123b9dadc8
child 66064 5a00cec6bc82
permissions -rw-r--r--
avoid redundant Preview documents;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65958
6338355b2a88 basic setup for document preview;
wenzelm
parents:
diff changeset
     1
'use strict';
6338355b2a88 basic setup for document preview;
wenzelm
parents:
diff changeset
     2
65974
fd5f80ee2de0 clarified event handling;
wenzelm
parents: 65971
diff changeset
     3
import * as timers from 'timers'
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
     4
import { ViewColumn, TextDocument, TextEditor, TextDocumentContentProvider,
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
     5
  ExtensionContext, Event, EventEmitter, Uri, Position, workspace,
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
     6
  window, commands } from 'vscode'
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
     7
import { LanguageClient } from 'vscode-languageclient';
65966
169d2928cce1 clarified modules;
wenzelm
parents: 65961
diff changeset
     8
import * as library from './library'
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
     9
import * as protocol from './protocol';
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    10
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    11
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    12
/* Uri information */
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    13
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    14
const preview_uri_template = Uri.parse("isabelle-preview:Preview")
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    15
const preview_uri_scheme = preview_uri_template.scheme
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    16
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    17
function encode_preview(document_uri: Uri | undefined): Uri | undefined
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    18
{
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    19
  if (document_uri && library.is_file(document_uri)) {
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    20
    return preview_uri_template.with({ query: document_uri.fsPath })
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    21
  }
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    22
  else undefined
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    23
}
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    24
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    25
function decode_preview(preview_uri: Uri | undefined): Uri | undefined
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    26
{
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    27
  if (preview_uri && preview_uri.scheme === preview_uri_scheme) {
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    28
    return Uri.file(preview_uri.query)
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    29
  }
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    30
  else undefined
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    31
}
65958
6338355b2a88 basic setup for document preview;
wenzelm
parents:
diff changeset
    32
6338355b2a88 basic setup for document preview;
wenzelm
parents:
diff changeset
    33
65977
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents: 65974
diff changeset
    34
/* HTML content */
65971
wenzelm
parents: 65967
diff changeset
    35
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    36
const preview_content = new Map<string, string>()
65958
6338355b2a88 basic setup for document preview;
wenzelm
parents:
diff changeset
    37
65977
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents: 65974
diff changeset
    38
const default_preview_content =
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents: 65974
diff changeset
    39
  `<html>
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents: 65974
diff changeset
    40
  <head>
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents: 65974
diff changeset
    41
    <meta http-equiv="Content-type" content="text/html; charset=UTF-8">
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents: 65974
diff changeset
    42
  </head>
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents: 65974
diff changeset
    43
  <body>
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents: 65974
diff changeset
    44
    <h1>Isabelle Preview</h1>
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents: 65974
diff changeset
    45
  </body>
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents: 65974
diff changeset
    46
  </html>`
65971
wenzelm
parents: 65967
diff changeset
    47
65984
8e6a833da7db register commands earlier, before prover startup;
wenzelm
parents: 65983
diff changeset
    48
class Content_Provider implements TextDocumentContentProvider
65958
6338355b2a88 basic setup for document preview;
wenzelm
parents:
diff changeset
    49
{
6338355b2a88 basic setup for document preview;
wenzelm
parents:
diff changeset
    50
  dispose() { }
6338355b2a88 basic setup for document preview;
wenzelm
parents:
diff changeset
    51
65961
7f87310d6c09 update preview after document change;
wenzelm
parents: 65960
diff changeset
    52
  private emitter = new EventEmitter<Uri>()
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    53
  public update(preview_uri: Uri) { this.emitter.fire(preview_uri) }
65961
7f87310d6c09 update preview after document change;
wenzelm
parents: 65960
diff changeset
    54
  get onDidChange(): Event<Uri> { return this.emitter.event }
7f87310d6c09 update preview after document change;
wenzelm
parents: 65960
diff changeset
    55
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    56
  provideTextDocumentContent(preview_uri: Uri): string
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    57
  {
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    58
    return preview_content.get(preview_uri.toString()) || default_preview_content
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    59
  }
65958
6338355b2a88 basic setup for document preview;
wenzelm
parents:
diff changeset
    60
}
6338355b2a88 basic setup for document preview;
wenzelm
parents:
diff changeset
    61
6338355b2a88 basic setup for document preview;
wenzelm
parents:
diff changeset
    62
65971
wenzelm
parents: 65967
diff changeset
    63
/* init */
65959
47309113ee4d clarified view column;
wenzelm
parents: 65958
diff changeset
    64
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    65
let language_client: LanguageClient
65984
8e6a833da7db register commands earlier, before prover startup;
wenzelm
parents: 65983
diff changeset
    66
let content_provider: Content_Provider
65974
fd5f80ee2de0 clarified event handling;
wenzelm
parents: 65971
diff changeset
    67
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    68
export function init(context: ExtensionContext, client: LanguageClient)
65958
6338355b2a88 basic setup for document preview;
wenzelm
parents:
diff changeset
    69
{
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    70
  language_client = client
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    71
65984
8e6a833da7db register commands earlier, before prover startup;
wenzelm
parents: 65983
diff changeset
    72
  content_provider = new Content_Provider()
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    73
  context.subscriptions.push(
65984
8e6a833da7db register commands earlier, before prover startup;
wenzelm
parents: 65983
diff changeset
    74
    workspace.registerTextDocumentContentProvider(preview_uri_scheme, content_provider),
8e6a833da7db register commands earlier, before prover startup;
wenzelm
parents: 65983
diff changeset
    75
    content_provider)
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    76
65987
44e44bfc738a tuned signature;
wenzelm
parents: 65986
diff changeset
    77
  language_client.onNotification(protocol.preview_response_type, params =>
44e44bfc738a tuned signature;
wenzelm
parents: 65986
diff changeset
    78
    {
44e44bfc738a tuned signature;
wenzelm
parents: 65986
diff changeset
    79
      const preview_uri = encode_preview(Uri.parse(params.uri))
44e44bfc738a tuned signature;
wenzelm
parents: 65986
diff changeset
    80
      if (preview_uri) {
44e44bfc738a tuned signature;
wenzelm
parents: 65986
diff changeset
    81
        preview_content.set(preview_uri.toString(), params.content)
65994
46123b9dadc8 proper update of already existing preview;
wenzelm
parents: 65987
diff changeset
    82
        content_provider.update(preview_uri)
66027
396785562768 avoid redundant Preview documents;
wenzelm
parents: 65994
diff changeset
    83
396785562768 avoid redundant Preview documents;
wenzelm
parents: 65994
diff changeset
    84
        const existing_document =
396785562768 avoid redundant Preview documents;
wenzelm
parents: 65994
diff changeset
    85
          workspace.textDocuments.find(document =>
396785562768 avoid redundant Preview documents;
wenzelm
parents: 65994
diff changeset
    86
            document.uri.scheme === preview_uri.scheme &&
396785562768 avoid redundant Preview documents;
wenzelm
parents: 65994
diff changeset
    87
            document.uri.query === preview_uri.query)
396785562768 avoid redundant Preview documents;
wenzelm
parents: 65994
diff changeset
    88
        if (!existing_document && params.column != 0) {
65994
46123b9dadc8 proper update of already existing preview;
wenzelm
parents: 65987
diff changeset
    89
          commands.executeCommand("vscode.previewHtml", preview_uri, params.column, params.label)
46123b9dadc8 proper update of already existing preview;
wenzelm
parents: 65987
diff changeset
    90
        }
65987
44e44bfc738a tuned signature;
wenzelm
parents: 65986
diff changeset
    91
      }
44e44bfc738a tuned signature;
wenzelm
parents: 65986
diff changeset
    92
    })
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    93
}
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    94
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    95
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    96
/* commands */
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    97
65985
1be7135917a6 clarified name;
wenzelm
parents: 65984
diff changeset
    98
function preview_column(split: boolean): ViewColumn
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
    99
{
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   100
  const active_editor = window.activeTextEditor
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   101
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   102
  if (!active_editor) return ViewColumn.One
65985
1be7135917a6 clarified name;
wenzelm
parents: 65984
diff changeset
   103
  else if (!split) return active_editor.viewColumn
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   104
  else if (active_editor.viewColumn === ViewColumn.One) return ViewColumn.Two
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   105
  else return ViewColumn.Three
65974
fd5f80ee2de0 clarified event handling;
wenzelm
parents: 65971
diff changeset
   106
}
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   107
65987
44e44bfc738a tuned signature;
wenzelm
parents: 65986
diff changeset
   108
export function request(uri?: Uri, split: boolean = false)
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   109
{
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   110
  const document_uri = uri || window.activeTextEditor.document.uri
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   111
  const preview_uri = encode_preview(document_uri)
65984
8e6a833da7db register commands earlier, before prover startup;
wenzelm
parents: 65983
diff changeset
   112
  if (preview_uri && language_client) {
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   113
    language_client.sendNotification(protocol.preview_request_type,
65986
d2b2f08533c5 added update operation;
wenzelm
parents: 65985
diff changeset
   114
      { uri: document_uri.toString(), column: preview_column(split) })
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   115
  }
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   116
}
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   117
65987
44e44bfc738a tuned signature;
wenzelm
parents: 65986
diff changeset
   118
export function update(preview_uri: Uri)
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   119
{
65987
44e44bfc738a tuned signature;
wenzelm
parents: 65986
diff changeset
   120
  const document_uri = decode_preview(preview_uri)
44e44bfc738a tuned signature;
wenzelm
parents: 65986
diff changeset
   121
  if (document_uri && language_client) {
44e44bfc738a tuned signature;
wenzelm
parents: 65986
diff changeset
   122
    language_client.sendNotification(protocol.preview_request_type,
44e44bfc738a tuned signature;
wenzelm
parents: 65986
diff changeset
   123
      { uri: document_uri.toString(), column: 0 })
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   124
  }
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   125
}
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   126
65987
44e44bfc738a tuned signature;
wenzelm
parents: 65986
diff changeset
   127
export function source(preview_uri: Uri)
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   128
{
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   129
  const document_uri = decode_preview(preview_uri)
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   130
  if (document_uri) {
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   131
    const editor =
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   132
      window.visibleTextEditors.find(editor =>
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   133
        editor.document.uri.scheme === document_uri.scheme &&
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   134
        editor.document.uri.fsPath === document_uri.fsPath)
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   135
    if (editor) window.showTextDocument(editor.document, editor.viewColumn)
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   136
    else workspace.openTextDocument(document_uri).then(window.showTextDocument)
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   137
  }
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   138
  else commands.executeCommand("workbench.action.navigateBack")
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65977
diff changeset
   139
}