From 1e4f634c7f10865e50e4ef9753691731baaf38fb Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Fri, 13 Sep 2024 11:44:22 +0200
Subject: [PATCH] feat: display the next unfocused goals

---
 .../components/atoms/EmptyState.module.css    |  1 -
 .../organisms/GoalSection.module.css          | 12 +++++++++++
 .../src/components/organisms/GoalSection.tsx  | 20 ++++++++++++++-----
 .../components/templates/ProovViewPage.tsx    |  5 +++--
 client/goal-view-ui/src/types.ts              |  3 ++-
 5 files changed, 32 insertions(+), 9 deletions(-)
 create mode 100644 client/goal-view-ui/src/components/organisms/GoalSection.module.css

diff --git a/client/goal-view-ui/src/components/atoms/EmptyState.module.css b/client/goal-view-ui/src/components/atoms/EmptyState.module.css
index 82dbf1c13..063d0dbf1 100644
--- a/client/goal-view-ui/src/components/atoms/EmptyState.module.css
+++ b/client/goal-view-ui/src/components/atoms/EmptyState.module.css
@@ -1,7 +1,6 @@
 .EmptyStateSection {
     display: flex;
     flex-direction: row;
-    justify-content: space-between;
     align-items: flex-start;
     align-content: center;
 }
diff --git a/client/goal-view-ui/src/components/organisms/GoalSection.module.css b/client/goal-view-ui/src/components/organisms/GoalSection.module.css
new file mode 100644
index 000000000..ae16a2447
--- /dev/null
+++ b/client/goal-view-ui/src/components/organisms/GoalSection.module.css
@@ -0,0 +1,12 @@
+.UnfocusedView {
+    display: flex;
+    flex-direction: column;
+    width: 100%;
+}
+
+.HintText {
+    font-style: italic;
+    font-family: var(--vscode-editor-fonont-family);
+    font-size: small;
+    opacity: 0.5;
+}
\ No newline at end of file
diff --git a/client/goal-view-ui/src/components/organisms/GoalSection.tsx b/client/goal-view-ui/src/components/organisms/GoalSection.tsx
index a1ee5d7e0..2598cd63e 100644
--- a/client/goal-view-ui/src/components/organisms/GoalSection.tsx
+++ b/client/goal-view-ui/src/components/organisms/GoalSection.tsx
@@ -1,11 +1,11 @@
-import React, {FunctionComponent, ReactNode, useEffect, useRef, useState} from 'react';
-import { VscPass } from 'react-icons/vsc';
+import React, {FunctionComponent, useEffect, useRef} from 'react';
 
 import GoalCollapsibleSection from './GoalCollapsibles';
 import GoalTabSection from './GoalTabs';
 import EmptyState from '../atoms/EmptyState';
 import { CollapsibleGoal } from '../../types';
 
+import classes from './GoalSection.module.css';
 
 type GoalSectionProps = {
     goals: CollapsibleGoal[],
@@ -13,13 +13,14 @@ type GoalSectionProps = {
     displaySetting: string;
     emptyMessage: string;
     emptyIcon?: JSX.Element;
+    unfocusedGoals?: CollapsibleGoal[],
     maxDepth: number;
     helpMessageHandler: (message: string) => void;
 };
 
 const goalSection: FunctionComponent<GoalSectionProps> = (props) => {
     
-    const {goals, collapseGoalHandler, displaySetting, emptyMessage, emptyIcon, maxDepth, helpMessageHandler} = props;
+    const {goals, collapseGoalHandler, displaySetting, unfocusedGoals, emptyMessage, emptyIcon, maxDepth, helpMessageHandler} = props;
     const emptyMessageRef = useRef<HTMLDivElement>(null);
 
     useEffect(() => {
@@ -38,10 +39,19 @@ const goalSection: FunctionComponent<GoalSectionProps> = (props) => {
     }
 
     const section = goals.length === 0 ?
-        <>
+        unfocusedGoals !== undefined && unfocusedGoals.length > 0 ?
+        <div className={classes.UnfocusedView}>
             <EmptyState message={emptyMessage} icon={emptyIcon} />
+            <div className={classes.HintText}>
+                Next unfocused goals (focus with bullet):
+            </div>
             <div ref={emptyMessageRef}/>
-        </>
+            <GoalCollapsibleSection goals={unfocusedGoals} collapseGoalHandler={collapseGoalHandler} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler} />
+        </div>
+        : <>
+            <EmptyState message={emptyMessage} icon={emptyIcon} />
+            <div ref={emptyMessageRef}/>
+          </>
     : displaySetting === 'Tabs' ?
         <GoalTabSection goals={goals} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler}/>
         : <GoalCollapsibleSection goals={goals} collapseGoalHandler={collapseGoalHandler} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler}/>;
diff --git a/client/goal-view-ui/src/components/templates/ProovViewPage.tsx b/client/goal-view-ui/src/components/templates/ProovViewPage.tsx
index 6825f4be3..46e6ce246 100644
--- a/client/goal-view-ui/src/components/templates/ProovViewPage.tsx
+++ b/client/goal-view-ui/src/components/templates/ProovViewPage.tsx
@@ -50,12 +50,13 @@ const proofViewPage: FunctionComponent<ProofViewPageProps> = (props) => {
                 <GoalSection 
                     key={"goals"}
                     goals={goals!.main}
-                    collapseGoalHandler={(id) => collapseGoalHandler(id, ProofViewGoalsKey.main)} 
+                    unfocusedGoals={goals!.unfocused}
+                    collapseGoalHandler={(id) => collapseGoalHandler(id, goals!.main.length ? ProofViewGoalsKey.main : ProofViewGoalsKey.unfocused)}
                     displaySetting={displaySetting}
                     emptyMessage={
                         goals!.shelved.length ? "There are shelved goals. Try using `Unshelve.`" :
                         goals!.givenUp.length ? "There are some goals you gave up. Go back and solve them, or use `Admitted.`" :
-                        goals!.unfocused.length ? "The subproof is complete, but there are some unfocused goals. Focus next goal with bullet -." :
+                        goals!.unfocused.length ? "The subproof is complete." :
                         "There are no more subgoals"
                     }
                     emptyIcon={
diff --git a/client/goal-view-ui/src/types.ts b/client/goal-view-ui/src/types.ts
index 43b0b13f9..866af31d4 100644
--- a/client/goal-view-ui/src/types.ts
+++ b/client/goal-view-ui/src/types.ts
@@ -22,7 +22,8 @@ export type ProofViewGoalsType = {
 export enum ProofViewGoalsKey {
     main = "main", 
     shelved = "shelved", 
-    givenUp = "givenUp"
+    givenUp = "givenUp",
+    unfocused = "unfocused"
 }
 
 export enum MessageSeverity {