proofsearch: fix #33

aya-prover · Dec 25, 2024 · b7748b4 · b7748b4
1 parent 3eb79c9
commit b7748b4
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/src/main/java/org/aya/intellij/actions/search/ProofSearch.java b/src/main/java/org/aya/intellij/actions/search/ProofSearch.java
@@ -98,6 +98,7 @@ private static boolean matches(@NotNull ProofShape ps, @NotNull Term term) {
   }
 
   static @NotNull Either<String, ProofShape> parse(@NotNull Project project, @NotNull String pattern) {
+    if (pattern.isBlank()) return Either.left("Pattern is empty");
     var reporter = new BufferReporter();
     try {
       var parser = new AyaIJParserImpl(project, reporter);

diff --git a/src/main/java/org/aya/intellij/psi/utils/AyaPsiFactory.java b/src/main/java/org/aya/intellij/psi/utils/AyaPsiFactory.java
@@ -25,7 +25,7 @@ public class AyaPsiFactory {
 
   public static @NotNull PsiElement expr(@NotNull Project project, @NotNull String text) {
     var fn = (AyaPsiFnDecl) file(project, "def a : " + text).getFirstChild();
-    return Objects.requireNonNull(Objects.requireNonNull(fn.getType()).getExpr());
+    return Objects.requireNonNull(Objects.requireNonNull(fn.getType()).getExpr(), text);
   }
 
   public static @NotNull AyaPsiQualifiedId qualifiedId(@NotNull Project project, @NotNull String text) {