Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove hypothesis display from goal list #962

Merged
merged 2 commits into from
Dec 11, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 23 additions & 9 deletions client/goal-view-ui/src/App.tsx
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
import React, {useState, useCallback, useEffect} from 'react';
import "./App.css";

import ProofViewPage from './components/templates/ProovViewPage';
import ProofViewPage from './components/templates/ProofViewPage';
import {Goal, ProofViewGoals, ProofViewGoalsKey, ProofViewMessage} from './types';

import { vscode } from "./utilities/vscode";
Expand Down Expand Up @@ -29,17 +29,17 @@ const app = () => {
setGoals(allGoals === null
? allGoals
: {
main: allGoals.goals.map((goal: Goal) => {
return {...goal, isOpen: true};
main: allGoals.goals.map((goal: Goal, index: number) => {
return {...goal, isOpen: true, isContextHidden: index !== 0};
}),
shelved: allGoals.shelvedGoals.map((goal: Goal) => {
return {...goal, isOpen: true};
shelved: allGoals.shelvedGoals.map((goal: Goal, index: number) => {
return {...goal, isOpen: true, isContextHidden: index !== 0};
}),
givenUp: allGoals.givenUpGoals.map((goal: Goal) => {
return {...goal, isOpen: true};
givenUp: allGoals.givenUpGoals.map((goal: Goal, index: number) => {
return {...goal, isOpen: true, isContextHidden: index !== 0};
}),
unfocused: allGoals.unfocusedGoals.map((goal: Goal) => {
return {...goal, isOpen: false};
unfocused: allGoals.unfocusedGoals.map((goal: Goal, index: number) => {
return {...goal, isOpen: false, isContextHidden: index !== 0};
})
}
);
Expand Down Expand Up @@ -72,6 +72,19 @@ const app = () => {
});
};

const toggleContext = (id: string, key: ProofViewGoalsKey) => {
const newGoals = goals![key].map(goal => {
if(goal.id === id){
return {...goal, isContextHidden: !goal.isContextHidden};
}
return goal;
});
setGoals({
...goals!,
[key]: newGoals
});
};

const settingsClickHandler = () => {
vscode.postMessage({
command: "openGoalSettings",
Expand All @@ -89,6 +102,7 @@ const app = () => {
settingsClickHandler={settingsClickHandler}
helpMessage={helpMessage}
helpMessageHandler={(message: string) => setHelpMessage(message)}
toggleContextHandler={toggleContext}
/>
</main>
);
Expand Down
18 changes: 14 additions & 4 deletions client/goal-view-ui/src/components/atoms/Accordion.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,13 @@ type AccordionProps = {
collapsed: boolean;
title: string;
collapseHandler?: (params: any) => void;
seconaryActionHandler?: (params: any) => void;
seconaryActionIcon?: JSX.Element;
};

const accordion: FunctionComponent<AccordionProps> = (props) => {

const {title, collapseHandler} = props;
const {title, collapseHandler, seconaryActionHandler, seconaryActionIcon} = props;
const [collapsed, setCollapsed] = useState(props.collapsed);
useEffect(() => {
setCollapsed(props.collapsed);
Expand All @@ -25,15 +27,23 @@ const accordion: FunctionComponent<AccordionProps> = (props) => {

const toggleCollapse = collapseHandler ? collapseHandler : () => setCollapsed(!collapsed);

const secondaryActionButton = (seconaryActionHandler !== undefined && seconaryActionIcon !== undefined) ? <VSCodeButton appearance={'icon'} onClick={seconaryActionHandler} className={classes.Demphasize}> {seconaryActionIcon} </VSCodeButton> : null;
const secondaryAction = collapsed ? null : secondaryActionButton;
const actionRow =
<div>
{secondaryAction}
<VSCodeButton appearance={'icon'} ariaLabel='Collapse' onClick={toggleCollapse}>
<VscChevronDown className={!collapsed ? [classes.Rotated, classes.Demphasize].join(' ') : ''} />
</VSCodeButton>
</div>;

return (
<div className={classes.Block}>

{/* The header with title and button */}
<div className={classes.Header}>
<span className={!collapsed ? classes.Demphasize : ''}>{title}</span>
<VSCodeButton appearance={'icon'} ariaLabel='Collapse' onClick={toggleCollapse}>
<VscChevronDown className={!collapsed ? [classes.Rotated, classes.Demphasize].join(' ') : ''} />
</VSCodeButton>
{actionRow}
</div>

{/* The panel that collapses */}
Expand Down
Original file line number Diff line number Diff line change
@@ -1,12 +1,15 @@
import React, {FunctionComponent} from 'react';

import { VscEye, VscEyeClosed } from 'react-icons/vsc';

import GoalBlock from './GoalBlock';
import Accordion from '../atoms/Accordion';
import { CollapsibleGoal } from '../../types';

type CollapsibleGoalBlockProps = {
goal: CollapsibleGoal,
collapseHandler: (id: string) => void,
collapseHandler: (id: string) => void,
toggleContextHandler: (id:string) => void,
goalIndex: number,
goalIndicator: string,
maxDepth: number,
Expand All @@ -15,11 +18,18 @@ type CollapsibleGoalBlockProps = {

const collapsibleGoalBlock: FunctionComponent<CollapsibleGoalBlockProps> = (props) => {

const {goal, goalIndex, goalIndicator, collapseHandler, maxDepth, helpMessageHandler} = props;
const {goal, goalIndex, goalIndicator, collapseHandler, toggleContextHandler, maxDepth, helpMessageHandler} = props;

const secondaryActionIcon = goal.isContextHidden ? <VscEye /> : <VscEyeClosed />;
const secondaryActionHandler = toggleContextHandler !== undefined ? () => toggleContextHandler(goal.id) : undefined;

return (
<Accordion title={"Goal " + goalIndex} collapsed={!goal.isOpen} collapseHandler={() => collapseHandler(goal.id)}>
<GoalBlock goal={goal} goalIndicator={goalIndicator} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler}/>
<Accordion title={"Goal " + goalIndex} collapsed={!goal.isOpen}
collapseHandler={() => collapseHandler(goal.id)}
seconaryActionHandler={secondaryActionHandler}
seconaryActionIcon={secondaryActionIcon}
>
<GoalBlock goal={goal} goalIndicator={goalIndicator} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler} displayHyps={!goal.isContextHidden}/>
</Accordion>
);

Expand Down
15 changes: 9 additions & 6 deletions client/goal-view-ui/src/components/molecules/GoalBlock.tsx
Original file line number Diff line number Diff line change
@@ -1,6 +1,4 @@
import React, {FunctionComponent} from 'react';
import {VSCodeButton} from '@vscode/webview-ui-toolkit/react';
import {VscChevronDown} from 'react-icons/vsc';

import HypothesesBlock from './HypothesesBlock';
import GoalComponent from '../atoms/Goal';
Expand All @@ -13,18 +11,23 @@ type GoalBlockProps = {
goal: Goal
goalIndicator?: string,
maxDepth: number,
helpMessageHandler: (message: string) => void
helpMessageHandler: (message: string) => void,
displayHyps: boolean
};

const goalBlock: FunctionComponent<GoalBlockProps> = (props) => {

const {goal, goalIndicator, maxDepth, helpMessageHandler} = props;
const {goal, goalIndicator, maxDepth, displayHyps, helpMessageHandler} = props;
const indicator = goalIndicator ? <span className={classes.GoalIndex} >({goalIndicator})</span> : null;
const hyps = displayHyps ? <HypothesesBlock hypotheses={goal.hypotheses} maxDepth={maxDepth}/> : null;

return (
<div className={classes.Block}>
<HypothesesBlock hypotheses={goal.hypotheses} maxDepth={maxDepth}/>
<div className={classes.SeparatorZone}> {indicator} <Separator /> </div>
{hyps}
<div className={classes.SeparatorZone}>
{indicator}
<Separator />
</div>
<GoalComponent goal={goal.goal} maxDepth={maxDepth} setHelpMessage={helpMessageHandler}/>
</div>
);
Expand Down
19 changes: 16 additions & 3 deletions client/goal-view-ui/src/components/organisms/GoalCollapsibles.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,14 @@ import classes from './GoalCollapsibles.module.css';
type GoalSectionProps = {
goals: CollapsibleGoal[],
collapseGoalHandler: (id: string) => void,
toggleContextHandler: (id: string) => void,
maxDepth: number,
helpMessageHandler: (message: string) => void
};

const goalSection: FunctionComponent<GoalSectionProps> = (props) => {

const {goals, collapseGoalHandler, maxDepth, helpMessageHandler} = props;
const {goals, collapseGoalHandler, toggleContextHandler, maxDepth, helpMessageHandler} = props;
const firstGoalRef = useRef<HTMLDivElement>(null);

useEffect(() => {
Expand All @@ -36,14 +37,26 @@ const goalSection: FunctionComponent<GoalSectionProps> = (props) => {
if(index === 0) {
return (
<>
<CollapsibleGoalBlock goal={goal} goalIndex={index + 1} goalIndicator={index + 1 + " / " + goals.length} collapseHandler={collapseGoalHandler} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler}/>
<CollapsibleGoalBlock
goal={goal} goalIndex={index + 1} goalIndicator={index + 1 + " / " + goals.length}
collapseHandler={collapseGoalHandler}
toggleContextHandler={toggleContextHandler}
helpMessageHandler={helpMessageHandler}
maxDepth={maxDepth}
/>
<div ref={firstGoalRef}/>
</>
);
}

return (
<CollapsibleGoalBlock goal={goal} goalIndex={index + 1} goalIndicator={index + 1 + " / " + goals.length} collapseHandler={collapseGoalHandler} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler}/>
<CollapsibleGoalBlock
goal={goal} goalIndex={index + 1} goalIndicator={index + 1 + " / " + goals.length}
collapseHandler={collapseGoalHandler}
toggleContextHandler={toggleContextHandler}
maxDepth={maxDepth}
helpMessageHandler={helpMessageHandler}
/>
);
});

Expand Down
16 changes: 12 additions & 4 deletions client/goal-view-ui/src/components/organisms/GoalSection.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,8 @@ import classes from './GoalSection.module.css';

type GoalSectionProps = {
goals: CollapsibleGoal[],
collapseGoalHandler: (id: string) => void,
collapseGoalHandler: (id: string) => void,
toggleContextHandler: (id: string) => void,
displaySetting: string;
emptyMessage: string;
emptyIcon?: JSX.Element;
Expand All @@ -20,7 +21,7 @@ type GoalSectionProps = {

const goalSection: FunctionComponent<GoalSectionProps> = (props) => {

const {goals, collapseGoalHandler, displaySetting, unfocusedGoals, emptyMessage, emptyIcon, maxDepth, helpMessageHandler} = props;
const {goals, collapseGoalHandler, toggleContextHandler, displaySetting, unfocusedGoals, emptyMessage, emptyIcon, maxDepth, helpMessageHandler} = props;
const emptyMessageRef = useRef<HTMLDivElement>(null);

useEffect(() => {
Expand All @@ -46,15 +47,22 @@ const goalSection: FunctionComponent<GoalSectionProps> = (props) => {
Next unfocused goals (focus with bullet):
</div>
<div ref={emptyMessageRef}/>
<GoalCollapsibleSection goals={unfocusedGoals} collapseGoalHandler={collapseGoalHandler} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler} />
<GoalCollapsibleSection goals={unfocusedGoals}
collapseGoalHandler={collapseGoalHandler}
toggleContextHandler={toggleContextHandler}
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}/>;
: <GoalCollapsibleSection goals={goals}
collapseGoalHandler={collapseGoalHandler}
maxDepth={maxDepth} helpMessageHandler={helpMessageHandler}
toggleContextHandler={toggleContextHandler}
/>;

return section;
};
Expand Down
2 changes: 1 addition & 1 deletion client/goal-view-ui/src/components/organisms/GoalTabs.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ const goalSection: FunctionComponent<GoalSectionProps> = (props) => {
const viewId = "view-" + index;
return (
<VSCodePanelView id={viewId} key={viewId}>
<GoalBlock goal={goal} goalIndicator={index + 1 + " / " + goals.length} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler}/>
<GoalBlock goal={goal} goalIndicator={index + 1 + " / " + goals.length} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler} displayHyps={true}/>
<div ref={el => goalRefs.current[index] = el}/>
</VSCodePanelView>
);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,9 +20,10 @@ import classes from './GoalPage.module.css';
import { VscPass, VscWarning } from 'react-icons/vsc';

type ProofViewPageProps = {
goals: ProofViewGoals,
messages: ProofViewMessage[],
collapseGoalHandler: (id: string, key: ProofViewGoalsKey) => void,
goals: ProofViewGoals;
messages: ProofViewMessage[];
collapseGoalHandler: (id: string, key: ProofViewGoalsKey) => void;
toggleContextHandler: (id: string, key: ProofViewGoalsKey) => void;
displaySetting: string;
maxDepth: number;
settingsClickHandler: () => void;
Expand All @@ -32,7 +33,11 @@ type ProofViewPageProps = {

const proofViewPage: FunctionComponent<ProofViewPageProps> = (props) => {

const {goals, messages, displaySetting, collapseGoalHandler, maxDepth, settingsClickHandler, helpMessage, helpMessageHandler} = props;
const {goals, messages, displaySetting,
collapseGoalHandler, maxDepth, settingsClickHandler,
helpMessage, helpMessageHandler,
toggleContextHandler,
} = props;

const renderGoals = () => {
const goalBadge = <VSCodeBadge>{goals!.main.length}</VSCodeBadge>;
Expand All @@ -52,6 +57,7 @@ const proofViewPage: FunctionComponent<ProofViewPageProps> = (props) => {
goals={goals!.main}
unfocusedGoals={goals!.unfocused}
collapseGoalHandler={(id) => collapseGoalHandler(id, goals!.main.length ? ProofViewGoalsKey.main : ProofViewGoalsKey.unfocused)}
toggleContextHandler={(id) => toggleContextHandler(id, goals!.main.length ? ProofViewGoalsKey.main : ProofViewGoalsKey.unfocused)}
displaySetting={displaySetting}
emptyMessage={
goals!.shelved.length ? "There are shelved goals. Try using `Unshelve.`" :
Expand All @@ -69,8 +75,9 @@ const proofViewPage: FunctionComponent<ProofViewPageProps> = (props) => {
<VSCodePanelView className={classes.View}>
<GoalSection
key="shelved"
goals={goals!.shelved}
collapseGoalHandler={(id) => collapseGoalHandler(id, ProofViewGoalsKey.shelved)}
goals={goals!.shelved}
collapseGoalHandler={(id) => collapseGoalHandler(id, ProofViewGoalsKey.shelved)}
toggleContextHandler={(id) => toggleContextHandler(id, ProofViewGoalsKey.shelved)}
displaySetting={displaySetting}
emptyMessage='There are no shelved goals'
maxDepth={maxDepth}
Expand All @@ -80,8 +87,9 @@ const proofViewPage: FunctionComponent<ProofViewPageProps> = (props) => {
<VSCodePanelView className={classes.View}>
<GoalSection
key="givenup"
goals={goals!.givenUp}
collapseGoalHandler={(id) => collapseGoalHandler(id, ProofViewGoalsKey.givenUp)}
goals={goals!.givenUp}
collapseGoalHandler={(id) => collapseGoalHandler(id, ProofViewGoalsKey.givenUp)}
toggleContextHandler={(id) => toggleContextHandler(id, ProofViewGoalsKey.givenUp)}
displaySetting={displaySetting}
emptyMessage='There are no given up goals'
maxDepth={maxDepth}
Expand Down
1 change: 1 addition & 0 deletions client/goal-view-ui/src/types.ts
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ export interface Goal {

export interface CollapsibleGoal extends Goal {
isOpen: boolean;
isContextHidden: boolean;
};

export type ProofViewGoalsType = {
Expand Down
Loading