diff --git a/build.gradle.kts b/build.gradle.kts index ac4ae6169..7cc45ad67 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -5,16 +5,18 @@ import org.jetbrains.grammarkit.tasks.GenerateParserTask import org.jetbrains.kotlin.gradle.tasks.KotlinCompile import org.jetbrains.intellij.tasks.PatchPluginXmlTask import org.jetbrains.intellij.tasks.RunIdeBase +import org.jetbrains.kotlin.gradle.dsl.JvmTarget +import org.jetbrains.kotlin.gradle.dsl.KotlinVersion val projectArend = gradle.includedBuild("Arend") group = "org.arend.lang" -version = "1.9.0.4" +version = "1.9.0.5" plugins { idea - kotlin("jvm") version "1.9.21" - id("org.jetbrains.intellij") version "1.16.1" - id("org.jetbrains.grammarkit") version "2022.3.2" + kotlin("jvm") version "2.0.0" + id("org.jetbrains.intellij") version "1.17.4" + id("org.jetbrains.grammarkit") version "2022.3.2.2" } repositories { @@ -66,11 +68,11 @@ tasks { } intellij { - version.set("2023.3") + version.set("2024.1") pluginName.set("Arend") updateSinceUntilBuild.set(true) instrumentCode.set(true) - plugins.set(listOf("org.jetbrains.plugins.yaml", "com.intellij.java", "IdeaVIM:2.10.2")) + plugins.set(listOf("org.jetbrains.plugins.yaml", "com.intellij.java", "IdeaVIM:2.12.0")) } tasks.named("runIde") { @@ -88,8 +90,7 @@ val generateArendLexer = tasks.register("genArendLexer") { description = "Generates lexer" group = "build setup" sourceFile.set(file("src/main/grammars/ArendLexer.flex")) - targetDir.set("src/main/lexer/org/arend/lexer") - targetClass.set("ArendLexer") + targetOutputDir.set(file("src/main/lexer/org/arend/lexer")) purgeOldFiles.set(true) } @@ -97,7 +98,7 @@ val generateArendParser = tasks.register("genArendParser") { description = "Generates parser" group = "build setup" sourceFile.set(file("src/main/grammars/ArendParser.bnf")) - targetRoot.set("src/main/parser") + targetRootOutputDir.set(file("src/main/parser")) pathToParser.set("/org/arend/parser/ArendParser.java") pathToPsiRoot.set("/org/arend/psi") purgeOldFiles.set(true) @@ -107,17 +108,16 @@ val generateArendDocLexer = tasks.register("genArendDocLexer" description = "Generates doc lexer" group = "build setup" sourceFile.set(file("src/main/grammars/ArendDocLexer.flex")) - targetDir.set("src/main/doc-lexer/org/arend/lexer") - targetClass.set("ArendDocLexer") + targetOutputDir.set(file("src/main/doc-lexer/org/arend/lexer")) purgeOldFiles.set(true) } tasks.withType().configureEach { - kotlinOptions { - jvmTarget = "17" - languageVersion = "1.9" - apiVersion = "1.9" - freeCompilerArgs = listOf("-Xjvm-default=all") + compilerOptions { + jvmTarget.set(JvmTarget.JVM_17) + languageVersion.set(KotlinVersion.KOTLIN_2_0) + apiVersion.set(KotlinVersion.KOTLIN_1_9) + freeCompilerArgs.set(listOf("-Xjvm-default=all")) } dependsOn(generateArendLexer, generateArendParser, generateArendDocLexer) } diff --git a/gradle.properties b/gradle.properties index 8480afdde..210ab371d 100644 --- a/gradle.properties +++ b/gradle.properties @@ -1 +1,2 @@ org.gradle.jvmargs=-Xms512M -Xmx6g -XX:MaxMetaspaceSize=1g -Dkotlin.daemon.jvm.options=-Xmx6g +kotlin.stdlib.default.dependency = false diff --git a/src/main/kotlin/org/arend/ArendFileType.kt b/src/main/kotlin/org/arend/ArendFileType.kt index 938090979..aac188114 100644 --- a/src/main/kotlin/org/arend/ArendFileType.kt +++ b/src/main/kotlin/org/arend/ArendFileType.kt @@ -3,7 +3,7 @@ package org.arend import com.intellij.openapi.fileTypes.LanguageFileType import org.arend.util.FileUtils -class ArendFileType : LanguageFileType(ArendLanguage.INSTANCE) { +open class ArendFileType : LanguageFileType(ArendLanguage.INSTANCE) { override fun getName(): String = "Arend" override fun getDescription(): String = "Arend files" @@ -11,9 +11,6 @@ class ArendFileType : LanguageFileType(ArendLanguage.INSTANCE) { override fun getDefaultExtension(): String = FileUtils.EXTENSION.drop(1) override fun getIcon() = ArendIcons.AREND_FILE - - companion object { - @JvmField - val INSTANCE = ArendFileType() - } } + +object ArendFileTypeInstance : ArendFileType() \ No newline at end of file diff --git a/src/main/kotlin/org/arend/actions/ArendActions.kt b/src/main/kotlin/org/arend/actions/ArendActions.kt index bea5f8a16..a153b723f 100644 --- a/src/main/kotlin/org/arend/actions/ArendActions.kt +++ b/src/main/kotlin/org/arend/actions/ArendActions.kt @@ -4,5 +4,7 @@ import com.intellij.openapi.actionSystem.DefaultActionGroup import org.arend.ArendIcons.AREND class ArendActions : DefaultActionGroup("Arend Actions", "Show Arend Actions", AREND) { - override fun isPopup(): Boolean = true + init { + templatePresentation.isPopupGroup = true + } } diff --git a/src/main/kotlin/org/arend/actions/SearchArendFilesContributor.kt b/src/main/kotlin/org/arend/actions/SearchArendFilesContributor.kt index c74419b8e..0ff01e515 100644 --- a/src/main/kotlin/org/arend/actions/SearchArendFilesContributor.kt +++ b/src/main/kotlin/org/arend/actions/SearchArendFilesContributor.kt @@ -13,6 +13,7 @@ import com.intellij.openapi.actionSystem.AnActionEvent import com.intellij.openapi.project.Project import com.intellij.psi.PsiFile import org.arend.ArendFileType +import org.arend.ArendFileTypeInstance import org.arend.util.arendModules import java.util.Collections.singletonList @@ -32,7 +33,7 @@ class SearchArendFilesContributor(val event: AnActionEvent) : AbstractGotoSECont return super.acceptItem(item) } } - model.setFilterItems(singletonList(FileTypeRef.forFileType(ArendFileType.INSTANCE))) + model.setFilterItems(singletonList(FileTypeRef.forFileType(ArendFileTypeInstance))) return model } diff --git a/src/main/kotlin/org/arend/documentation/ArendDocumentationProvider.kt b/src/main/kotlin/org/arend/documentation/ArendDocumentationProvider.kt index e979174e5..2c81d6832 100644 --- a/src/main/kotlin/org/arend/documentation/ArendDocumentationProvider.kt +++ b/src/main/kotlin/org/arend/documentation/ArendDocumentationProvider.kt @@ -17,8 +17,6 @@ import com.intellij.ui.awt.RelativePoint import com.intellij.ui.jcef.JBCefBrowser import com.intellij.ui.jcef.JBCefBrowserBase import com.intellij.ui.jcef.JBCefJSQuery -import com.intellij.ui.util.height -import com.intellij.ui.util.width import org.arend.codeInsight.ArendCodeInsightUtils import org.arend.documentation.ArendKeyword.Companion.isArendKeyword import org.arend.ext.module.LongName @@ -66,7 +64,7 @@ class ArendDocumentationProvider : AbstractDocumentationProvider() { return if (ref is PsiReferable && longName.length != link.length) ref.documentation else ref as? PsiElement } - override fun getCustomDocumentationElement(editor: Editor, file: PsiFile, contextElement: PsiElement?): PsiElement? { + override fun getCustomDocumentationElement(editor: Editor, file: PsiFile, contextElement: PsiElement?, targetOffset: Int): PsiElement? { if (contextElement?.isArendKeyword() == true) { return contextElement } @@ -221,11 +219,7 @@ class ArendDocumentationProvider : AbstractDocumentationProvider() { try { val widthResult = result.toIntOrNull() ?: return@addHandler response val diffWidth = screenWidth - popup.locationOnScreen.x - if (widthResult > diffWidth) { - popup.width = diffWidth - } else { - popup.width = widthResult - } + popup.size = Dimension(if (widthResult > diffWidth) diffWidth else widthResult, popup.size.height) } catch (e: Exception) { e.printStackTrace() } @@ -235,11 +229,7 @@ class ArendDocumentationProvider : AbstractDocumentationProvider() { try { val heightResult = result.toIntOrNull() ?: return@addHandler response val diffHeight = screenHeight - popup.locationOnScreen.y - if (heightResult > diffHeight) { - popup.height = diffHeight - } else { - popup.height = heightResult - } + popup.size = Dimension(popup.size.width, if (heightResult > diffHeight) diffHeight else heightResult) } catch (e: Exception) { e.printStackTrace() } diff --git a/src/main/kotlin/org/arend/formatting/ArendCodeStyleImportsPanelWrapper.kt b/src/main/kotlin/org/arend/formatting/ArendCodeStyleImportsPanelWrapper.kt index cb21824b4..df47efb93 100644 --- a/src/main/kotlin/org/arend/formatting/ArendCodeStyleImportsPanelWrapper.kt +++ b/src/main/kotlin/org/arend/formatting/ArendCodeStyleImportsPanelWrapper.kt @@ -9,7 +9,7 @@ import com.intellij.psi.codeStyle.CodeStyleSettings import com.intellij.ui.components.JBRadioButton import com.intellij.ui.dsl.builder.* import com.intellij.ui.layout.selected -import org.arend.ArendFileType +import org.arend.ArendFileTypeInstance import org.arend.settings.ArendCustomCodeStyleSettings import org.arend.settings.ArendCustomCodeStyleSettings.OptimizeImportsPolicy import org.arend.util.ArendBundle @@ -24,7 +24,7 @@ class ArendCodeStyleImportsPanelWrapper(settings: CodeStyleSettings) : CodeStyle override fun createHighlighter(scheme: EditorColorsScheme): EditorHighlighter? = null - override fun getFileType(): FileType = ArendFileType.INSTANCE + override fun getFileType(): FileType = ArendFileTypeInstance override fun getPreviewText(): String? = null diff --git a/src/main/kotlin/org/arend/module/editor/ArendModuleConfigurationView.kt b/src/main/kotlin/org/arend/module/editor/ArendModuleConfigurationView.kt index 0d6cd62f6..8372499b8 100644 --- a/src/main/kotlin/org/arend/module/editor/ArendModuleConfigurationView.kt +++ b/src/main/kotlin/org/arend/module/editor/ArendModuleConfigurationView.kt @@ -189,7 +189,7 @@ class ArendModuleConfigurationView( get() = dualList.selectedList.content set(value) { dualList.selectedList.content = value - dualList.availableList.content -= value + dualList.availableList.content = dualList.availableList.content - value } override var versionString: String diff --git a/src/main/kotlin/org/arend/module/orderRoot/ArendLibraryRootsComponentDescriptor.kt b/src/main/kotlin/org/arend/module/orderRoot/ArendLibraryRootsComponentDescriptor.kt index 04379886f..bc5f780e8 100644 --- a/src/main/kotlin/org/arend/module/orderRoot/ArendLibraryRootsComponentDescriptor.kt +++ b/src/main/kotlin/org/arend/module/orderRoot/ArendLibraryRootsComponentDescriptor.kt @@ -7,7 +7,7 @@ import com.intellij.openapi.roots.libraries.ui.AttachRootButtonDescriptor import com.intellij.openapi.roots.libraries.ui.DescendentBasedRootFilter import com.intellij.openapi.roots.libraries.ui.LibraryRootsComponentDescriptor import com.intellij.openapi.roots.libraries.ui.OrderRootTypePresentation -import org.arend.ArendFileType +import org.arend.ArendFileTypeInstance import org.arend.util.ArendLibraryChooserDescriptor import org.arend.util.FileUtils @@ -15,7 +15,7 @@ import org.arend.util.FileUtils object ArendLibraryRootsComponentDescriptor : LibraryRootsComponentDescriptor() { override fun getRootDetectors() = listOf( ArendConfigRootDetector, - DescendentBasedRootFilter.createFileTypeBasedFilter(OrderRootType.SOURCES, false, ArendFileType.INSTANCE, "sources"), + DescendentBasedRootFilter.createFileTypeBasedFilter(OrderRootType.SOURCES, false, ArendFileTypeInstance, "sources"), DescendentBasedRootFilter(OrderRootType.CLASSES, false, "binaries") { it.name.endsWith(FileUtils.SERIALIZED_EXTENSION) }, diff --git a/src/main/kotlin/org/arend/psi/ArendFile.kt b/src/main/kotlin/org/arend/psi/ArendFile.kt index 1b8876afb..698aeccf5 100644 --- a/src/main/kotlin/org/arend/psi/ArendFile.kt +++ b/src/main/kotlin/org/arend/psi/ArendFile.kt @@ -11,7 +11,7 @@ import com.intellij.psi.impl.source.resolve.FileContextUtil import com.intellij.psi.util.CachedValueProvider import com.intellij.psi.util.CachedValuesManager import com.intellij.psi.util.PsiModificationTracker -import org.arend.ArendFileType +import org.arend.ArendFileTypeInstance import org.arend.ArendIcons import org.arend.ArendLanguage import org.arend.IArendFile @@ -38,6 +38,7 @@ import org.arend.resolving.ArendReference import org.arend.resolving.IntellijTCReferable import org.arend.term.concrete.Concrete import org.arend.typechecking.TypeCheckingService +import org.arend.util.FileUtils import org.arend.util.libraryName import org.arend.util.mapFirstNotNull import java.util.concurrent.ConcurrentHashMap @@ -87,7 +88,7 @@ class ArendFile(viewProvider: FileViewProvider) : PsiFileBase(viewProvider, Aren } override fun setName(name: String): PsiElement = - super.setName(if (name.endsWith('.' + ArendFileType.INSTANCE.defaultExtension)) name else name + '.' + ArendFileType.INSTANCE.defaultExtension) + super.setName(if (name.endsWith(FileUtils.EXTENSION)) name else name + FileUtils.EXTENSION) override fun getStub(): ArendFileStub? = super.getStub() as ArendFileStub? @@ -192,9 +193,9 @@ class ArendFile(viewProvider: FileViewProvider) : PsiFileBase(viewProvider, Aren override fun getReference(): ArendReference? = null - override fun getFileType() = ArendFileType.INSTANCE + override fun getFileType() = ArendFileTypeInstance - override fun textRepresentation(): String = name.removeSuffix("." + ArendFileType.INSTANCE.defaultExtension) + override fun textRepresentation(): String = name.removeSuffix(FileUtils.EXTENSION) override fun getPrecedence(): Precedence = Precedence.DEFAULT diff --git a/src/main/kotlin/org/arend/psi/ArendPsiFactory.kt b/src/main/kotlin/org/arend/psi/ArendPsiFactory.kt index f9a0b5fb7..0893d75b6 100644 --- a/src/main/kotlin/org/arend/psi/ArendPsiFactory.kt +++ b/src/main/kotlin/org/arend/psi/ArendPsiFactory.kt @@ -5,7 +5,7 @@ import com.intellij.psi.PsiElement import com.intellij.psi.PsiFile import com.intellij.psi.PsiFileFactory import com.intellij.psi.PsiParserFacade -import org.arend.ArendFileType +import org.arend.ArendFileTypeInstance import org.arend.InjectionTextLanguage import org.arend.psi.ext.* @@ -182,7 +182,7 @@ class ArendPsiFactory( } fun createFromText(code: String): ArendFile? = - psiFactory().createFileFromText(fileName, ArendFileType.INSTANCE, code) as? ArendFile + psiFactory().createFileFromText(fileName, ArendFileTypeInstance, code) as? ArendFile private fun psiFactory() = PsiFileFactory.getInstance(project) diff --git a/src/main/kotlin/org/arend/refactoring/changeSignature/ArendChangeSignatureDialog.kt b/src/main/kotlin/org/arend/refactoring/changeSignature/ArendChangeSignatureDialog.kt index 0340a2961..b509e01f9 100644 --- a/src/main/kotlin/org/arend/refactoring/changeSignature/ArendChangeSignatureDialog.kt +++ b/src/main/kotlin/org/arend/refactoring/changeSignature/ArendChangeSignatureDialog.kt @@ -33,7 +33,7 @@ import com.intellij.ui.ToolbarDecorator import com.intellij.ui.table.TableView import com.intellij.ui.treeStructure.Tree import com.intellij.util.Consumer -import org.arend.ArendFileType +import org.arend.ArendFileTypeInstance import org.arend.ext.module.LongName import org.arend.naming.reference.LocatedReferable import org.arend.naming.scope.ListScope @@ -127,7 +127,7 @@ class ArendChangeSignatureDialog(project: Project, super.customizeParametersTable(table) } - override fun getFileType() = ArendFileType.INSTANCE + override fun getFileType() = ArendFileTypeInstance override fun createParametersInfoModel(descriptor: ArendChangeSignatureDescriptor) = ArendParameterTableModel( descriptor, this, myDefaultValueContext) @@ -156,7 +156,7 @@ class ArendChangeSignatureDialog(project: Project, if (item.parameter.name.let { it.isEmpty() || isElim && it == "_" }) //We may need to transform "with-body" to "elim-body" so "_" may turn into a problem return RefactoringBundle.message("refactoring.introduce.parameter.invalid.name", item.parameter.name) } - + val allPsiTargets = HashSet() fun processFragment(fragment: ArendExpressionCodeFragment) { @@ -173,7 +173,7 @@ class ArendChangeSignatureDialog(project: Project, /* Validate namespace commands to be invoked upon refactoring start; purge unused namespace commands */ val unusedNsCmds = HashSet() for (nsCmd in this.deferredNsCmds) if (nsCmd.getAmendedScope().elements.intersect(allPsiTargets).isEmpty()) unusedNsCmds.add(nsCmd) - this.deferredNsCmds.removeAll(unusedNsCmds) + this.deferredNsCmds.removeAll(unusedNsCmds) /* Validate that code fragments for parameter types do not contain resolving errors */ var hasErrors = false diff --git a/src/main/kotlin/org/arend/refactoring/changeSignature/ArendParameterTableModel.kt b/src/main/kotlin/org/arend/refactoring/changeSignature/ArendParameterTableModel.kt index 823c7b4d9..027433358 100644 --- a/src/main/kotlin/org/arend/refactoring/changeSignature/ArendParameterTableModel.kt +++ b/src/main/kotlin/org/arend/refactoring/changeSignature/ArendParameterTableModel.kt @@ -8,7 +8,7 @@ import com.intellij.refactoring.changeSignature.ParameterTableModelItemBase import com.intellij.refactoring.ui.CodeFragmentTableCellEditorBase import com.intellij.ui.BooleanTableCellEditor import com.intellij.ui.BooleanTableCellRenderer -import org.arend.ArendFileType +import org.arend.ArendFileTypeInstance import org.arend.ext.module.LongName import org.arend.psi.ArendExpressionCodeFragment import org.arend.util.FileUtils.isCorrectDefinitionName @@ -47,14 +47,14 @@ class ArendParameterTableModel(val descriptor: ArendChangeSignatureDescriptor, } private class ArendTypeColumn(descriptor: ArendChangeSignatureDescriptor, val dialog: ArendChangeSignatureDialog) : - TypeColumn(descriptor.method.project, ArendFileType.INSTANCE) { + TypeColumn(descriptor.method.project, ArendFileTypeInstance) { override fun setValue(item: ArendChangeSignatureDialogParameterTableModelItem?, value: PsiCodeFragment) { val fragment = value as? ArendExpressionCodeFragment ?: return item?.parameter?.setType(fragment.text) } override fun doCreateEditor(o: ArendChangeSignatureDialogParameterTableModelItem?): TableCellEditor { - return object: CodeFragmentTableCellEditorBase(myProject, ArendFileType.INSTANCE) { + return object: CodeFragmentTableCellEditorBase(myProject, ArendFileTypeInstance) { override fun getTableCellEditorComponent(table: JTable?, value: Any?, isSelected: Boolean, row: Int, column: Int): Component { clearListeners() val result = super.getTableCellEditorComponent(table, value, isSelected, row, column) diff --git a/src/main/kotlin/org/arend/refactoring/move/ArendMoveMembersDialog.kt b/src/main/kotlin/org/arend/refactoring/move/ArendMoveMembersDialog.kt index 060acbc13..75eb2d206 100644 --- a/src/main/kotlin/org/arend/refactoring/move/ArendMoveMembersDialog.kt +++ b/src/main/kotlin/org/arend/refactoring/move/ArendMoveMembersDialog.kt @@ -20,7 +20,7 @@ import com.intellij.ui.dsl.builder.Align import com.intellij.ui.dsl.builder.Row import com.intellij.ui.dsl.builder.panel import com.intellij.util.Alarm -import org.arend.ArendFileType +import org.arend.ArendFileTypeInstance import org.arend.codeInsight.ArendCodeInsightUtils import org.arend.ext.module.ModulePath import org.arend.module.AllArendFilesScope @@ -77,12 +77,12 @@ class ArendMoveMembersDialog(project: Project, val containingFile = container.containingFile as? ArendFile val globalScope = containingFile?.libraryConfig?.let { AllArendFilesScope(it) } ?: EmptyScope.INSTANCE - targetFileField = EditorTextField(PsiDocumentManager.getInstance(project).getDocument(ArendLongNameCodeFragment(project, fullName?.modulePath?.toString() ?: "", null, customScopeGetter = { globalScope })), project, ArendFileType.INSTANCE) + targetFileField = EditorTextField(PsiDocumentManager.getInstance(project).getDocument(ArendLongNameCodeFragment(project, fullName?.modulePath?.toString() ?: "", null, customScopeGetter = { globalScope })), project, ArendFileTypeInstance) targetModuleField = EditorTextField(PsiDocumentManager.getInstance(project).getDocument(ArendLongNameCodeFragment(project, fullName?.longName?.toString() ?: "", null, customScopeGetter = { val group = simpleLocate(targetFileField.text, "", enclosingModule).first group?.let { FilteringScope(LexicalScope.insideOf(it, EmptyScope.INSTANCE)) { referable -> referable !is ArendClassField && referable !is ArendConstructor && referable !is ArendFieldDefIdentifier - } } ?: EmptyScope.INSTANCE })), project, ArendFileType.INSTANCE) + } } ?: EmptyScope.INSTANCE })), project, ArendFileTypeInstance) memberSelectionPanel = ArendMemberSelectionPanel("Members to move", memberInfos) staticGroup = JRadioButton("Static") diff --git a/src/main/kotlin/org/arend/resolving/ArendReference.kt b/src/main/kotlin/org/arend/resolving/ArendReference.kt index 8c5f211aa..67124dc35 100644 --- a/src/main/kotlin/org/arend/resolving/ArendReference.kt +++ b/src/main/kotlin/org/arend/resolving/ArendReference.kt @@ -5,7 +5,6 @@ import com.intellij.openapi.components.service import com.intellij.openapi.util.TextRange import com.intellij.psi.* import com.intellij.psi.impl.source.tree.LeafPsiElement -import org.arend.ArendFileType import org.arend.ArendIcons import org.arend.codeInsight.completion.ReplaceInsertHandler import org.arend.core.definition.Definition @@ -30,6 +29,7 @@ import org.arend.term.abs.ConcreteBuilder import org.arend.term.concrete.Concrete import org.arend.toolWindow.repl.getReplCompletion import org.arend.typechecking.TypeCheckingService +import org.arend.util.FileUtils interface ArendReference : PsiReference { override fun getElement(): ArendReferenceElement @@ -238,7 +238,7 @@ open class ArendReferenceImpl(element: T, beforeImpor } private fun doRename(oldNameIdentifier: PsiElement, rawName: String) { - val name = rawName.removeSuffix('.' + ArendFileType.INSTANCE.defaultExtension) + val name = rawName.removeSuffix(FileUtils.EXTENSION) if (!ArendNamesValidator.INSTANCE.isIdentifier(name, oldNameIdentifier.project)) return val factory = ArendPsiFactory(oldNameIdentifier.project) val newNameIdentifier = when (oldNameIdentifier) { diff --git a/src/main/kotlin/org/arend/tracer/ArendTraceProcess.kt b/src/main/kotlin/org/arend/tracer/ArendTraceProcess.kt index a33ff0544..7b0f8f713 100644 --- a/src/main/kotlin/org/arend/tracer/ArendTraceProcess.kt +++ b/src/main/kotlin/org/arend/tracer/ArendTraceProcess.kt @@ -28,7 +28,7 @@ import com.intellij.xdebugger.impl.DebuggerSupport import com.intellij.xdebugger.impl.actions.* import com.intellij.xdebugger.impl.actions.handlers.XDebuggerActionHandler import com.intellij.xdebugger.ui.XDebugTabLayouter -import org.arend.ArendFileType +import org.arend.ArendFileTypeInstance import org.arend.psi.ext.ArendExpr import org.arend.psi.ArendFile import org.arend.psi.ArendPsiFactory @@ -221,7 +221,7 @@ class ArendTraceProcess(session: XDebugSession, private val tracingData: ArendTr } private object EditorsProvider : XDebuggerEditorsProviderBase() { - override fun getFileType(): FileType = ArendFileType.INSTANCE + override fun getFileType(): FileType = ArendFileTypeInstance override fun createExpressionCodeFragment( project: Project, text: String, diff --git a/src/main/kotlin/org/arend/typechecking/error/PsiHyperlinkInfo.kt b/src/main/kotlin/org/arend/typechecking/error/PsiHyperlinkInfo.kt index f897db0d4..7df35898d 100644 --- a/src/main/kotlin/org/arend/typechecking/error/PsiHyperlinkInfo.kt +++ b/src/main/kotlin/org/arend/typechecking/error/PsiHyperlinkInfo.kt @@ -13,7 +13,7 @@ import com.intellij.openapi.project.Project import com.intellij.psi.PsiElement import com.intellij.psi.SmartPointerManager import com.intellij.psi.SmartPsiElementPointer -import org.arend.ArendFileType +import org.arend.ArendFileTypeInstance import org.arend.ext.error.ArgInferenceError import org.arend.ext.error.GeneralError import org.arend.ext.error.SourceInfoReference @@ -49,7 +49,7 @@ fun mapToTypeDiffInfo(error: GeneralError?): Pair if (error.expected != null && error.actual != null) Pair(error.expected, error.actual) else null else -> null } ?: return null - return Pair(diffContentFactory.create(pair.first.toString(), ArendFileType.INSTANCE), diffContentFactory.create(pair.second.toString(), ArendFileType.INSTANCE)) + return Pair(diffContentFactory.create(pair.first.toString(), ArendFileTypeInstance), diffContentFactory.create(pair.second.toString(), ArendFileTypeInstance)) } class DiffHyperlinkInfo(private val typeDiffInfo: Pair): HyperlinkInfo { diff --git a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt index e2818d08d..1ab1a3341 100644 --- a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt +++ b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt @@ -1,6 +1,7 @@ package org.arend.typechecking.execution import com.intellij.execution.process.ProcessHandler +import com.intellij.ide.SaveAndSyncHandler import com.intellij.openapi.application.ApplicationManager import com.intellij.openapi.application.runReadAction import com.intellij.openapi.components.service diff --git a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt index 37ec71035..4557b085d 100644 --- a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt +++ b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt @@ -7,7 +7,7 @@ import com.intellij.openapi.project.Project import com.intellij.psi.PsiDocumentManager import com.intellij.ui.EditorTextField import com.intellij.ui.dsl.builder.panel -import org.arend.ArendFileType +import org.arend.ArendFileTypeInstance import org.arend.definition.ArendFileDefinitionScope import org.arend.module.AllArendFilesScope import org.arend.module.AllModulesScope @@ -29,7 +29,7 @@ class TypeCheckRunConfigurationEditor(private val project: Project) : SettingsEd init { libraryComponent = EditorTextField(PsiDocumentManager.getInstance(project).getDocument( - ArendLongNameCodeFragment(project, LIBRARY_TEXT, null, customScopeGetter = { AllModulesScope(project) })), project, ArendFileType.INSTANCE) + ArendLongNameCodeFragment(project, LIBRARY_TEXT, null, customScopeGetter = { AllModulesScope(project) })), project, ArendFileTypeInstance) val moduleDocument = ArendLongNameCodeFragment(project, MODULE_TEXT, null, customScopeGetter = { val library = libraryComponent.text if (library == PRELUDE) { @@ -39,7 +39,7 @@ class TypeCheckRunConfigurationEditor(private val project: Project) : SettingsEd val arendModuleConfigService = ArendModuleConfigService.getInstance(module) arendModuleConfigService?.let { AllArendFilesScope(it, withPrelude = false) } ?: EmptyScope.INSTANCE }) - modulePathComponent = EditorTextField(PsiDocumentManager.getInstance(project).getDocument(moduleDocument), project, ArendFileType.INSTANCE) + modulePathComponent = EditorTextField(PsiDocumentManager.getInstance(project).getDocument(moduleDocument), project, ArendFileTypeInstance) definitionNameComponent = EditorTextField(PsiDocumentManager.getInstance(project).getDocument(ArendLongNameCodeFragment(project, DEFINITION_TEXT, null, customScopeGetter = { val library = libraryComponent.text val module = modulePathComponent.text @@ -51,7 +51,7 @@ class TypeCheckRunConfigurationEditor(private val project: Project) : SettingsEd val arendFile = moduleDocument.scope.resolveName(module)?.underlyingReferable as? ArendFile? ?: return@ArendLongNameCodeFragment EmptyScope.INSTANCE ArendFileDefinitionScope(arendFile) - })), project, ArendFileType.INSTANCE) + })), project, ArendFileTypeInstance) } override fun resetEditorFrom(configuration: TypeCheckConfiguration) { diff --git a/src/main/kotlin/org/arend/ui/ArendEditor.kt b/src/main/kotlin/org/arend/ui/ArendEditor.kt index 5f2e5cc80..209c3d5d2 100644 --- a/src/main/kotlin/org/arend/ui/ArendEditor.kt +++ b/src/main/kotlin/org/arend/ui/ArendEditor.kt @@ -7,7 +7,7 @@ import com.intellij.openapi.editor.ex.EditorEx import com.intellij.openapi.editor.highlighter.EditorHighlighterFactory import com.intellij.openapi.editor.impl.EditorImpl import com.intellij.openapi.project.Project -import org.arend.ArendFileType +import org.arend.ArendFileTypeInstance import org.arend.settings.ArendProjectSettings class ArendEditor( @@ -23,7 +23,7 @@ class ArendEditor( editor.isViewer = readOnly editor.highlighter = EditorHighlighterFactory .getInstance() - .createEditorHighlighter(project, ArendFileType.INSTANCE) + .createEditorHighlighter(project, ArendFileTypeInstance) project?.serviceIfCreated()?.run { editor.setFontSize(data.popupFontSize) } diff --git a/src/main/resources/META-INF/plugin.xml b/src/main/resources/META-INF/plugin.xml index 9ae26aa57..25f8b817f 100644 --- a/src/main/resources/META-INF/plugin.xml +++ b/src/main/resources/META-INF/plugin.xml @@ -3,7 +3,7 @@ JetBrains - + diff --git a/src/test/kotlin/org/arend/FileTree.kt b/src/test/kotlin/org/arend/FileTree.kt index a1d74c442..844ef0b1a 100644 --- a/src/test/kotlin/org/arend/FileTree.kt +++ b/src/test/kotlin/org/arend/FileTree.kt @@ -24,7 +24,7 @@ fun fileTreeFromText(@Language("Arend") text: String): FileTree { check(fileNames.size == fileTexts.size) { "Have you placed `-- ! filename.ard` markers?" } } - val modulePaths = fileNames.map { ModulePath(it.removeSuffix('.' + ArendFileType.INSTANCE.defaultExtension).split('/')) } + val modulePaths = fileNames.map { ModulePath(it.removeSuffix(FileUtils.EXTENSION).split('/')) } fun fill(dir: Entry.Directory, path: List, contents: String) { val name = path.first() diff --git a/src/test/kotlin/org/arend/ParsingTest.kt b/src/test/kotlin/org/arend/ParsingTest.kt index 556314492..1ac9e31b9 100644 --- a/src/test/kotlin/org/arend/ParsingTest.kt +++ b/src/test/kotlin/org/arend/ParsingTest.kt @@ -3,7 +3,7 @@ package org.arend import com.intellij.testFramework.ParsingTestCase import org.arend.parser.ArendParserDefinition -class ParsingTest : ParsingTestCase("org/arend/parser/fixtures", ArendFileType.INSTANCE.defaultExtension, ArendParserDefinition()) { +class ParsingTest : ParsingTestCase("org/arend/parser/fixtures", ArendFileTypeInstance.defaultExtension, ArendParserDefinition()) { override fun getTestDataPath() = "src/test/resources"