ide: display meta solution in pretty

plctlab · Jun 4, 2024 · fd42ae9 · fd42ae9
1 parent fb857d0
commit fd42ae9
Show file tree

Hide file tree

Showing 5 changed files with 15 additions and 7 deletions.
diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -74,6 +74,7 @@ public ExprTycker(@NotNull TyckState state, @NotNull Reporter reporter) {
   public void solveMetas() {
     state.solveMetas(reporter);
     withTerms.forEach(with -> with.data().theCoreType().update(this::freezeHoles));
+    userHoles.forEach(hole -> hole.data().solution().update(this::freezeHoles));
   }
 
   /**

diff --git a/cli-impl/src/main/java/org/aya/cli/literate/FaithfulPrettier.java b/cli-impl/src/main/java/org/aya/cli/literate/FaithfulPrettier.java
@@ -74,19 +74,21 @@ static void checkHighlights(@NotNull ImmutableSeq<HighlightInfo> highlights) {
       case HighlightInfo.Def def -> Doc.linkDef(highlightVar(raw, def.kind()), def.target(), hover(def.type()));
       case HighlightInfo.Ref ref -> Doc.linkRef(highlightVar(raw, ref.kind()), ref.target(), hover(ref.type()));
       case HighlightInfo.Lit lit -> highlightLit(raw, lit.kind());
-      case HighlightInfo.Err err -> {
-        var doc = doHighlight(StringSlice.of(raw), base, err.children());
-        var style = switch (err.problem().level()) {
+      case HighlightInfo.Err(var problem, var children) -> {
+        var doc = doHighlight(StringSlice.of(raw), base, children);
+        var style = switch (problem.level()) {
           case ERROR -> BasePrettier.ERROR;
           case WARN -> BasePrettier.WARNING;
           case GOAL -> BasePrettier.GOAL;
           case INFO -> null;
         };
         yield style == null ? doc : new Doc.Tooltip(Doc.styled(style, doc), () -> Doc.codeBlock(
           Language.Builtin.Aya,
-          err.problem().brief(options()).toDoc()
+          problem.brief(options()).toDoc()
         ));
       }
+      case HighlightInfo.UserMeta meta -> new Doc.Tooltip(Doc.plain(raw),
+        () -> Doc.codeBlock(Language.Builtin.Aya, meta.hover().toDoc(options())));
     };
   }
 

diff --git a/cli-impl/src/main/java/org/aya/cli/literate/HighlightInfo.java b/cli-impl/src/main/java/org/aya/cli/literate/HighlightInfo.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.cli.literate;
 
@@ -88,4 +88,7 @@ record Err(
 
   /** A literal */
   record Lit(@NotNull SourcePos sourcePos, @NotNull LitKind kind) implements HighlightInfo { }
+
+  /** Usually metavariables */
+  record UserMeta(@NotNull SourcePos sourcePos, @NotNull AyaDocile hover) implements HighlightInfo { }
 }
diff --git a/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java b/cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java
@@ -92,7 +92,8 @@ else if (SPECIAL_SYMBOL.contains(tokenType))
       case Expr.LitInt _ -> info.append(LitKind.Int.toLit(pos));
       case Expr.LitString _ -> info.append(LitKind.String.toLit(pos));
       case Expr.Hole hole when hole.filling() == null -> {
-        // info.append();
+        var hover = hole.solution().get();
+        if (hover != null) info.append(new HighlightInfo.UserMeta(pos, hover));
       }
       default -> StmtVisitor.super.visitExpr(pos, expr);
     }

diff --git a/ide-lsp/src/main/java/org/aya/lsp/models/HighlightResult.java b/ide-lsp/src/main/java/org/aya/lsp/models/HighlightResult.java
@@ -64,8 +64,9 @@ public record Symbol(
           case Prim -> Option.some(Kind.PrimRef);
           case Unknown -> Option.none();
         };
-        case HighlightInfo.Lit _ -> Option.none();   // handled by client
+        case HighlightInfo.Lit _ -> Option.none(); // handled by client
         case HighlightInfo.Err _ -> Option.none(); // handled by client
+        case HighlightInfo.UserMeta _ -> Option.none(); // handled by something else
       };
     }
   }