Skip to content

Commit c9cdb8b

Browse files
rtetleyrtetley
authored
Merge pull request #834 from coq-community/ellipsis
Ellipsis
2 parents 83d4fed + 3af6d5b commit c9cdb8b

18 files changed

+164
-51
lines changed

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

+5-1
Original file line numberDiff line numberDiff line change
@@ -9,12 +9,16 @@ const app = () => {
99
const [goals, setGoals] = useState<ProofViewGoals>(null);
1010
const [messages, setMessages] = useState<ProofViewMessage[]>([]);
1111
const [goalDisplaySetting, setGoalDisplaySetting] = useState<string>("List");
12+
const [goalDepth, setGoalDepth] = useState<number>(10);
1213

1314
const handleMessage = useCallback ((msg: any) => {
1415
switch (msg.data.command) {
1516
case 'updateDisplaySettings':
1617
setGoalDisplaySetting(msg.data.text);
1718
break;
19+
case 'updateGoalDepth':
20+
setGoalDepth(msg.data.text);
21+
break;
1822
case 'renderProofView':
1923
const allGoals = msg.data.proofView.proof;
2024
const messages = msg.data.proofView.messages;
@@ -64,7 +68,7 @@ const app = () => {
6468

6569
return (
6670
<main>
67-
<ProofViewPage goals={goals} messages={messages} collapseGoalHandler={collapseGoalHandler} displaySetting={goalDisplaySetting}/>
71+
<ProofViewPage goals={goals} messages={messages} collapseGoalHandler={collapseGoalHandler} displaySetting={goalDisplaySetting} maxDepth={goalDepth}/>
6872
</main>
6973
);
7074
};

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

+4-2
Original file line numberDiff line numberDiff line change
@@ -5,18 +5,20 @@ import { PpString } from '../../types';
55
import PpDisplay from '../../utilities/pp';
66

77
type GoalProps = {
8-
goal: PpString,
8+
goal: PpString,
9+
maxDepth: number
910
};
1011

1112
const goal : FunctionComponent<GoalProps> = (props) => {
1213

13-
const {goal} = props;
14+
const {goal, maxDepth} = props;
1415

1516
return (
1617
<div className={classes.Goal}>
1718
<PpDisplay
1819
pp={goal}
1920
coqCss={classes}
21+
maxDepth={maxDepth}
2022
/>
2123
</div>
2224
);

‎client/goal-view-ui/src/components/atoms/Hypothesis.tsx

+3-1
Original file line numberDiff line numberDiff line change
@@ -6,17 +6,19 @@ import PpDisplay from '../../utilities/pp';
66

77
type HypothesisProps = {
88
content: Hyp;
9+
maxDepth: number;
910
};
1011

1112
const hypothesis: FunctionComponent<HypothesisProps> = (props) => {
1213

13-
const {content} = props;
14+
const {content, maxDepth} = props;
1415

1516
return (
1617
<div className={classes.Hypothesis}>
1718
<PpDisplay
1819
pp={content}
1920
coqCss={classes}
21+
maxDepth={maxDepth}
2022
/>
2123
</div>
2224
);

‎client/goal-view-ui/src/components/atoms/Message.tsx

+4-2
Original file line numberDiff line numberDiff line change
@@ -6,12 +6,13 @@ import PpDisplay from '../../utilities/pp';
66

77
type MessageProps = {
88
message: PpString,
9-
severity: MessageSeverity
9+
severity: MessageSeverity,
10+
maxDepth: number
1011
};
1112

1213
const message : FunctionComponent<MessageProps> = (props) => {
1314

14-
const {message, severity} = props;
15+
const {message, severity, maxDepth} = props;
1516

1617
const classNames = [classes.Message];
1718

@@ -38,6 +39,7 @@ const message : FunctionComponent<MessageProps> = (props) => {
3839
<PpDisplay
3940
pp={message}
4041
coqCss={classes}
42+
maxDepth={maxDepth}
4143
/>
4244
</span>
4345
);

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

+6-5
Original file line numberDiff line numberDiff line change
@@ -5,19 +5,20 @@ import Accordion from '../atoms/Accordion';
55
import { CollapsibleGoal } from '../../types';
66

77
type CollapsibleGoalBlockProps = {
8-
goal: CollapsibleGoal
8+
goal: CollapsibleGoal,
99
collapseHandler: (id: string) => void,
10-
goalIndex: number
11-
goalIndicator: string
10+
goalIndex: number,
11+
goalIndicator: string,
12+
maxDepth: number
1213
};
1314

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

16-
const {goal, goalIndex, goalIndicator, collapseHandler} = props;
17+
const {goal, goalIndex, goalIndicator, collapseHandler, maxDepth} = props;
1718

1819
return (
1920
<Accordion title={"Goal " + goalIndex} collapsed={!goal.isOpen} collapseHandler={() => collapseHandler(goal.id)}>
20-
<GoalBlock goal={goal} goalIndicator={goalIndicator} />
21+
<GoalBlock goal={goal} goalIndicator={goalIndicator} maxDepth={maxDepth}/>
2122
</Accordion>
2223
);
2324

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

+5-4
Original file line numberDiff line numberDiff line change
@@ -11,19 +11,20 @@ import { Goal } from '../../types';
1111

1212
type GoalBlockProps = {
1313
goal: Goal
14-
goalIndicator?: string
14+
goalIndicator?: string,
15+
maxDepth: number
1516
};
1617

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

19-
const {goal, goalIndicator} = props;
20+
const {goal, goalIndicator, maxDepth} = props;
2021
const indicator = goalIndicator ? <span className={classes.GoalIndex} >({goalIndicator})</span> : null;
2122

2223
return (
2324
<div className={classes.Block}>
24-
<HypothesesBlock hypotheses={goal.hypotheses}/>
25+
<HypothesesBlock hypotheses={goal.hypotheses} maxDepth={maxDepth}/>
2526
<div className={classes.SeparatorZone}> {indicator} <Separator /> </div>
26-
<GoalComponent goal={goal.goal}/>
27+
<GoalComponent goal={goal.goal} maxDepth={maxDepth}/>
2728
</div>
2829
);
2930
};

‎client/goal-view-ui/src/components/molecules/HypothesesBlock.tsx

+3-2
Original file line numberDiff line numberDiff line change
@@ -7,14 +7,15 @@ import { Hyp } from '../../types';
77

88
type HypothesesBlockProps = {
99
hypotheses: Hyp[];
10+
maxDepth: number
1011
};
1112

1213
const hypothesesBlock: FunctionComponent<HypothesesBlockProps> = (props) => {
1314

14-
const {hypotheses} = props;
15+
const {hypotheses, maxDepth} = props;
1516

1617
const hypothesesComponents = hypotheses.map((hyp, index) => {
17-
return <Hypothesis key={index} content={hyp} />;
18+
return <Hypothesis key={index} content={hyp} maxDepth={maxDepth}/>;
1819
});
1920

2021
return (

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

+5-4
Original file line numberDiff line numberDiff line change
@@ -7,12 +7,13 @@ import classes from './GoalCollapsibles.module.css';
77

88
type GoalSectionProps = {
99
goals: CollapsibleGoal[],
10-
collapseGoalHandler: (id: string) => void,
10+
collapseGoalHandler: (id: string) => void,
11+
maxDepth: number
1112
};
1213

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

15-
const {goals, collapseGoalHandler} = props;
16+
const {goals, collapseGoalHandler, maxDepth} = props;
1617
const firstGoalRef = useRef<HTMLDivElement>(null);
1718

1819
useEffect(() => {
@@ -34,14 +35,14 @@ const goalSection: FunctionComponent<GoalSectionProps> = (props) => {
3435
if(index === 0) {
3536
return (
3637
<>
37-
<CollapsibleGoalBlock goal={goal} goalIndex={index + 1} goalIndicator={index + 1 + " / " + goals.length} collapseHandler={collapseGoalHandler}/>
38+
<CollapsibleGoalBlock goal={goal} goalIndex={index + 1} goalIndicator={index + 1 + " / " + goals.length} collapseHandler={collapseGoalHandler} maxDepth={maxDepth}/>
3839
<div ref={firstGoalRef}/>
3940
</>
4041
);
4142
}
4243

4344
return (
44-
<CollapsibleGoalBlock goal={goal} goalIndex={index + 1} goalIndicator={index + 1 + " / " + goals.length} collapseHandler={collapseGoalHandler}/>
45+
<CollapsibleGoalBlock goal={goal} goalIndex={index + 1} goalIndicator={index + 1 + " / " + goals.length} collapseHandler={collapseGoalHandler} maxDepth={maxDepth}/>
4546
);
4647
});
4748

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

+5-4
Original file line numberDiff line numberDiff line change
@@ -12,12 +12,13 @@ type GoalSectionProps = {
1212
collapseGoalHandler: (id: string) => void,
1313
displaySetting: string;
1414
emptyMessage: string;
15-
emptyIcon?: JSX.Element
15+
emptyIcon?: JSX.Element;
16+
maxDepth: number;
1617
};
1718

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

20-
const {goals, collapseGoalHandler, displaySetting, emptyMessage, emptyIcon} = props;
21+
const {goals, collapseGoalHandler, displaySetting, emptyMessage, emptyIcon, maxDepth} = props;
2122
const emptyMessageRef = useRef<HTMLDivElement>(null);
2223

2324
useEffect(() => {
@@ -41,8 +42,8 @@ const goalSection: FunctionComponent<GoalSectionProps> = (props) => {
4142
<div ref={emptyMessageRef}/>
4243
</>
4344
: displaySetting === 'Tabs' ?
44-
<GoalTabSection goals={goals} />
45-
: <GoalCollapsibleSection goals={goals} collapseGoalHandler={collapseGoalHandler} />;
45+
<GoalTabSection goals={goals} maxDepth={maxDepth} />
46+
: <GoalCollapsibleSection goals={goals} collapseGoalHandler={collapseGoalHandler} maxDepth={maxDepth}/>;
4647

4748
return section;
4849
};

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

+3-2
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,12 @@ import classes from './GoalTabs.module.css';
1212

1313
type GoalSectionProps = {
1414
goals: Goal[];
15+
maxDepth: number
1516
};
1617

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

19-
const {goals} = props;
20+
const {goals, maxDepth} = props;
2021
const goalRefs = useRef<Array<HTMLDivElement | null>>([]);
2122
useLayoutEffect(() => {
2223
goalRefs.current = goalRefs.current.slice(0, goals.length);
@@ -49,7 +50,7 @@ const goalSection: FunctionComponent<GoalSectionProps> = (props) => {
4950
const viewId = "view-" + index;
5051
return (
5152
<VSCodePanelView id={viewId} key={viewId}>
52-
<GoalBlock goal={goal} goalIndicator={index + 1 + " / " + goals.length}/>
53+
<GoalBlock goal={goal} goalIndicator={index + 1 + " / " + goals.length} maxDepth={maxDepth}/>
5354
<div ref={el => goalRefs.current[index] = el}/>
5455
</VSCodePanelView>
5556
);

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

+6-2
Original file line numberDiff line numberDiff line change
@@ -21,11 +21,12 @@ type ProofViewPageProps = {
2121
messages: ProofViewMessage[],
2222
collapseGoalHandler: (id: string, key: ProofViewGoalsKey) => void,
2323
displaySetting: string;
24+
maxDepth: number;
2425
};
2526

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

28-
const {goals, messages, displaySetting, collapseGoalHandler} = props;
29+
const {goals, messages, displaySetting, collapseGoalHandler, maxDepth} = props;
2930

3031
const renderGoals = () => {
3132
const goalBadge = <VSCodeBadge>{goals!.main.length}</VSCodeBadge>;
@@ -53,6 +54,7 @@ const proofViewPage: FunctionComponent<ProofViewPageProps> = (props) => {
5354
emptyIcon={
5455
goals!.shelved.length === 0 && goals!.givenUp.length === 0 ? <VscPass /> : <VscWarning />
5556
}
57+
maxDepth={maxDepth}
5658
/>
5759
</VSCodePanelView>,
5860
<VSCodePanelView className={classes.View}>
@@ -62,6 +64,7 @@ const proofViewPage: FunctionComponent<ProofViewPageProps> = (props) => {
6264
collapseGoalHandler={(id) => collapseGoalHandler(id, ProofViewGoalsKey.shelved)}
6365
displaySetting={displaySetting}
6466
emptyMessage='There are no shelved goals'
67+
maxDepth={maxDepth}
6568
/>
6669
</VSCodePanelView>,
6770
<VSCodePanelView className={classes.View}>
@@ -71,6 +74,7 @@ const proofViewPage: FunctionComponent<ProofViewPageProps> = (props) => {
7174
collapseGoalHandler={(id) => collapseGoalHandler(id, ProofViewGoalsKey.givenUp)}
7275
displaySetting={displaySetting}
7376
emptyMessage='There are no given up goals'
77+
maxDepth={maxDepth}
7478
/>
7579
</VSCodePanelView>
7680
];
@@ -85,7 +89,7 @@ const proofViewPage: FunctionComponent<ProofViewPageProps> = (props) => {
8589

8690
const displayMessages = messages.map(m => {
8791
return (
88-
<Message message={m[1]} severity={m[0]}/>
92+
<Message message={m[1]} severity={m[0]} maxDepth={maxDepth}/>
8993
);
9094
});
9195

‎client/goal-view-ui/src/types.ts

+1
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,7 @@ export type BoxDisplay = Break | Term | Box | null;
7171
export interface Box {
7272
id: string,
7373
type: DisplayType.box,
74+
depth: number,
7475
classList: string[],
7576
mode: PpMode,
7677
indent: number,

‎client/goal-view-ui/src/utilities/Pp.module.css

+20-1
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,19 @@
33
width: 100%;
44
}
55

6+
.Ellipsis {
7+
color: var(--vscode-coq-termReference);
8+
font-style: italic;
9+
cursor: pointer;
10+
}
11+
612
.Content {
713
white-space: pre;
814
}
915

1016
.Box {
1117
display: inline;
18+
cursor: pointer;
1219
}
1320

1421
.Box + .Text {
@@ -17,4 +24,16 @@
1724

1825
.Box + .Tag {
1926
vertical-align: bottom;
20-
}
27+
}
28+
29+
.Hovered:not(:has(.Hovered:hover)):hover {
30+
border-width: 1px;
31+
border-style: dashed;
32+
border-color: white;
33+
}
34+
35+
/* .Box:not(:has(.Box:hover)):hover {
36+
border-width: 1px;
37+
border-style: dashed;
38+
border-color: white;
39+
} */

0 commit comments

Comments
 (0)