src/Tools/VSCode/extension/src/extension.ts
changeset 66098 5aa9cb83e70e
parent 66097 ee4c2d5b650e
child 66138 f7ef4c50b747
equal deleted inserted replaced
66097:ee4c2d5b650e 66098:5aa9cb83e70e
     2 
     2 
     3 import * as path from 'path';
     3 import * as path from 'path';
     4 import * as fs from 'fs';
     4 import * as fs from 'fs';
     5 import * as library from './library'
     5 import * as library from './library'
     6 import * as decorations from './decorations';
     6 import * as decorations from './decorations';
     7 import * as preview from './preview';
     7 import * as preview_panel from './preview_panel';
     8 import * as protocol from './protocol';
     8 import * as protocol from './protocol';
     9 import * as state from './state';
     9 import * as state_panel from './state_panel';
    10 import * as symbol from './symbol';
    10 import * as symbol from './symbol';
    11 import * as completion from './completion';
    11 import * as completion from './completion';
    12 import { ExtensionContext, workspace, window, commands, languages } from 'vscode';
    12 import { ExtensionContext, workspace, window, commands, languages } from 'vscode';
    13 import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind, NotificationType }
    13 import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind, NotificationType }
    14   from 'vscode-languageclient';
    14   from 'vscode-languageclient';
   100       language_client.onNotification(protocol.dynamic_output_type,
   100       language_client.onNotification(protocol.dynamic_output_type,
   101         params => { dynamic_output.clear(); dynamic_output.appendLine(params.content) })
   101         params => { dynamic_output.clear(); dynamic_output.appendLine(params.content) })
   102     })
   102     })
   103 
   103 
   104 
   104 
   105     /* state */
   105     /* state panel */
   106 
   106 
   107     context.subscriptions.push(
   107     context.subscriptions.push(
   108       commands.registerCommand("isabelle.state", uri => state.init(uri)),
   108       commands.registerCommand("isabelle.state", uri => state_panel.init(uri)),
   109       commands.registerCommand("_isabelle.state-locate", state.locate),
   109       commands.registerCommand("_isabelle.state-locate", state_panel.locate),
   110       commands.registerCommand("_isabelle.state-update", state.update))
   110       commands.registerCommand("_isabelle.state-update", state_panel.update))
   111 
   111 
   112     language_client.onReady().then(() => state.setup(context, language_client))
   112     language_client.onReady().then(() => state_panel.setup(context, language_client))
   113 
   113 
   114 
   114 
   115     /* preview */
   115     /* preview panel */
   116 
   116 
   117     context.subscriptions.push(
   117     context.subscriptions.push(
   118       commands.registerCommand("isabelle.preview", uri => preview.request(uri, false)),
   118       commands.registerCommand("isabelle.preview", uri => preview_panel.request(uri, false)),
   119       commands.registerCommand("isabelle.preview-split", uri => preview.request(uri, true)),
   119       commands.registerCommand("isabelle.preview-split", uri => preview_panel.request(uri, true)),
   120       commands.registerCommand("isabelle.preview-source", preview.source),
   120       commands.registerCommand("isabelle.preview-source", preview_panel.source),
   121       commands.registerCommand("isabelle.preview-update", preview.update))
   121       commands.registerCommand("isabelle.preview-update", preview_panel.update))
   122 
   122 
   123     language_client.onReady().then(() => preview.setup(context, language_client))
   123     language_client.onReady().then(() => preview_panel.setup(context, language_client))
   124 
   124 
   125 
   125 
   126     /* Isabelle symbols */
   126     /* Isabelle symbols */
   127 
   127 
   128     language_client.onReady().then(() =>
   128     language_client.onReady().then(() =>