Platform update to 2024.1 (v1.9.0.5)

build.gradle.kts

@@ -4,16 +4,18 @@ import org.jetbrains.grammarkit.tasks.GenerateLexerTask
 import org.jetbrains.grammarkit.tasks.GenerateParserTask
 import org.jetbrains.kotlin.gradle.tasks.KotlinCompile
 import org.jetbrains.intellij.tasks.PatchPluginXmlTask
+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 {
@@ -56,18 +58,18 @@ idea {
 
 tasks {
     val test by getting(Test::class) {
-        setScanForTestClasses(false)
+        isScanForTestClasses = false
         // Only run tests from classes that end with "Test"
         include("**/*Test.class")
     }
 }
 
 intellij {
-    version.set("2023.3")
+    version.set("2024.1")
     pluginName.set("Arend")
     updateSinceUntilBuild.set(true)
     instrumentCode.set(true)
-    plugins.set(listOf("yaml", "java", "IdeaVIM:2.7.5"))
+    plugins.set(listOf("yaml", "java", "IdeaVIM:2.12.0"))
 }
 
 tasks.named<JavaExec>("runIde") {
@@ -85,16 +87,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)
@@ -104,17 +105,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,7 +3,7 @@ package org.arend
 import com.intellij.openapi.fileTypes.LanguageFileType
 import org.arend.util.FileUtils
 
-object ArendFileType : LanguageFileType(ArendLanguage.INSTANCE) {
+open class ArendFileType : LanguageFileType(ArendLanguage.INSTANCE) {
     override fun getName(): String = "Arend"
 
     override fun getDescription(): String = "Arend files"
@@ -12,3 +12,5 @@ object ArendFileType : LanguageFileType(ArendLanguage.INSTANCE) {
 
     override fun getIcon() = ArendIcons.AREND_FILE
 }
+
+object ArendFileTypeInstance : ArendFileType()

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)))
+        model.setFilterItems(singletonList(FileTypeRef.forFileType(ArendFileTypeInstance)))
         return model
     }
 

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
+    override fun getFileType(): FileType = ArendFileTypeInstance
 
     override fun getPreviewText(): String? = null
 

src/main/kotlin/org/arend/highlight/ArendUnusedImportHighlightingPass.kt

@@ -6,7 +6,6 @@ import com.intellij.codeInsight.daemon.impl.HighlightInfo
 import com.intellij.codeInsight.daemon.impl.HighlightInfoType
 import com.intellij.codeInsight.daemon.impl.UnusedSymbolUtil
 import com.intellij.codeInsight.daemon.impl.UpdateHighlightersUtil
-import com.intellij.codeInsight.daemon.impl.quickfix.QuickFixAction
 import com.intellij.codeInspection.InspectionManager
 import com.intellij.codeInspection.ProblemHighlightType
 import com.intellij.codeInspection.ex.QuickFixWrapper
@@ -53,12 +52,13 @@ class ArendUnusedImportHighlightingPass(private val file: ArendFile, private val
         val profile = InspectionProjectProfileManager.getInstance(myProject).currentProfile
         val key = HighlightDisplayKey.find(ArendUnusedImportInspection.ID)
         val highlightInfoType = if (key == null) HighlightInfoType.UNUSED_SYMBOL else HighlightInfoType.HighlightInfoTypeImpl(profile.getErrorLevel(key, element).severity, HighlightInfoType.UNUSED_SYMBOL.attributesKey)
-        UnusedSymbolUtil.createUnusedSymbolInfo(element, description, highlightInfoType, ArendUnusedImportInspection.ID)?.let {
-            val actualOptimizationResult = optimizationResult
-            if (actualOptimizationResult != null) {
-                val intentionAction = QuickFixWrapper.wrap(InspectionManager.getInstance(element.project).createProblemDescriptor(element, description, ArendOptimizeImportsQuickFix(actualOptimizationResult), ProblemHighlightType.GENERIC_ERROR_OR_WARNING, true), 0)
-                QuickFixAction.registerQuickFixAction(it, intentionAction)
-            }
+        val builder = UnusedSymbolUtil.createUnusedSymbolInfoBuilder(element, description, highlightInfoType, ArendUnusedImportInspection.ID)
+        val actualOptimizationResult = optimizationResult
+        if (actualOptimizationResult != null) {
+            val intentionAction = QuickFixWrapper.wrap(InspectionManager.getInstance(element.project).createProblemDescriptor(element, description, ArendOptimizeImportsQuickFix(actualOptimizationResult), ProblemHighlightType.GENERIC_ERROR_OR_WARNING, true), 0)
+            builder.registerFix(intentionAction, null, null, null, null)
+        }
+        builder.create()?.let {
             collector.add(it)
         }
     }

src/main/kotlin/org/arend/module/editor/ArendModuleConfigurationView.kt

@@ -127,7 +127,7 @@ class ArendModuleConfigurationView(project: Project?, root: String?, name: Strin
         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, "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

@@ -15,7 +15,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.ext.module.LongName
@@ -41,6 +41,7 @@ import org.arend.resolving.ArendReference
 import org.arend.resolving.DataLocatedReferable
 import org.arend.typechecking.BackgroundTypechecker
 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
@@ -116,13 +117,13 @@ class ArendFile(viewProvider: FileViewProvider) : PsiFileBase(viewProvider, Aren
     }
 
     fun cleanupTCRefMaps() {
-        for (refKind in RefKind.values()) {
+        for (refKind in RefKind.entries) {
             getTCRefMap(refKind).cleanup(project)
         }
     }
 
     override fun setName(name: String): PsiElement =
-        super.setName(if (name.endsWith('.' + ArendFileType.defaultExtension)) name else name + '.' + ArendFileType.defaultExtension)
+        super.setName(if (name.endsWith(FileUtils.EXTENSION)) name else name + FileUtils.EXTENSION)
 
     override fun getStub(): ArendFileStub? = super.getStub() as ArendFileStub?
 
@@ -228,9 +229,9 @@ class ArendFile(viewProvider: FileViewProvider) : PsiFileBase(viewProvider, Aren
 
     override fun getReference(): ArendReference? = null
 
-    override fun getFileType(): FileType = ArendFileType
+    override fun getFileType(): FileType = ArendFileTypeInstance
 
-    override fun textRepresentation(): String = name.removeSuffix("." + ArendFileType.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.*
 
@@ -175,7 +175,7 @@ class ArendPsiFactory(
     }
 
     fun createFromText(code: String): ArendFile? =
-        psiFactory().createFileFromText(fileName, ArendFileType, 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

@@ -7,13 +7,13 @@ import com.intellij.refactoring.changeSignature.*
 import com.intellij.refactoring.ui.ComboBoxVisibilityPanel
 import com.intellij.ui.treeStructure.Tree
 import com.intellij.util.Consumer
-import org.arend.ArendFileType
+import org.arend.ArendFileTypeInstance
 import org.arend.psi.ArendPsiFactory
 
 class ArendChangeSignatureDialog(project: Project, val descriptor: ArendChangeSignatureDescriptor) :
     ChangeSignatureDialogBase<ArendParameterInfo, PsiElement, String, ArendChangeSignatureDescriptor, ParameterTableModelItemBase<ArendParameterInfo>, ArendParameterTableModel>(project, descriptor, false, descriptor.method.context) {
 
-    override fun getFileType() = ArendFileType
+    override fun getFileType() = ArendFileTypeInstance
 
     override fun createParametersInfoModel(descriptor: ArendChangeSignatureDescriptor) =
         ArendParameterTableModel(descriptor, myDefaultValueContext)

src/main/kotlin/org/arend/refactoring/changeSignature/ArendParameterTableModel.kt

@@ -8,7 +8,7 @@ import com.intellij.refactoring.changeSignature.ParameterTableModelBase
 import com.intellij.refactoring.changeSignature.ParameterTableModelItemBase
 import com.intellij.ui.BooleanTableCellEditor
 import com.intellij.ui.BooleanTableCellRenderer
-import org.arend.ArendFileType
+import org.arend.ArendFileTypeInstance
 import javax.swing.table.TableCellEditor
 import javax.swing.table.TableCellRenderer
 
@@ -38,7 +38,6 @@ class ArendParameterTableModel(val descriptor: ArendChangeSignatureDescriptor, d
         }
     }
 
-    @Suppress("UnstableApiUsage")
     override fun removeRow(idx: Int) {
         super.removeRow(idx)
     }
@@ -65,7 +64,7 @@ class ArendParameterTableModel(val descriptor: ArendChangeSignatureDescriptor, d
     private class ArendTypeColumn(descriptor: ArendChangeSignatureDescriptor) :
         TypeColumn<ArendParameterInfo, ParameterTableModelItemBase<ArendParameterInfo>>(
             descriptor.method.project,
-            ArendFileType
+            ArendFileTypeInstance
         ) {
         override fun setValue(item: ParameterTableModelItemBase<ArendParameterInfo>?, value: PsiCodeFragment) {
             val fragment = value as? PsiTypeCodeFragment ?: return

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
@@ -28,6 +27,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
@@ -239,7 +239,7 @@ open class ArendReferenceImpl<T : ArendReferenceElement>(element: T, private val
 }
 
 private fun doRename(oldNameIdentifier: PsiElement, rawName: String) {
-    val name = rawName.removeSuffix('.' + ArendFileType.defaultExtension)
+    val name = rawName.removeSuffix(FileUtils.EXTENSION)
     if (!ArendNamesValidator.isIdentifier(name, oldNameIdentifier.project)) return
     val factory = ArendPsiFactory(oldNameIdentifier.project)
     val newNameIdentifier = when (oldNameIdentifier) {

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
+        override fun getFileType(): FileType = ArendFileTypeInstance
         override fun createExpressionCodeFragment(
             project: Project,
             text: String,

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)
+                .createEditorHighlighter(project, ArendFileTypeInstance)
         project?.serviceIfCreated<ArendProjectSettings>()?.run {
             editor.setFontSize(data.popupFontSize)
         }

src/main/resources/META-INF/plugin.xml

@@ -3,7 +3,7 @@
     <vendor>JetBrains</vendor>
 
     <!-- please see http://www.jetbrains.org/intellij/sdk/docs/basics/getting_started/build_number_ranges.html for description -->
-    <idea-version since-build="233.9102.97"/>
+    <idea-version since-build="233.11799.241"/>
 
     <!-- please see http://www.jetbrains.org/intellij/sdk/docs/basics/getting_started/plugin_compatibility.html
          on how to target different products -->

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.defaultExtension).split('/')) }
+    val modulePaths = fileNames.map { ModulePath(it.removeSuffix(FileUtils.EXTENSION).split('/')) }
 
     fun fill(dir: Entry.Directory, path: List<String>, contents: String) {
         val name = path.first()

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.defaultExtension, ArendParserDefinition()) {
+class ParsingTest : ParsingTestCase("org/arend/parser/fixtures", ArendFileTypeInstance.defaultExtension, ArendParserDefinition()) {
 
     override fun getTestDataPath() = "src/test/resources"