import semver = require ( 'semver' ) ; import { commands , DocumentFilter , ExtensionContext , languages , workspace , version , extensions } from 'vscode' ; import { batchExecuteFile } from './batch' ; import { LeanCompletionItemProvider } from './completion' ; import { LeanDefinitionProvider } from './definition' ; import { LeanDiagnosticsProvider } from './diagnostics' ; import { DocViewProvider } from './docview' ; import { LeanHoles } from './holes' ; import { TacticSuggestions } from './tacticsuggestions' ; import { LeanHoverProvider } from './hover' ; import { InfoProvider } from './infoview' ; import { AbbreviationFeature } from './abbreviation' ; import { LeanpkgService } from './leanpkg' ; import { RoiManager } from './roi' ; import { LeanWorkspaceSymbolProvider } from './search' ; import { Server } from './server' ; import { LeanStatusBarItem } from './statusbar' ; import { LeanSyncService } from './sync' ; import { LeanTaskGutter , LeanTaskMessages } from './taskgutter' ; import { StaticServer } from './staticserver' ; import { LibraryNoteLinkProvider } from './librarynote' ; async function checkLean3 ( ) { const lean4 = extensions . getExtension ( 'leanprover.lean4' ) ; if ( ! lean4 ) { return true ; } return ! ( await lean4 . activate ( ) ) . isLean4Project ; } async function configExcludeOLean ( ) { const files = workspace . getConfiguration ( 'files' ) ; const exclude = files . get ( 'exclude' ) ; exclude [ '**/*.olean' ] = true ; await files . update ( 'exclude' , exclude , true ) ; } const LEAN_MODE = { language : 'lean' , } ; export async function activate ( context ) { const isLean3 = await checkLean3 ( ) ; if ( ! isLean3 ) { return ; } void configExcludeOLean ( ) ; const server = new Server ( ) ; context . subscriptions . push ( server ) ; const roiManager = new RoiManager ( server , LEAN_MODE ) ; context . subscriptions . push ( roiManager ) ; context . subscriptions . push ( new LeanSyncService ( server , LEAN_MODE ) ) ; context . subscriptions . push ( commands . registerCommand ( 'lean.restartServer' , ( ) => server . restart ( ) ) , commands . registerTextEditorCommand ( 'lean.batchExecute' , ( editor , edit , args ) => { batchExecuteFile ( server , editor , edit , args ) ; } ) ) ; context . subscriptions . push ( new LeanDiagnosticsProvider ( server ) ) ; context . subscriptions . push ( new LeanTaskGutter ( server , context ) , new LeanTaskMessages ( server ) ) ; context . subscriptions . push ( languages . registerHoverProvider ( LEAN_MODE , new LeanHoverProvider ( server ) ) ) ; context . subscriptions . push ( languages . registerCompletionItemProvider ( LEAN_MODE , new LeanCompletionItemProvider ( server ) , '.' ) ) ; context . subscriptions . push ( new AbbreviationFeature ( ) ) ; context . subscriptions . push ( languages . registerDefinitionProvider ( LEAN_MODE , new LeanDefinitionProvider ( server ) ) ) ; context . subscriptions . push ( languages . registerWorkspaceSymbolProvider ( new LeanWorkspaceSymbolProvider ( server ) ) ) ; context . subscriptions . push ( new LeanHoles ( server , LEAN_MODE ) ) ; context . subscriptions . push ( new LeanStatusBarItem ( server , roiManager ) ) ; let staticServer = null ; function waitStaticServer ( ) { const infoView = new InfoProvider ( server , LEAN_MODE , context , staticServer ) ; context . subscriptions . push ( infoView ) ; context . subscriptions . push ( new DocViewProvider ( staticServer ) ) ; context . subscriptions . push ( new TacticSuggestions ( server , infoView , LEAN_MODE ) ) ; } if ( semver . gte ( version , '1.47.0' ) ) { waitStaticServer ( ) ; } else { staticServer = new StaticServer ( context ) ; context . subscriptions . push ( staticServer ) ; staticServer . server . on ( 'listening' , waitStaticServer ) ; } context . subscriptions . push ( new LeanpkgService ( server ) ) ; context . subscriptions . push ( languages . registerDocumentLinkProvider ( LEAN_MODE , new LibraryNoteLinkProvider ( ) ) ) ; }