Merge pull request #846 from thery/depth

set the default max depth = coq max depth

client/goal-view-ui/src/App.tsx

@@ -4,12 +4,15 @@ import "./App.css";
 import ProofViewPage from './components/templates/ProovViewPage';
 import {Goal, ProofViewGoals, ProofViewGoalsKey, ProofViewMessage} from './types';
 
+import { vscode } from "./utilities/vscode";
+
 const app = () => {
 
   const [goals, setGoals] = useState<ProofViewGoals>(null);
   const [messages, setMessages] = useState<ProofViewMessage[]>([]);
   const [goalDisplaySetting, setGoalDisplaySetting] = useState<string>("List");
   const [goalDepth, setGoalDepth] = useState<number>(10);
+  const [helpMessage, setHelpMessage] = useState<string>("");
 
   const handleMessage = useCallback ((msg: any) => {
     switch (msg.data.command) {
@@ -66,9 +69,24 @@ const app = () => {
         });
     };
 
+    const settingsClickHandler = () => {
+        vscode.postMessage({
+            command: "openGoalSettings",
+        });
+    };
+
   return (
     <main>
-        <ProofViewPage goals={goals} messages={messages} collapseGoalHandler={collapseGoalHandler} displaySetting={goalDisplaySetting} maxDepth={goalDepth}/>
+        <ProofViewPage 
+            goals={goals} 
+            messages={messages} 
+            collapseGoalHandler={collapseGoalHandler} 
+            displaySetting={goalDisplaySetting} 
+            maxDepth={goalDepth} 
+            settingsClickHandler={settingsClickHandler}
+            helpMessage={helpMessage}
+            helpMessageHandler={(message: string) => setHelpMessage(message)}
+        />
     </main>
   );
 };

client/goal-view-ui/src/components/atoms/Goal.tsx

@@ -1,20 +1,33 @@
-import React, {FunctionComponent} from 'react';
+import React, {FunctionComponent, MouseEvent, KeyboardEvent} from 'react';
 
 import classes from './PpString.module.css';
 import { PpString } from '../../types';
 import PpDisplay from '../../utilities/pp';
 
 type GoalProps = {
     goal: PpString,
-    maxDepth: number
+    maxDepth: number,
+    setHelpMessage: (message: string) => void;
 };
 
 const goal : FunctionComponent<GoalProps> = (props) => {
 
-    const {goal, maxDepth} = props;
+    const {goal, maxDepth, setHelpMessage} = props;
 
     return (
-        <div className={classes.Goal}>
+        <div 
+            className={classes.Goal} 
+            onMouseOver={() => {
+                if(setHelpMessage !== undefined) {
+                    setHelpMessage("Click on the window and keep Alt pressed in to enable term eliding/expanding.");
+                }
+            }}
+            onMouseOut={() => {
+                if(setHelpMessage !== undefined) {
+                    setHelpMessage("");
+                }
+            }}
+        >
             <PpDisplay 
                 pp={goal}
                 coqCss={classes}

client/goal-view-ui/src/components/molecules/CollapsibleGoalBlock.tsx

@@ -9,16 +9,17 @@ type CollapsibleGoalBlockProps = {
     collapseHandler: (id: string) => void, 
     goalIndex: number,
     goalIndicator: string,
-    maxDepth: number
+    maxDepth: number,
+    helpMessageHandler: (message: string) => void
 };
 
 const collapsibleGoalBlock: FunctionComponent<CollapsibleGoalBlockProps> = (props) => {
 
-    const {goal, goalIndex, goalIndicator, collapseHandler, maxDepth} = props;
+    const {goal, goalIndex, goalIndicator, collapseHandler, maxDepth, helpMessageHandler} = props;
 
     return (
         <Accordion title={"Goal " + goalIndex} collapsed={!goal.isOpen} collapseHandler={() => collapseHandler(goal.id)}>
-            <GoalBlock goal={goal} goalIndicator={goalIndicator} maxDepth={maxDepth}/>
+            <GoalBlock goal={goal} goalIndicator={goalIndicator} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler}/>
         </Accordion>
     );
 

client/goal-view-ui/src/components/molecules/GoalBlock.tsx

@@ -12,19 +12,20 @@ import { Goal } from '../../types';
 type GoalBlockProps = {
     goal: Goal
     goalIndicator?: string,
-    maxDepth: number
+    maxDepth: number,
+    helpMessageHandler: (message: string) => void
 };
 
 const goalBlock: FunctionComponent<GoalBlockProps> = (props) => {
 
-    const {goal, goalIndicator, maxDepth} = props;
+    const {goal, goalIndicator, maxDepth, helpMessageHandler} = props;
     const indicator = goalIndicator ? <span className={classes.GoalIndex} >({goalIndicator})</span> : null;
 
     return (
         <div className={classes.Block}>
             <HypothesesBlock hypotheses={goal.hypotheses} maxDepth={maxDepth}/>
             <div className={classes.SeparatorZone}> {indicator} <Separator /> </div>
-            <GoalComponent goal={goal.goal} maxDepth={maxDepth}/>
+            <GoalComponent goal={goal.goal} maxDepth={maxDepth} setHelpMessage={helpMessageHandler}/>
         </div>
     );
 };

client/goal-view-ui/src/components/organisms/GoalCollapsibles.tsx

@@ -8,12 +8,13 @@ import classes from './GoalCollapsibles.module.css';
 type GoalSectionProps = {
     goals: CollapsibleGoal[],
     collapseGoalHandler: (id: string) => void,
-    maxDepth: number
+    maxDepth: number,
+    helpMessageHandler: (message: string) => void
 };
 
 const goalSection: FunctionComponent<GoalSectionProps> = (props) => {
 
-    const {goals, collapseGoalHandler, maxDepth} = props;
+    const {goals, collapseGoalHandler, maxDepth, helpMessageHandler} = props;
     const firstGoalRef = useRef<HTMLDivElement>(null);
 
     useEffect(() => {
@@ -35,14 +36,14 @@ const goalSection: FunctionComponent<GoalSectionProps> = (props) => {
         if(index === 0) {
             return (
                 <>
-                    <CollapsibleGoalBlock goal={goal} goalIndex={index + 1} goalIndicator={index + 1 + " / " + goals.length} collapseHandler={collapseGoalHandler} maxDepth={maxDepth}/>
+                    <CollapsibleGoalBlock goal={goal} goalIndex={index + 1} goalIndicator={index + 1 + " / " + goals.length} collapseHandler={collapseGoalHandler} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler}/>
                     <div ref={firstGoalRef}/>
                 </>
             );
         }
 
         return (
-            <CollapsibleGoalBlock goal={goal} goalIndex={index + 1} goalIndicator={index + 1 + " / " + goals.length} collapseHandler={collapseGoalHandler} maxDepth={maxDepth}/>
+            <CollapsibleGoalBlock goal={goal} goalIndex={index + 1} goalIndicator={index + 1 + " / " + goals.length} collapseHandler={collapseGoalHandler} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler}/>
         );
     });
 

client/goal-view-ui/src/components/organisms/GoalSection.tsx

@@ -14,11 +14,12 @@ type GoalSectionProps = {
     emptyMessage: string;
     emptyIcon?: JSX.Element;
     maxDepth: number;
+    helpMessageHandler: (message: string) => void;
 };
 
 const goalSection: FunctionComponent<GoalSectionProps> = (props) => {
 
-    const {goals, collapseGoalHandler, displaySetting, emptyMessage, emptyIcon, maxDepth} = props;
+    const {goals, collapseGoalHandler, displaySetting, emptyMessage, emptyIcon, maxDepth, helpMessageHandler} = props;
     const emptyMessageRef = useRef<HTMLDivElement>(null);
 
     useEffect(() => {
@@ -42,8 +43,8 @@ const goalSection: FunctionComponent<GoalSectionProps> = (props) => {
             <div ref={emptyMessageRef}/>
         </>
     : displaySetting === 'Tabs' ?
-        <GoalTabSection goals={goals} maxDepth={maxDepth} />
-        : <GoalCollapsibleSection goals={goals} collapseGoalHandler={collapseGoalHandler} maxDepth={maxDepth}/>;
+        <GoalTabSection goals={goals} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler}/>
+        : <GoalCollapsibleSection goals={goals} collapseGoalHandler={collapseGoalHandler} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler}/>;
 
     return section;
 };

client/goal-view-ui/src/components/organisms/GoalTabs.tsx

@@ -12,12 +12,13 @@ import classes from './GoalTabs.module.css';
 
 type GoalSectionProps = {
     goals: Goal[];
-    maxDepth: number
+    maxDepth: number;
+    helpMessageHandler: (message: string) => void;
 };
 
 const goalSection: FunctionComponent<GoalSectionProps> = (props) => {
 
-    const {goals, maxDepth} = props;
+    const {goals, maxDepth, helpMessageHandler} = props;
     const goalRefs = useRef<Array<HTMLDivElement | null>>([]);
     useLayoutEffect(() => {
         goalRefs.current = goalRefs.current.slice(0, goals.length);
@@ -50,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}/>
+                <GoalBlock goal={goal} goalIndicator={index + 1 + " / " + goals.length} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler}/>
                 <div ref={el => goalRefs.current[index] = el}/>
             </VSCodePanelView>
         );

client/goal-view-ui/src/components/templates/GoalPage.module.css

@@ -3,13 +3,33 @@
     width: 100%;
 }
 
+.ButtonContainer {
+    display: flex;
+    justify-content: space-between;
+    align-items: center;
+    width: 100%;
+    height: fit-content;
+    margin-bottom: 12px;
+}
+
+.HelpMessage {
+    font-style: italic;
+    opacity: .4;
+    font-size: 12px;
+    text-overflow: ellipsis;
+    flex-basis: auto;
+    overflow: hidden;
+    white-space: nowrap;
+}
+
 .Panel {
     display: flex;
     flex-direction: column;
     width: 100%;
     overflow: auto;
 }
 
+
 .View {
     width: 100%;
 }

client/goal-view-ui/src/components/templates/ProovViewPage.tsx

@@ -4,9 +4,12 @@ import {
     VSCodeBadge, 
     VSCodePanels, 
     VSCodePanelTab, 
-    VSCodePanelView 
+    VSCodePanelView,
+    VSCodeButton
 } from '@vscode/webview-ui-toolkit/react';
 
+import { VscGear } from 'react-icons/vsc';
+
 import GoalSection from '../organisms/GoalSection';
 import EmptyState from '../atoms/EmptyState';
 import Accordion from '../atoms/Accordion';
@@ -22,11 +25,14 @@ type ProofViewPageProps = {
     collapseGoalHandler: (id: string, key: ProofViewGoalsKey) => void,
     displaySetting: string;
     maxDepth: number;
+    settingsClickHandler: () => void;
+    helpMessage: string;
+    helpMessageHandler: (message: string) => void;
 };
 
 const proofViewPage: FunctionComponent<ProofViewPageProps> = (props) => {
 
-    const {goals, messages, displaySetting, collapseGoalHandler, maxDepth} = props;
+    const {goals, messages, displaySetting, collapseGoalHandler, maxDepth, settingsClickHandler, helpMessage, helpMessageHandler} = props;
 
     const renderGoals = () => {
         const goalBadge = <VSCodeBadge>{goals!.main.length}</VSCodeBadge>;
@@ -55,6 +61,7 @@ const proofViewPage: FunctionComponent<ProofViewPageProps> = (props) => {
                         goals!.shelved.length === 0 && goals!.givenUp.length === 0 ? <VscPass /> : <VscWarning />
                     }
                     maxDepth={maxDepth}
+                    helpMessageHandler={helpMessageHandler}
                 /> 
             </VSCodePanelView>,
             <VSCodePanelView className={classes.View}> 
@@ -65,6 +72,7 @@ const proofViewPage: FunctionComponent<ProofViewPageProps> = (props) => {
                     displaySetting={displaySetting}
                     emptyMessage='There are no shelved goals'
                     maxDepth={maxDepth}
+                    helpMessageHandler={helpMessageHandler}
                 /> 
             </VSCodePanelView>,
             <VSCodePanelView className={classes.View}> 
@@ -75,6 +83,7 @@ const proofViewPage: FunctionComponent<ProofViewPageProps> = (props) => {
                     displaySetting={displaySetting}
                     emptyMessage='There are no given up goals'
                     maxDepth={maxDepth}
+                    helpMessageHandler={helpMessageHandler}
                 /> 
             </VSCodePanelView>
         ];
@@ -99,6 +108,22 @@ const proofViewPage: FunctionComponent<ProofViewPageProps> = (props) => {
 
     return (
         <div className={classes.Page}>
+            <div className={classes.ButtonContainer}>
+                <div className={classes.HelpMessage}>{helpMessage}</div>
+                <VSCodeButton 
+                    appearance={'icon'} 
+                    onClick={settingsClickHandler}
+                    onMouseOver={() => {
+                        helpMessageHandler("Open proof view panel settings.");
+                    }}
+                    onMouseOut={() => {
+                        helpMessageHandler("");
+                    }}
+                    aria-label='Settings'
+                >
+                    <VscGear/>
+                </VSCodeButton>
+            </div>
             <Accordion title={'Proof'} collapsed={false}>
                 {collapsibleGoalsDisplay}
             </Accordion>

client/goal-view-ui/src/utilities/pp-box.tsx

@@ -8,13 +8,17 @@ interface PpBoxProps extends Box {
     breaks: BreakInfo[],
     maxDepth: number,
     hide: boolean,
-    hovered: boolean
+    hovered: boolean,
+    addedDepth: number,
 }
 
+const ADDED_DEPTH_FACTOR = 10;
+
 const PpBox: FunctionComponent<PpBoxProps> = (props) => {
 
-    const {mode, depth, coqCss, id, indent, breaks, boxChildren, hovered, maxDepth} = props;
+    const {mode, depth, coqCss, id, indent, breaks, boxChildren, hovered, maxDepth, addedDepth} = props;
     const [hide, setHide] = useState<boolean>(depth >= maxDepth);
+    const [depthOpen, setDepthOpen] = useState<number>(addedDepth);
 
     const ellpisis = (
         <span className={classes.Ellipsis}>
@@ -40,6 +44,7 @@ const PpBox: FunctionComponent<PpBoxProps> = (props) => {
                         indent={child.indent}
                         breaks={breaks}
                         boxChildren={child.boxChildren}
+                        addedDepth={addedDepth + depthOpen}
                     />
                 );
             } else if (child.type === DisplayType.break) {
@@ -73,7 +78,16 @@ const PpBox: FunctionComponent<PpBoxProps> = (props) => {
             className={classNames.join(' ')}
             onClick={(e) => {
                 e.stopPropagation();
-                if(e.altKey) { setHide(!hide); };
+                if(e.altKey) { 
+                    if(hide) {
+                        setDepthOpen(depthOpen + ADDED_DEPTH_FACTOR);
+                        setHide(false);
+                    }
+                    else {
+                        setDepthOpen(Math.max(depthOpen - ADDED_DEPTH_FACTOR, 0));
+                        setHide(true);
+                    }
+                };
             }}
         >
             {inner}

client/goal-view-ui/src/utilities/pp.tsx

@@ -361,6 +361,7 @@ const ppDisplay : FunctionComponent<PpProps> = (props) => {
                         boxChildren={displayState.display.boxChildren}
                         indent={displayState.display.indent}
                         breaks={displayState.breakIds}
+                        addedDepth={0}
                     />
                     : null
                 }

client/package.json

@@ -148,7 +148,7 @@
           },
           "vscoq.goals.maxDepth": {
             "type": "number",
-            "default": 10,
+            "default": 17,
             "markdownDescription": "The maximum depth in goals over which an ellipsis will be displayed (instead of the sub-terms)."
           }
         }

client/src/panels/GoalPanel.ts

@@ -1,4 +1,4 @@
-import { Disposable, Webview, WebviewPanel, window, workspace, Uri, ViewColumn, TextEditor, Position } from "vscode";
+import { Disposable, Webview, WebviewPanel, window, workspace, Uri, ViewColumn, TextEditor, Position, commands } from "vscode";
 import { ProofViewNotification } from '../protocol/types';
 import { getUri } from "../utilities/getUri";
 import { getNonce } from "../utilities/getNonce";
@@ -238,6 +238,8 @@ export default class GoalPanel {
         const text = message.text;
 
         switch (command) {
+            case 'openGoalSettings':
+                commands.executeCommand('workbench.action.openSettings', 'vscoq.goals');
             // Add more switch case statements here as more webview message commands
             // are created within the webview context (i.e. inside media/main.js)
         }