Platform update to 2023.3 (v1.9.0.4)

JetBrains · Dec 17, 2023 · eb537bb · eb537bb
1 parent 4b6a58c
commit eb537bb
Show file tree

Hide file tree

Showing 23 changed files with 95 additions and 88 deletions.
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -7,13 +7,13 @@ import org.jetbrains.intellij.tasks.PatchPluginXmlTask
 
 val projectArend = gradle.includedBuild("Arend")
 group = "org.arend.lang"
-version = "1.9.0.2"
+version = "1.9.0.4"
 
 plugins {
     idea
-    kotlin("jvm") version "1.8.21"
-    id("org.jetbrains.intellij") version "1.13.3"
-    id("org.jetbrains.grammarkit") version "2022.3.1"
+    kotlin("jvm") version "1.9.21"
+    id("org.jetbrains.intellij") version "1.16.1"
+    id("org.jetbrains.grammarkit") version "2022.3.2"
 }
 
 repositories {
@@ -63,11 +63,11 @@ tasks {
 }
 
 intellij {
-    version.set("2023.1")
+    version.set("2023.3")
     pluginName.set("Arend")
     updateSinceUntilBuild.set(true)
     instrumentCode.set(true)
-    plugins.set(listOf("yaml", "java", "IdeaVIM:2.1.0"))
+    plugins.set(listOf("yaml", "java", "IdeaVIM:2.7.5"))
 }
 
 tasks.named<JavaExec>("runIde") {
@@ -112,8 +112,8 @@ val generateArendDocLexer = tasks.register<GenerateLexerTask>("genArendDocLexer"
 tasks.withType<KotlinCompile>().configureEach {
     kotlinOptions {
         jvmTarget = "17"
-        languageVersion = "1.7"
-        apiVersion = "1.7"
+        languageVersion = "1.9"
+        apiVersion = "1.9"
         freeCompilerArgs = listOf("-Xjvm-default=all")
     }
     dependsOn(generateArendLexer, generateArendParser, generateArendDocLexer)
@@ -137,7 +137,7 @@ tasks.register<Copy>("prelude") {
 }
 
 tasks.withType<Wrapper> {
-    gradleVersion = "7.6"
+    gradleVersion = "8.5"
 }
 
 // Utils

diff --git a/src/main/kotlin/org/arend/ArendStartupActivity.kt b/src/main/kotlin/org/arend/ArendStartupActivity.kt
@@ -1,6 +1,5 @@
 package org.arend
 
-import com.intellij.ProjectTopics
 import com.intellij.openapi.application.runReadAction
 import com.intellij.openapi.components.service
 import com.intellij.openapi.module.Module
@@ -22,7 +21,7 @@ class ArendStartupActivity : StartupActivity.RequiredForSmartMode {
     override fun runActivity(project: Project) {
         val libraryManager = project.service<TypeCheckingService>().libraryManager
 
-        project.messageBus.connect(project).subscribe(ProjectTopics.MODULES, object : ModuleListener {
+        project.messageBus.connect(project).subscribe(ModuleListener.TOPIC, object : ModuleListener {
             override fun modulesAdded(project: Project, modules: List<Module>) {
                 for (module in modules) {
                     if (ArendModuleType.has(module)) {
@@ -57,7 +56,7 @@ class ArendStartupActivity : StartupActivity.RequiredForSmartMode {
                 val progressFraction = 1.0 / modules.size.toDouble()
                 for (module in modules) {
                     module.register()
-                    indicator.fraction = indicator.fraction + progressFraction
+                    indicator.fraction += progressFraction
                 }
             }
         })

diff --git a/src/main/kotlin/org/arend/highlight/BasePassFactory.kt b/src/main/kotlin/org/arend/highlight/BasePassFactory.kt
@@ -20,7 +20,7 @@ abstract class BasePassFactory<T : PsiFile>(private val clazz: Class<T>) : Dirty
             return null
         }
 
-        val textRange = FileStatusMap.getDirtyTextRange(editor, passId)
+        val textRange = FileStatusMap.getDirtyTextRange(editor.document, file, passId)
         return if (textRange == null) {
             EmptyHighlightingPass(file.project, editor.document)
         } else {

diff --git a/src/main/kotlin/org/arend/intention/generating/LetWrappingOptionEditorRenderer.kt b/src/main/kotlin/org/arend/intention/generating/LetWrappingOptionEditorRenderer.kt
@@ -28,7 +28,7 @@ internal class LetWrappingOptionEditorRenderer(
     private val insertedRangeReference: AtomicReference<TextRange?> = AtomicReference(null)
     private val highlighterReference: AtomicReference<ScopeHighlighter?> = AtomicReference(ScopeHighlighter(editor))
 
-    private inline fun executeWriteCommand(noinline action: () -> Unit) {
+    private fun executeWriteCommand(action: () -> Unit) {
         executeCommand(project, null, commandGroupId) { runWriteAction(action) }
     }
 

diff --git a/src/main/kotlin/org/arend/module/ArendModuleBuilder.kt b/src/main/kotlin/org/arend/module/ArendModuleBuilder.kt
@@ -36,7 +36,7 @@ class ArendModuleBuilder : ModuleBuilder() {
                 } catch (e: ConfigurationException) {
                     //IDEA-98382 We should allow Next step if user has wrong SDK
                     if (Messages.showDialog(
-                            JavaUiBundle.message("dialog.message.0.do.you.want.to.proceed", e.message),
+                            JavaUiBundle.message("dialog.message.0.do.you.want.to.proceed", e.messageHtml),
                             e.title,
                             arrayOf(CommonBundle.getYesButtonText(), CommonBundle.getNoButtonText()),
                             1,

diff --git a/src/main/kotlin/org/arend/module/ModuleSynchronizer.kt b/src/main/kotlin/org/arend/module/ModuleSynchronizer.kt
@@ -1,6 +1,5 @@
 package org.arend.module
 
-import com.intellij.ProjectTopics
 import com.intellij.openapi.application.ApplicationManager
 import com.intellij.openapi.application.runReadAction
 import com.intellij.openapi.application.runWriteAction
@@ -24,7 +23,7 @@ import kotlin.Pair
 
 class ModuleSynchronizer(private val project: Project) : ModuleRootListener {
     fun install() {
-        project.messageBus.connect().subscribe(ProjectTopics.PROJECT_ROOTS, this)
+        project.messageBus.connect().subscribe(ModuleRootListener.TOPIC, this)
         synchronizeModules()
     }
 

diff --git a/src/main/kotlin/org/arend/module/config/ArendModuleConfigurationUpdater.kt b/src/main/kotlin/org/arend/module/config/ArendModuleConfigurationUpdater.kt
@@ -1,6 +1,7 @@
 package org.arend.module.config
 
 import com.intellij.ide.util.projectWizard.ModuleBuilder
+import com.intellij.openapi.application.runReadAction
 import com.intellij.openapi.module.Module
 import com.intellij.openapi.roots.ModifiableRootModel
 import com.intellij.openapi.util.io.FileUtil
@@ -44,23 +45,32 @@ class ArendModuleConfigurationUpdater(private val isNewModule: Boolean) : Module
                 })
             configService.copyFrom(this)
         } else {
-            val yaml = moduleRoot.findChild(FileUtils.LIBRARY_CONFIG_FILE)?.let {
-                PsiManager.getInstance(rootModel.project).findFile(it) as? YAMLFile
-            } ?: return
+            if (!runReadAction {
+                val yaml = moduleRoot.findChild(FileUtils.LIBRARY_CONFIG_FILE)?.let {
+                    PsiManager.getInstance(rootModel.project).findFile(it) as? YAMLFile
+                } ?: return@runReadAction false
 
-            configService.copyFromYAML(yaml, false)
-            copyFrom(configService)
+                configService.copyFromYAML(yaml, false)
+                copyFrom(configService)
+                return@runReadAction true
+            }) {
+                return
+            }
         }
 
         val rootPath = FileUtil.toSystemDependentName(moduleRoot.path)
 
         val srcDir = toAbsolute(rootPath, sourcesDir)
-        VfsUtil.createDirectories(srcDir)
+        if (isNewModule) {
+            VfsUtil.createDirectories(srcDir)
+        }
         contentEntry.addSourceFolder(VfsUtil.pathToUrl(srcDir), false)
 
         if (testsDir != "") {
             val testDir = toAbsolute(rootPath, testsDir)
-            VfsUtil.createDirectories(testDir)
+            if (isNewModule) {
+                VfsUtil.createDirectories(testDir)
+            }
             contentEntry.addSourceFolder(VfsUtil.pathToUrl(toAbsolute(rootPath, testDir)), true)
         }
 

diff --git a/src/main/kotlin/org/arend/module/editor/ArendModuleConfigurationView.kt b/src/main/kotlin/org/arend/module/editor/ArendModuleConfigurationView.kt
@@ -8,9 +8,9 @@ import com.intellij.openapi.util.io.FileUtil
 import com.intellij.openapi.vfs.VfsUtil
 import com.intellij.ui.ScrollPaneFactory
 import com.intellij.ui.components.JBCheckBox
+import com.intellij.ui.dsl.builder.AlignX
 import com.intellij.ui.dsl.builder.RowLayout
 import com.intellij.ui.dsl.builder.panel
-import com.intellij.ui.dsl.gridLayout.HorizontalAlign
 import com.intellij.ui.layout.selected
 import org.arend.ArendIcons
 import org.arend.library.LibraryDependency
@@ -160,7 +160,7 @@ class ArendModuleConfigurationView(project: Project?, root: String?, name: Strin
         aligned("Library version: ", versionField)
         aligned("Sources directory: ", sourcesTextField)
         aligned("Tests directory: ", testsTextField)
-        checked(binariesSwitch, binariesTextField) { horizontalAlign(HorizontalAlign.FILL) }
+        checked(binariesSwitch, binariesTextField) { align(AlignX.FILL) }
             .layout(RowLayout.LABEL_ALIGNED)
 
         group("Extensions") {

diff --git a/src/main/kotlin/org/arend/project/ArendProjectImportBuilder.kt b/src/main/kotlin/org/arend/project/ArendProjectImportBuilder.kt
@@ -31,7 +31,7 @@ class ArendProjectImportBuilder : ProjectImportBuilder<String>() {
     override fun commit(project: Project, model: ModifiableModuleModel?, modulesProvider: ModulesProvider?, artifactModel: ModifiableArtifactModel?): List<Module>? {
         val rootPath = fileToImport ?: return null
         val detector = ProjectStructureDetector.EP_NAME.findExtensionOrFail(ArendProjectStructureDetector::class.java)
-        val builder = ProjectFromSourcesBuilderImpl(WizardContext(project, project), ModulesProvider.EMPTY_MODULES_PROVIDER)
+        val builder = ProjectFromSourcesBuilderImpl(WizardContext(project, project), modulesProvider ?: ModulesProvider.EMPTY_MODULES_PROVIDER)
         builder.baseProjectPath = rootPath
         detector.setupProjectStructure(listOf(File(rootPath)), builder.getProjectDescriptor(detector))
         return builder.commit(project, model, modulesProvider, artifactModel)

diff --git a/src/main/kotlin/org/arend/quickfix/referenceResolve/ArendImportHintAction.kt b/src/main/kotlin/org/arend/quickfix/referenceResolve/ArendImportHintAction.kt
@@ -20,6 +20,7 @@ import com.intellij.psi.util.CachedValuesManager
 import com.intellij.psi.util.PsiModificationTracker
 import com.intellij.psi.util.parentOfType
 import com.intellij.util.SlowOperations
+import com.intellij.util.ThreeState
 import org.arend.settings.ArendSettings
 import org.arend.naming.scope.ScopeFactory
 import org.arend.psi.ArendFile
@@ -90,7 +91,7 @@ class ArendImportHintAction(private val referenceElement: ArendReferenceElement)
 
         if (availability == ImportHintActionAvailability.AVAILABLE_FOR_SILENT_FIX &&
                 service<ArendSettings>().autoImportOnTheFly && !refElementUnderCaret /* prevent on-the-fly autoimport of element under caret */ &&
-                (ApplicationManager.getApplication().isUnitTestMode || DaemonListeners.canChangeFileSilently(psiFile)) &&
+                (ApplicationManager.getApplication().isUnitTestMode || DaemonListeners.canChangeFileSilently(psiFile, true, ThreeState.UNSURE)) &&
                 isInModlessContext) {
             val action = ArendAddImportAction(project, editor, referenceElement, referenceResolveActions.toList(), true)
             CommandProcessor.getInstance().runUndoTransparentAction { action.execute() }

diff --git a/src/main/kotlin/org/arend/refactoring/ArendRenamePsiElementProcessor.kt b/src/main/kotlin/org/arend/refactoring/ArendRenamePsiElementProcessor.kt
@@ -32,9 +32,7 @@ class ArendRenamePsiElementProcessor: RenamePsiElementProcessor() {
             try {
                 super.canRun()
             } catch (e: ConfigurationException) {
-                if (e.message != null) {
-                    throw ConfigurationException("'" + patchedGetNewName() + "'" + "is not a valid Arend module name")
-                }
+                throw ConfigurationException("'" + patchedGetNewName() + "'" + "is not a valid Arend module name")
             }
         }
 

diff --git a/src/main/kotlin/org/arend/refactoring/move/ArendMoveMembersDialog.kt b/src/main/kotlin/org/arend/refactoring/move/ArendMoveMembersDialog.kt
@@ -20,10 +20,9 @@ import com.intellij.refactoring.util.CommonRefactoringUtil
 import com.intellij.ui.RowIcon
 import com.intellij.ui.ScrollPaneFactory
 import com.intellij.ui.SeparatorFactory
+import com.intellij.ui.dsl.builder.Align
 import com.intellij.ui.dsl.builder.Row
 import com.intellij.ui.dsl.builder.panel
-import com.intellij.ui.dsl.gridLayout.HorizontalAlign
-import com.intellij.ui.dsl.gridLayout.VerticalAlign
 import org.arend.ext.module.ModulePath
 import org.arend.module.config.ArendModuleConfigService
 import org.arend.psi.ext.ArendClassStat
@@ -72,9 +71,7 @@ class ArendMoveMembersDialog(project: Project,
         dynamicGroup = JRadioButton("Dynamic")
         lateinit var classPartRow: Row
         centerPanel = panel {
-            row { cell(ScrollPaneFactory.createScrollPane(memberSelectionPanel, true))
-                .horizontalAlign(HorizontalAlign.FILL)
-                .verticalAlign(VerticalAlign.FILL)
+            row { cell(ScrollPaneFactory.createScrollPane(memberSelectionPanel, true)).align(Align.FILL)
             }.resizableRow()
             aligned("Target file: ", targetFileTextField)
             aligned("Target module: ", targetModuleTextField)

diff --git a/src/main/kotlin/org/arend/search/proof/GearActionGroup.kt b/src/main/kotlin/org/arend/search/proof/GearActionGroup.kt
@@ -24,7 +24,7 @@ class GearActionGroup(private val searchUI: ProofSearchUI, val project: Project)
         if (myPopupState.isRecentlyHidden) return // do not show new popup
         val popup = ActionManager.getInstance()
             .createActionPopupMenu(ActionPlaces.TOOLWINDOW_POPUP, ActualGearActionGroup(searchUI, project))
-        val inputEvent = e.inputEvent
+        val inputEvent = e.inputEvent ?: return
         val x = if (inputEvent is MouseEvent) inputEvent.x else 0
         val y = if (inputEvent is MouseEvent) inputEvent.y else 0
         myPopupState.prepareToShow(popup.component)

diff --git a/src/main/kotlin/org/arend/search/proof/ProofSearchUI.kt b/src/main/kotlin/org/arend/search/proof/ProofSearchUI.kt
@@ -138,11 +138,8 @@ class ProofSearchUI(private val project: Project, private val caret: Caret?) : B
         val title = JBLabel(ArendBundle.message("arend.proof.search.title"))
         val topPanel = JPanel(MigLayout("flowx, ins 0, gap 0, fillx, filly"))
         val foregroundColor = when {
-            StartupUiUtil.isUnderDarcula() -> when {
-                UIUtil.isUnderWin10LookAndFeel() -> JBColor.WHITE
-                else -> JBColor(Gray._240, Gray._200)
-            }
-            else -> UIUtil.getLabelForeground()
+            JBColor.isBright() -> UIUtil.getLabelForeground()
+            else -> JBColor(Gray._240, Gray._200)
         }
         title.foreground = foregroundColor
         title.border = BorderFactory.createEmptyBorder(3, 5, 5, 0)

diff --git a/src/main/kotlin/org/arend/toolWindow/errors/ArendMessagesService.kt b/src/main/kotlin/org/arend/toolWindow/errors/ArendMessagesService.kt
@@ -3,7 +3,7 @@ package org.arend.toolWindow.errors
 import com.intellij.openapi.application.runInEdt
 import com.intellij.openapi.components.service
 import com.intellij.openapi.observable.properties.AtomicBooleanProperty
-import com.intellij.openapi.observable.properties.BooleanProperty
+import com.intellij.openapi.observable.properties.MutableBooleanProperty
 import com.intellij.openapi.project.Project
 import com.intellij.openapi.wm.ToolWindow
 import com.intellij.openapi.wm.ToolWindowManager
@@ -17,16 +17,16 @@ class ArendMessagesService(private val project: Project) {
     var isGoalTextPinned: Boolean = false
     var isErrorTextPinned: Boolean = false
 
-    var isShowImplicitGoals: BooleanProperty =
+    var isShowImplicitGoals: MutableBooleanProperty =
             AtomicBooleanProperty(project.service<ArendProjectSettings>().data.isShowImplicitGoals).apply {
                 afterChange { project.service<ArendProjectSettings>().data.isShowImplicitGoals = it }
             }
 
-    var isShowErrorsPanel: BooleanProperty =
+    var isShowErrorsPanel: MutableBooleanProperty =
             AtomicBooleanProperty(project.service<ArendProjectSettings>().data.isShowErrorsPanel).apply {
                 afterChange { project.service<ArendProjectSettings>().data.isShowErrorsPanel = it }
             }
-    var isShowGoalsInErrorsPanel: BooleanProperty =
+    var isShowGoalsInErrorsPanel: MutableBooleanProperty =
             AtomicBooleanProperty(project.service<ArendProjectSettings>().data.isShowGoalsInErrorsPanel).apply {
                 afterChange { project.service<ArendProjectSettings>().data.isShowGoalsInErrorsPanel = it }
             }

diff --git a/src/main/kotlin/org/arend/toolWindow/errors/ArendMessagesView.kt b/src/main/kotlin/org/arend/toolWindow/errors/ArendMessagesView.kt
@@ -303,40 +303,43 @@ class ArendMessagesView(private val project: Project, toolWindow: ToolWindow) :
     }
 
     fun update() {
-        val expandedPaths = TreeUtil.collectExpandedPaths(tree)
-        val selectedPath = tree.selectionPath
-
-        val filterSet = project.service<ArendProjectSettings>().messagesFilterSet
-        val errorsMap = project.service<ErrorService>().errors
-        val map = HashMap<PsiConcreteReferable, HashMap<PsiElement?, ArendErrorTreeElement>>()
-        tree.update(root) { node ->
-            if (node == root) errorsMap.entries.filter { entry -> entry.value.any { it.error.satisfies(filterSet) } }.map { it.key }
-            else when (val obj = node.userObject) {
-                is ArendFile -> {
-                    val arendErrors = errorsMap[obj]
-                    val children = LinkedHashSet<Any>()
-                    for (arendError in arendErrors ?: emptyList()) {
-                        if (!arendError.error.satisfies(filterSet)) {
-                            continue
-                        }
+        runInEdt {
+            val expandedPaths = TreeUtil.collectExpandedPaths(tree)
+            val selectedPath = tree.selectionPath
+
+            val filterSet = project.service<ArendProjectSettings>().messagesFilterSet
+            val errorsMap = project.service<ErrorService>().errors
+            val map = HashMap<PsiConcreteReferable, HashMap<PsiElement?, ArendErrorTreeElement>>()
+            tree.update(root) { node ->
+                if (node == root) errorsMap.entries.filter { entry -> entry.value.any { it.error.satisfies(filterSet) } }.map { it.key }
+                else when (val obj = node.userObject) {
+                    is ArendFile -> {
+                        val arendErrors = errorsMap[obj]
+                        val children = LinkedHashSet<Any>()
+                        for (arendError in arendErrors ?: emptyList()) {
+                            if (!arendError.error.satisfies(filterSet)) {
+                                continue
+                            }
 
-                        val def = arendError.definition
-                        if (def == null) {
-                            children.add(ArendErrorTreeElement(arendError))
-                        } else {
-                            children.add(def)
-                            map.computeIfAbsent(def) { LinkedHashMap() }.computeIfAbsent(arendError.cause) { ArendErrorTreeElement() }.add(arendError)
+                            val def = arendError.definition
+                            if (def == null) {
+                                children.add(ArendErrorTreeElement(arendError))
+                            } else {
+                                children.add(def)
+                                map.computeIfAbsent(def) { LinkedHashMap() }.computeIfAbsent(arendError.cause) { ArendErrorTreeElement() }.add(arendError)
+                            }
                         }
+                        children
                     }
-                    children
+
+                    is PsiConcreteReferable -> map[obj]?.values ?: emptySet()
+                    else -> emptySet()
                 }
-                is PsiConcreteReferable -> map[obj]?.values ?: emptySet()
-                else -> emptySet()
             }
-        }
 
-        treeModel.reload()
-        TreeUtil.restoreExpandedPaths(tree, expandedPaths)
-        tree.selectionPath = tree.getExistingPrefix(selectedPath)
+            treeModel.reload()
+            TreeUtil.restoreExpandedPaths(tree, expandedPaths)
+            tree.selectionPath = tree.getExistingPrefix(selectedPath)
+        }
     }
 }