Fix the scope in run configuration

JetBrains · Jul 4, 2024 · 31dad75 · 31dad75
1 parent 4648b84
commit 31dad75
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 42 deletions.
diff --git a/src/main/kotlin/org/arend/definition/ArendFileDefinitionScope.kt b/src/main/kotlin/org/arend/definition/ArendFileDefinitionScope.kt
diff --git a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckProcessHandler.kt
@@ -121,7 +121,7 @@ class TypeCheckProcessHandler(
 
                         val modulePaths = if (modulePath == null) library.loadedModules else listOf(modulePath)
                         val modules = modulePaths.mapNotNull {
-                            val module = library.config.findArendFile(it, withAdditional = false, withTests = command.isTest)
+                            val module = library.config.findArendFile(it, command.isTest)
                             if (module == null) {
                                 typecheckingErrorReporter.report(LibraryError.moduleNotFound(it, library.name))
                             } else if (command.definitionFullName == "") {

diff --git a/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt b/src/main/kotlin/org/arend/typechecking/execution/TypeCheckRunConfigurationEditor.kt
@@ -9,14 +9,14 @@ import com.intellij.ui.EditorTextField
 import com.intellij.ui.components.JBCheckBox
 import com.intellij.ui.dsl.builder.panel
 import org.arend.ArendFileTypeInstance
-import org.arend.definition.ArendFileDefinitionScope
 import org.arend.ext.module.ModulePath
 import org.arend.module.AllArendFilesScope
 import org.arend.module.AllModulesScope
 import org.arend.module.ArendPreludeLibrary.Companion.PRELUDE
 import org.arend.module.ArendPreludeScope
 import org.arend.module.config.ArendModuleConfigService
 import org.arend.naming.scope.EmptyScope
+import org.arend.naming.scope.LexicalScope
 import org.arend.psi.ArendFile
 import org.arend.psi.ext.PsiModuleReferable
 import org.arend.refactoring.move.ArendLongNameCodeFragment
@@ -57,7 +57,7 @@ class TypeCheckRunConfigurationEditor(private val project: Project) : SettingsEd
             }
             val arendFile = (moduleDocument.scope.resolveName(module) as? PsiModuleReferable)?.modules?.get(0) as? ArendFile?
                 ?: return@ArendLongNameCodeFragment EmptyScope.INSTANCE
-            ArendFileDefinitionScope(arendFile)
+            LexicalScope.opened(arendFile)
         })), project, ArendFileTypeInstance)
     }
 
@@ -84,9 +84,6 @@ class TypeCheckRunConfigurationEditor(private val project: Project) : SettingsEd
         aligned("$IS_TEST_TEXT:", isTestComponent)
         aligned("$MODULE_TEXT:", modulePathComponent)
         aligned("$DEFINITION_TEXT:", definitionNameComponent)
-        row {
-            text("If the definitions from the $MODULE_TEXT (Arend file) are not loaded, then either they are not there, or they have not loaded completely. Try opening the $MODULE_TEXT (Arend file) in the editor and re-view the list of definitions in the Run configuration window")
-        }
     }
 
     companion object {

diff --git a/src/main/kotlin/org/arend/typechecking/execution/configurations/TypeCheckRunState.kt b/src/main/kotlin/org/arend/typechecking/execution/configurations/TypeCheckRunState.kt
@@ -70,7 +70,7 @@ class TypeCheckRunState(private val environment: ExecutionEnvironment, private v
                 }
             } else {
                 if (command.definitionFullName == "") {
-                    val group = library?.getModuleGroup(modulePath, false) ?: library?.getModuleGroup(modulePath, true)
+                    val group = library?.getModuleGroup(modulePath, command.isTest)
                     if (library == null || group == null) {
                         NotificationErrorReporter(environment.project).report(ModuleNotFoundError(modulePath))
                         return null
@@ -83,7 +83,7 @@ class TypeCheckRunState(private val environment: ExecutionEnvironment, private v
                         }
                     }
                 } else {
-                    val scope = library?.moduleScopeProvider?.forModule(modulePath) ?: library?.testsModuleScopeProvider?.forModule(modulePath)
+                    val scope = if (command.isTest) library?.testsModuleScopeProvider?.forModule(modulePath) else library?.moduleScopeProvider?.forModule(modulePath)
                     if (library == null || scope == null) {
                         NotificationErrorReporter(environment.project).report(ModuleNotFoundError(modulePath))
                         return null