Merge tag 'v1.9.0.5'

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<JavaExec>("runIde") {
@@ -88,16 +90,15 @@ val generateArendLexer = tasks.register<GenerateLexerTask>("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)
 }
 
 val generateArendParser = tasks.register<GenerateParserTask>("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<GenerateLexerTask>("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<KotlinCompile>().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)
 }

gradle.properties

@@ -1 +1,2 @@
 org.gradle.jvmargs=-Xms512M -Xmx6g -XX:MaxMetaspaceSize=1g -Dkotlin.daemon.jvm.options=-Xmx6g
+kotlin.stdlib.default.dependency = false

src/main/kotlin/org/arend/ArendFileType.kt

@@ -3,17 +3,14 @@ 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"
 
     override fun getDefaultExtension(): String = FileUtils.EXTENSION.drop(1)
 
     override fun getIcon() = ArendIcons.AREND_FILE
-
-    companion object {
-        @JvmField
-        val INSTANCE = ArendFileType()
-    }
 }
+
+object ArendFileTypeInstance : ArendFileType()

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
+    }
 }

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
     }
 

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()
             }

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
 

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

src/main/kotlin/org/arend/module/orderRoot/ArendLibraryRootsComponentDescriptor.kt

@@ -7,15 +7,15 @@ 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
 
 
 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)
         },

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
 

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)
 

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<LocatedReferable>()
 
         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<NsCmdRefactoringAction>()
         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

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<ArendTextualParameter, ArendChangeSignatureDialogParameterTableModelItem>(descriptor.method.project, ArendFileType.INSTANCE) {
+        TypeColumn<ArendTextualParameter, ArendChangeSignatureDialogParameterTableModelItem>(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)

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")

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<T : ArendReferenceElement>(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) {