Skip to content

Commit

Permalink
feat: display the next unfocused goals
Browse files Browse the repository at this point in the history
  • Loading branch information
rtetley committed Sep 13, 2024
1 parent eaba783 commit 1e4f634
Show file tree
Hide file tree
Showing 5 changed files with 32 additions and 9 deletions.
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
.EmptyStateSection {
display: flex;
flex-direction: row;
justify-content: space-between;
align-items: flex-start;
align-content: center;
}
Expand Down
Original file line number Diff line number Diff line change
@@ -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;
}
20 changes: 15 additions & 5 deletions client/goal-view-ui/src/components/organisms/GoalSection.tsx
Original file line number Diff line number Diff line change
@@ -1,25 +1,26 @@
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[],
collapseGoalHandler: (id: string) => void,
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(() => {
Expand All @@ -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}/>;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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={
Expand Down
3 changes: 2 additions & 1 deletion client/goal-view-ui/src/types.ts
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,8 @@ export type ProofViewGoalsType = {
export enum ProofViewGoalsKey {
main = "main",
shelved = "shelved",
givenUp = "givenUp"
givenUp = "givenUp",
unfocused = "unfocused"
}

export enum MessageSeverity {
Expand Down

0 comments on commit 1e4f634

Please sign in to comment.