src/Tools/VSCode/extension/src/extension.ts
author wenzelm
Tue, 30 May 2017 11:50:12 +0200
changeset 65968 44e703278dfd
parent 65958 6338355b2a88
child 65969 1f93eb5c3d77
permissions -rw-r--r--
clarified modules;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     1
'use strict';
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     2
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     3
import * as vscode from 'vscode';
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     4
import * as path from 'path';
65172
365e97f009ed default cygwin_root from Isabelle distribution;
wenzelm
parents: 65171
diff changeset
     5
import * as fs from 'fs';
64755
ceb81f4928ea support for Windows;
wenzelm
parents: 64753
diff changeset
     6
import * as os from 'os';
65968
44e703278dfd clarified modules;
wenzelm
parents: 65958
diff changeset
     7
import * as library from './library'
65094
386d9d487f62 support for decorations;
wenzelm
parents: 64874
diff changeset
     8
import * as decorations from './decorations';
65958
6338355b2a88 basic setup for document preview;
wenzelm
parents: 65233
diff changeset
     9
import * as preview from './preview';
65201
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
    10
import * as protocol from './protocol';
65165
d98ede9e5917 updated to vscode-languageclient 3.0;
wenzelm
parents: 65153
diff changeset
    11
import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind, NotificationType }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    12
  from 'vscode-languageclient';
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    13
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    14
65201
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
    15
let last_caret_update: protocol.Caret_Update = {}
65180
b5a8f27a4980 tuned signature;
wenzelm
parents: 65172
diff changeset
    16
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    17
export function activate(context: vscode.ExtensionContext)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    18
{
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65167
diff changeset
    19
  const is_windows = os.type().startsWith("Windows")
64755
ceb81f4928ea support for Windows;
wenzelm
parents: 64753
diff changeset
    20
65968
44e703278dfd clarified modules;
wenzelm
parents: 65958
diff changeset
    21
  const isabelle_home = library.get_configuration<string>("home")
44e703278dfd clarified modules;
wenzelm
parents: 65958
diff changeset
    22
  const isabelle_args = library.get_configuration<Array<string>>("args")
44e703278dfd clarified modules;
wenzelm
parents: 65958
diff changeset
    23
  const cygwin_root = library.get_configuration<string>("cygwin_root")
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    24
65182
973b7669e7d9 proper Map operations;
wenzelm
parents: 65180
diff changeset
    25
973b7669e7d9 proper Map operations;
wenzelm
parents: 65180
diff changeset
    26
  /* server */
973b7669e7d9 proper Map operations;
wenzelm
parents: 65180
diff changeset
    27
65172
365e97f009ed default cygwin_root from Isabelle distribution;
wenzelm
parents: 65171
diff changeset
    28
  if (isabelle_home === "")
64755
ceb81f4928ea support for Windows;
wenzelm
parents: 64753
diff changeset
    29
    vscode.window.showErrorMessage("Missing user settings: isabelle.home")
64753
79ed396709e4 more robust startup;
wenzelm
parents: 64750
diff changeset
    30
  else {
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65167
diff changeset
    31
    const isabelle_tool = isabelle_home + "/bin/isabelle"
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65167
diff changeset
    32
    const standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"]
65167
wenzelm
parents: 65165
diff changeset
    33
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65167
diff changeset
    34
    const server_options: ServerOptions =
64755
ceb81f4928ea support for Windows;
wenzelm
parents: 64753
diff changeset
    35
      is_windows ?
65172
365e97f009ed default cygwin_root from Isabelle distribution;
wenzelm
parents: 65171
diff changeset
    36
        { command:
365e97f009ed default cygwin_root from Isabelle distribution;
wenzelm
parents: 65171
diff changeset
    37
            (cygwin_root === "" ? path.join(isabelle_home, "contrib", "cygwin") : cygwin_root) +
365e97f009ed default cygwin_root from Isabelle distribution;
wenzelm
parents: 65171
diff changeset
    38
            "/bin/bash",
64874
e13ff666af96 enable vscode_unicode_symbols by default, despite asymmetry of input and output;
wenzelm
parents: 64833
diff changeset
    39
          args: ["-l", isabelle_tool, "vscode_server"].concat(standard_args, isabelle_args) } :
64755
ceb81f4928ea support for Windows;
wenzelm
parents: 64753
diff changeset
    40
        { command: isabelle_tool,
64874
e13ff666af96 enable vscode_unicode_symbols by default, despite asymmetry of input and output;
wenzelm
parents: 64833
diff changeset
    41
          args: ["vscode_server"].concat(standard_args, isabelle_args) };
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65167
diff changeset
    42
    const client_options: LanguageClientOptions = {
64833
0f410e3b1d20 support for bibtex entries;
wenzelm
parents: 64756
diff changeset
    43
      documentSelector: ["isabelle", "isabelle-ml", "bibtex"]
64753
79ed396709e4 more robust startup;
wenzelm
parents: 64750
diff changeset
    44
    };
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    45
65168
9eabc312a2a2 prefer immutable bindings;
wenzelm
parents: 65167
diff changeset
    46
    const client = new LanguageClient("Isabelle", server_options, client_options, false)
65094
386d9d487f62 support for decorations;
wenzelm
parents: 64874
diff changeset
    47
65182
973b7669e7d9 proper Map operations;
wenzelm
parents: 65180
diff changeset
    48
65201
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
    49
    /* decorations */
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
    50
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
    51
    decorations.init(context)
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
    52
    vscode.workspace.onDidChangeConfiguration(() => decorations.init(context))
65233
e37209c0a42a always update decorations eventually after document changes: VSCode might reset it, but PIDE might produce an unchanged result that is not published again;
wenzelm
parents: 65202
diff changeset
    53
    vscode.workspace.onDidChangeTextDocument(event => decorations.touch_document(event.document))
65201
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
    54
    vscode.window.onDidChangeActiveTextEditor(decorations.update_editor)
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
    55
    vscode.workspace.onDidCloseTextDocument(decorations.close_document)
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
    56
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
    57
    client.onReady().then(() =>
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
    58
      client.onNotification(protocol.decoration_type, decorations.apply_decoration))
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
    59
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
    60
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    61
    /* caret handling and dynamic output */
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    62
65191
4c9c83311cad dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents: 65189
diff changeset
    63
    const dynamic_output = vscode.window.createOutputChannel("Isabelle Output")
4c9c83311cad dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents: 65189
diff changeset
    64
    context.subscriptions.push(dynamic_output)
4c9c83311cad dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents: 65189
diff changeset
    65
    dynamic_output.show(true)
4c9c83311cad dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents: 65189
diff changeset
    66
    dynamic_output.hide()
4c9c83311cad dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents: 65189
diff changeset
    67
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    68
    function update_caret()
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    69
    {
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    70
      const editor = vscode.window.activeTextEditor
65201
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
    71
      let caret_update: protocol.Caret_Update = {}
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    72
      if (editor) {
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    73
        const uri = editor.document.uri
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    74
        const cursor = editor.selection.active
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    75
        if (uri.scheme === "file" && cursor)
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    76
          caret_update = { uri: uri.toString(), line: cursor.line, character: cursor.character }
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    77
      }
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    78
      if (last_caret_update !== caret_update) {
65202
187277b77d50 suppress vacuous messages;
wenzelm
parents: 65201
diff changeset
    79
        if (caret_update.uri)
187277b77d50 suppress vacuous messages;
wenzelm
parents: 65201
diff changeset
    80
          client.sendNotification(protocol.caret_update_type, caret_update)
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    81
        last_caret_update = caret_update
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    82
      }
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    83
    }
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    84
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    85
    client.onReady().then(() =>
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    86
    {
65201
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
    87
      client.onNotification(protocol.dynamic_output_type,
65200
1227a68fac7a more explicit message type: allows body to become empty;
wenzelm
parents: 65191
diff changeset
    88
        params => { dynamic_output.clear(); dynamic_output.appendLine(params.body) })
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    89
      vscode.window.onDidChangeActiveTextEditor(_ => update_caret())
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    90
      vscode.window.onDidChangeTextEditorSelection(_ => update_caret())
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    91
      update_caret()
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    92
    })
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    93
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65186
diff changeset
    94
65958
6338355b2a88 basic setup for document preview;
wenzelm
parents: 65233
diff changeset
    95
    /* preview */
6338355b2a88 basic setup for document preview;
wenzelm
parents: 65233
diff changeset
    96
6338355b2a88 basic setup for document preview;
wenzelm
parents: 65233
diff changeset
    97
    preview.init(context)
6338355b2a88 basic setup for document preview;
wenzelm
parents: 65233
diff changeset
    98
6338355b2a88 basic setup for document preview;
wenzelm
parents: 65233
diff changeset
    99
65182
973b7669e7d9 proper Map operations;
wenzelm
parents: 65180
diff changeset
   100
    /* start server */
973b7669e7d9 proper Map operations;
wenzelm
parents: 65180
diff changeset
   101
65094
386d9d487f62 support for decorations;
wenzelm
parents: 64874
diff changeset
   102
    context.subscriptions.push(client.start());
386d9d487f62 support for decorations;
wenzelm
parents: 64874
diff changeset
   103
  }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   104
}
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   105
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   106
export function deactivate() { }