diff --git a/src/main/kotlin/org/arend/actions/ArendCreateFileAction.kt b/src/main/kotlin/org/arend/actions/ArendCreateFileAction.kt index 65f3feee4..3c0831ad2 100644 --- a/src/main/kotlin/org/arend/actions/ArendCreateFileAction.kt +++ b/src/main/kotlin/org/arend/actions/ArendCreateFileAction.kt @@ -35,6 +35,6 @@ class ArendCreateFileAction : CreateFileFromTemplateAction(CAPTION, "", ArendIco } private companion object { - private const val CAPTION = "New Arend File" + private const val CAPTION = "Arend File" } } diff --git a/src/main/kotlin/org/arend/actions/mark/ArendMarkActionUtils.kt b/src/main/kotlin/org/arend/actions/mark/ArendMarkActionUtils.kt index 4d76f97d4..c970e4541 100644 --- a/src/main/kotlin/org/arend/actions/mark/ArendMarkActionUtils.kt +++ b/src/main/kotlin/org/arend/actions/mark/ArendMarkActionUtils.kt @@ -5,7 +5,8 @@ import com.intellij.ide.projectView.actions.MarkRootActionBase import com.intellij.openapi.actionSystem.AnActionEvent import com.intellij.openapi.actionSystem.CommonDataKeys import com.intellij.openapi.actionSystem.LangDataKeys -import com.intellij.openapi.application.ApplicationManager +import com.intellij.openapi.application.invokeLater +import com.intellij.openapi.application.runWriteAction import com.intellij.openapi.module.Module import com.intellij.openapi.roots.* import com.intellij.openapi.vfs.LocalFileSystem @@ -44,8 +45,12 @@ private fun getDirByType(directoryType: DirectoryType, arendModuleConfigService: } private fun commitModel(module: Module?, model: ModifiableRootModel?) { - ApplicationManager.getApplication().runWriteAction { model?.commit() } - module?.project?.let { SaveAndSyncHandler.getInstance().scheduleProjectSave(it) } + invokeLater { + runWriteAction { + model?.commit() + } + module?.project?.let { SaveAndSyncHandler.getInstance().scheduleProjectSave(it) } + } } internal fun removeOldFolder(virtualFile: VirtualFile?, arendModuleConfigService: ArendModuleConfigService?, directoryType: DirectoryType) { diff --git a/src/main/kotlin/org/arend/intention/ReplaceBracketsIntention.kt b/src/main/kotlin/org/arend/intention/ReplaceBracketsIntention.kt index 53388f8d4..41cfa04cb 100644 --- a/src/main/kotlin/org/arend/intention/ReplaceBracketsIntention.kt +++ b/src/main/kotlin/org/arend/intention/ReplaceBracketsIntention.kt @@ -6,13 +6,14 @@ import com.intellij.openapi.editor.Editor import com.intellij.openapi.project.Project import com.intellij.psi.PsiDocumentManager import com.intellij.psi.PsiElement +import com.intellij.psi.util.elementType import com.intellij.refactoring.suggested.startOffset import org.arend.psi.ArendElementTypes.* import org.arend.psi.childOfType import org.arend.psi.ext.ArendCompositeElement import org.arend.util.ArendBundle -class ReplaceBracketsIntention : SelfTargetingIntention(PsiElement::class.java, ArendBundle.message("arend.replaceBrackets")) { +class ReplaceBracketsIntention : SelfTargetingIntention(PsiElement::class.java, ArendBundle.message("arend.replaceBrackets")) { private fun getBrackets(element: PsiElement): Pair { var currentElement: PsiElement? = element @@ -33,6 +34,11 @@ class ReplaceBracketsIntention : SelfTargetingIntention(PsiElement:: override fun isApplicableTo(element: PsiElement, caretOffset: Int, editor: Editor): Boolean { val (left, right) = getBrackets(element) + text = if (left.elementType == LPAREN) { + ArendBundle.message("arend.replaceBrackets") + } else { + ArendBundle.message("arend.replaceParentheses") + } return left == element || right == element } diff --git a/src/main/kotlin/org/arend/psi/listener/ArendPsiChangeService.kt b/src/main/kotlin/org/arend/psi/listener/ArendPsiChangeService.kt index 5b6e08a78..eae446172 100644 --- a/src/main/kotlin/org/arend/psi/listener/ArendPsiChangeService.kt +++ b/src/main/kotlin/org/arend/psi/listener/ArendPsiChangeService.kt @@ -22,8 +22,10 @@ class ArendPsiChangeService { } fun updateDefinition(def: PsiConcreteReferable, file: ArendFile, isExternalUpdate: Boolean) { - for (listener in listeners) { - listener.updateDefinition(def, file, isExternalUpdate) + synchronized(listeners) { + for (listener in listeners) { + listener.updateDefinition(def, file, isExternalUpdate) + } } } -} \ No newline at end of file +} diff --git a/src/main/kotlin/org/arend/yaml/YamlFileService.kt b/src/main/kotlin/org/arend/yaml/YamlFileService.kt index 3587f108c..65f9ac790 100644 --- a/src/main/kotlin/org/arend/yaml/YamlFileService.kt +++ b/src/main/kotlin/org/arend/yaml/YamlFileService.kt @@ -1,5 +1,7 @@ package org.arend.yaml +import com.intellij.openapi.application.ApplicationManager +import com.intellij.openapi.module.Module import com.intellij.openapi.module.ModuleUtilCore import com.intellij.openapi.project.Project import com.intellij.openapi.vfs.VirtualFile diff --git a/src/main/kotlin/org/arend/yaml/YamlNotificationProvider.kt b/src/main/kotlin/org/arend/yaml/YamlNotificationProvider.kt index 8969fee3c..2b8bc039d 100644 --- a/src/main/kotlin/org/arend/yaml/YamlNotificationProvider.kt +++ b/src/main/kotlin/org/arend/yaml/YamlNotificationProvider.kt @@ -1,5 +1,6 @@ package org.arend.yaml +import com.intellij.openapi.application.ApplicationManager import com.intellij.openapi.components.service import com.intellij.openapi.fileEditor.FileEditor import com.intellij.openapi.project.Project @@ -28,7 +29,13 @@ class YamlNotificationProvider : EditorNotificationProvider { panel.createActionLabel(ArendBundle.message("arend.updateYamlConfiguration")) { panel.isVisible = false yamlFileService.removeChangedFile(file) - yamlFileService.updateIdea(file) + ApplicationManager.getApplication().run { + executeOnPooledThread { + runReadAction { + yamlFileService.updateIdea(file) + } + } + } } return panel } diff --git a/src/main/resources/META-INF/plugin.xml b/src/main/resources/META-INF/plugin.xml index b96310490..1a2aa211d 100644 --- a/src/main/resources/META-INF/plugin.xml +++ b/src/main/resources/META-INF/plugin.xml @@ -553,13 +553,6 @@ - - - - - + + + diff --git a/src/main/resources/inspectionDescriptions/UnresolvedArendPattern.html b/src/main/resources/inspectionDescriptions/UnresolvedArendPattern.html index 9cf639c68..184c9b13f 100644 --- a/src/main/resources/inspectionDescriptions/UnresolvedArendPattern.html +++ b/src/main/resources/inspectionDescriptions/UnresolvedArendPattern.html @@ -1,5 +1,5 @@ -Reports patterns that don't resolve into constructors +Reports patterns that do not resolve into constructors \ No newline at end of file diff --git a/src/main/resources/intentionDescriptions/ReplaceBracketsIntention/description.html b/src/main/resources/intentionDescriptions/ReplaceBracketsIntention/description.html index 6c66b7a7c..f2086992e 100644 --- a/src/main/resources/intentionDescriptions/ReplaceBracketsIntention/description.html +++ b/src/main/resources/intentionDescriptions/ReplaceBracketsIntention/description.html @@ -1,5 +1,5 @@ -Replaces the brackets associated with this element from "(" and ") to "{" and "}" and vice versa +Replaces the brackets or the parentheses associated with this element from "(" and ") to "{" and "}" and vice versa \ No newline at end of file diff --git a/src/main/resources/messages/ArendBundle.properties b/src/main/resources/messages/ArendBundle.properties index 5bfd7a27f..7b6568a6c 100644 --- a/src/main/resources/messages/ArendBundle.properties +++ b/src/main/resources/messages/ArendBundle.properties @@ -199,7 +199,8 @@ arend.refactoring.move.unspecifiedPartOfTheClass=Unspecified part of the class arend.changeSignature.ambientError=Typechecking error in the expression or its parent arend.changeSignature.parseError=Unable to parse expression correctly -arend.replaceBrackets=Replace the brackets +arend.replaceBrackets=Replace with brackets +arend.replaceParentheses=Replace with parentheses arend.updateYamlConfigurationQuestion=Would you like to update the settings from the YAML file? arend.updateYamlConfiguration=Update diff --git a/src/test/kotlin/org/arend/intention/ReplaceBracketsIntentionTest.kt b/src/test/kotlin/org/arend/intention/ReplaceBracketsIntentionTest.kt index abf18cd6c..dce3c1706 100644 --- a/src/test/kotlin/org/arend/intention/ReplaceBracketsIntentionTest.kt +++ b/src/test/kotlin/org/arend/intention/ReplaceBracketsIntentionTest.kt @@ -4,15 +4,17 @@ import org.arend.quickfix.QuickFixTestBase import org.arend.util.ArendBundle class ReplaceBracketsIntentionTest : QuickFixTestBase() { - private val fixName = ArendBundle.message("arend.replaceBrackets") - private fun doTest(contents: String, result: String) = simpleQuickFixTest(fixName, contents, result) + private val fixNameBrackets = ArendBundle.message("arend.replaceBrackets") + private val fixNameParentheses = ArendBundle.message("arend.replaceParentheses") + private fun doTestBrackets(contents: String, result: String) = simpleQuickFixTest(fixNameBrackets, contents, result) + private fun doTestParentheses(contents: String, result: String) = simpleQuickFixTest(fixNameParentheses, contents, result) - fun testReplaceBrackets1() = doTest( + fun testReplaceBrackets() = doTestBrackets( """\func foo ({-caret-}a : Nat) => 1""", """\func foo {a : Nat} => 1""" ) - fun testReplaceBrackets2() = doTest( + fun testReplaceParentheses() = doTestParentheses( """ \func foo (a : Nat) => 1 \func bar => foo {{-caret-}foo 0}