fun initialize()

in src/main/kotlin/org/arend/typechecking/TypeCheckingService.kt [151:206]


    fun initialize(): Boolean {
        if (isInitialized) {
            return false
        }

        synchronized(ArendPreludeLibrary::class.java) {
            if (isInitialized) {
                return false
            }

            // Initialize prelude
            val preludeLibrary = ArendPreludeLibrary(project)
            this.preludeLibrary = preludeLibrary
            libraryManager.loadLibrary(preludeLibrary, null)
            preludeLibrary.prelude?.generatedModuleLocation = Prelude.MODULE_LOCATION

            if (Prelude.isInitialized()) {
                val tcRefMap = preludeLibrary.prelude?.getTCRefMap(Referable.RefKind.EXPR)
                if (tcRefMap != null) {
                    Prelude.forEach {
                        val name = it.referable.refLongName
                        tcRefMap[name] = it.referable as IntellijTCReferable
                        val dataRef = it.referable
                        if (dataRef is DataLocatedReferable) {
                            val ref = Scope.resolveName(preludeScope, name.toList())
                            if (ref is PsiLocatedReferable) {
                                dataRef.setPointer(ref)
                            }
                        }
                    }
                }
            }

            val concreteProvider = PsiConcreteProvider(project, DummyErrorReporter.INSTANCE, null)
            preludeLibrary.resolveNames(concreteProvider, libraryManager.libraryErrorReporter)
            Prelude.PreludeTypechecking(InstanceProviderSet(), concreteProvider, ArendReferableConverter, PsiElementComparator).typecheckLibrary(preludeLibrary)
            preludeLibrary.prelude?.let {
                fillAdditionalNames(it, additionalNames)
            }

            // Set the listener that updates typechecked definitions
            service<ArendPsiChangeService>().addListener(this)

            // Listen for YAML files changes
            val yamlFileListener = YAMLFileListener(project)
            yamlFileListener.register()
            EditorFactory.getInstance().eventMulticaster.addDocumentListener(yamlFileListener, project)

            ModuleSynchronizer(project).install()

            isInitialized = true
            isLoaded = true
        }

        return true
    }