side-by-side goals #90

pull/251/merge
Jon Eugster 9 months ago
parent aedf073a33
commit 2a070332f2

@ -153,8 +153,8 @@ export const Goal = React.memo((props: GoalProps) => {
{ ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} : { ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} :
undefined, undefined,
[locs, goal.mvarId]) [locs, goal.mvarId])
const goalLi = <div key={'goal'}> const goalLi = <div key={'goal'} className="goal">
<div className="goal-title">{t("Goal")}:</div> {/* <div className="goal-title">{t("Goal")}:</div> */}
<LocationsContext.Provider value={goalLocs}> <LocationsContext.Provider value={goalLocs}>
<InteractiveCode fmt={goal.type} /> <InteractiveCode fmt={goal.type} />
</LocationsContext.Provider> </LocationsContext.Provider>
@ -168,18 +168,28 @@ export const Goal = React.memo((props: GoalProps) => {
const objectHyps = hyps.filter(hyp => !hyp.isAssumption) const objectHyps = hyps.filter(hyp => !hyp.isAssumption)
const assumptionHyps = hyps.filter(hyp => hyp.isAssumption) const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
return <div> return <>
{/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */} {/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */}
{filter.reverse && goalLi} {filter.reverse && goalLi}
<div className="hypotheses">
{! typewriter && objectHyps.length > 0 && {! typewriter && objectHyps.length > 0 &&
<div className="hyp-group"><div className="hyp-group-title">{t("Objects")}:</div> <div className="hyp-group"><div className="hyp-group-title">{t("Objects")}:</div>
{objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> } {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
{!typewriter && assumptionHyps.length > 0 && {!typewriter && assumptionHyps.length > 0 &&
<div className="hyp-group"><div className="hyp-group-title">{t("Assumptions")}:</div> <div className="hyp-group"><div className="hyp-group-title">{t("Assumptions")}:</div>
{assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> } {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
{!filter.reverse && goalLi} </div>
{!filter.reverse && <>
<div className='goal-sign'>
<svg width="100%" height="100%">
<line x1="0%" y1="0%" x2="0%" y2="100%" />
<line x1="0%" y1="50%" x2="100%" y2="50%" />
</svg>
</div>
{goalLi}
</>}
{/* {showHints && hints} */} {/* {showHints && hints} */}
</div> </>
}) })
export const MainAssumptions = React.memo((props: GoalProps2) => { export const MainAssumptions = React.memo((props: GoalProps2) => {

@ -189,3 +189,32 @@
.tooltip-arrow { .tooltip-arrow {
display: none; display: none;
} }
.goal-tab {
/* border: 2px dotted darkgreen; */
display: flex;
flex-direction: row;
}
.goal-tab .goal, .goal-tab .hypotheses {
/* border: 1px solid lightblue; */
display: inline-block;
flex: 1;
display: flex;
flex-direction: column;
justify-content: center;
}
.goal-sign {
/* border: 1px solid lightblue; */
width: 1rem;
margin-left: .5rem;
margin-right: .5rem;
display: inline-block;
}
.goal-sign line {
stroke: var(--clr-dark-gray);
stroke-width: 2;
}

Loading…
Cancel
Save