level completed message in editor

leanprover-community · Feb 14, 2024 · 3775ad9 · 3775ad9
1 parent 780514e
commit 3775ad9
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 2 deletions.
diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx
@@ -268,7 +268,7 @@ interface GoalsProps {
 
 export function Goals({ goals, filter }: GoalsProps) {
     if (goals.goals.length === 0) {
-        return <>No goals</>
+        return <></>
     } else {
         return <>
           {goals.goals.map((g, i) => <Goal typewriter={false} key={i} goal={g.goal} filter={filter} />)}

diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
@@ -232,7 +232,11 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
     ret = <div><p>{serverStoppedResult.message}</p><p className="error">{serverStoppedResult.reason}</p></div>
   } else {
     ret = <div className="infoview vscode-light">
-      {proof.completed && <div className="level-completed">Level completed! 🎉</div>}
+      {proof.completedWithWarnings &&
+        <div className="level-completed">
+          {proof.completed ? "Level completed! 🎉" : "Level completed with warnings 🎭"}
+        </div>
+      }
       <Infos />
       <Hints hints={proof.steps[curPos?.line]?.goals[0]?.hints}
         showHidden={showHelp.has(curPos?.line)} step={curPos?.line}

diff --git a/client/src/css/infoview.css b/client/src/css/infoview.css
@@ -41,6 +41,13 @@
 .level-completed {
   font-size: 1.8rem;
   font-weight: 500;
+  padding-left: .5em;
+  padding-right: .5em;
+  padding-top: .2em;
+  padding-bottom: .2em;
+  border-radius: .5em;
+  background-color: #eee;
+
 }
 
 .typewriter {