Merge pull request #962 from coq/default-goal-display

Remove hypothesis display from goal list
coq · Dec 11, 2024 · 050c12d · 050c12d
2 parents c33919f + 59ecec2
commit 050c12d
Show file tree

Hide file tree

Showing 9 changed files with 106 additions and 39 deletions.
diff --git a/client/goal-view-ui/src/App.tsx b/client/goal-view-ui/src/App.tsx
@@ -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";
@@ -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};
                     })
                 }
             );
@@ -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",
@@ -89,6 +102,7 @@ const app = () => {
             settingsClickHandler={settingsClickHandler}
             helpMessage={helpMessage}
             helpMessageHandler={(message: string) => setHelpMessage(message)}
+            toggleContextHandler={toggleContext}
         />
     </main>
   );

diff --git a/client/goal-view-ui/src/components/atoms/Accordion.tsx b/client/goal-view-ui/src/components/atoms/Accordion.tsx
@@ -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);
@@ -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 */}

diff --git a/client/goal-view-ui/src/components/molecules/CollapsibleGoalBlock.tsx b/client/goal-view-ui/src/components/molecules/CollapsibleGoalBlock.tsx
@@ -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,
@@ -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>
     );
 

diff --git a/client/goal-view-ui/src/components/molecules/GoalBlock.tsx b/client/goal-view-ui/src/components/molecules/GoalBlock.tsx
@@ -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';
@@ -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>
     );

diff --git a/client/goal-view-ui/src/components/organisms/GoalCollapsibles.tsx b/client/goal-view-ui/src/components/organisms/GoalCollapsibles.tsx
@@ -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(() => {
@@ -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}
+            />
         );
     });
 

diff --git a/client/goal-view-ui/src/components/organisms/GoalSection.tsx b/client/goal-view-ui/src/components/organisms/GoalSection.tsx
@@ -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;
@@ -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(() => {
@@ -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;
 };

diff --git a/client/goal-view-ui/src/components/organisms/GoalTabs.tsx b/client/goal-view-ui/src/components/organisms/GoalTabs.tsx
@@ -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>
         );

diff --git a/...rc/components/templates/ProovViewPage.tsx → ...rc/components/templates/ProofViewPage.tsx b/...rc/components/templates/ProovViewPage.tsx → ...rc/components/templates/ProofViewPage.tsx
@@ -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;
@@ -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>;
@@ -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.`" :
@@ -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}
@@ -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}

diff --git a/client/goal-view-ui/src/types.ts b/client/goal-view-ui/src/types.ts
@@ -10,6 +10,7 @@ export interface Goal {
 
 export interface CollapsibleGoal extends Goal  {
     isOpen: boolean;
+    isContextHidden: boolean;
 };
 
 export type ProofViewGoalsType = {