prettier goal view
This commit is contained in:
+4
-2
@@ -3,19 +3,21 @@
|
||||
:root {
|
||||
--clr-primary: #1976d2;
|
||||
--clr-code: rgba(0, 32, 90, 0.87);
|
||||
--ff-primary: Roboto;
|
||||
--ff-code: Roboto Mono;
|
||||
}
|
||||
|
||||
|
||||
/* General styling */
|
||||
|
||||
body {
|
||||
font-family: Roboto;
|
||||
font-family: var(--ff-primary);
|
||||
-webkit-font-smoothing: antialiased;
|
||||
-moz-osx-font-smoothing: grayscale;
|
||||
}
|
||||
|
||||
code {
|
||||
font-family: Roboto Mono;
|
||||
font-family: var(--ff-code);
|
||||
color: var(--clr-code);
|
||||
}
|
||||
|
||||
|
||||
@@ -123,7 +123,6 @@ interface GoalProps {
|
||||
export const Goal = React.memo((props: GoalProps) => {
|
||||
const { goal, filter } = props
|
||||
|
||||
const prefix = goal.goalPrefix ?? 'Prove: '
|
||||
const filteredList = getFilteredHypotheses(goal.hyps, filter);
|
||||
const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList;
|
||||
const locs = React.useContext(LocationsContext)
|
||||
@@ -133,7 +132,7 @@ export const Goal = React.memo((props: GoalProps) => {
|
||||
undefined,
|
||||
[locs, goal.mvarId])
|
||||
const goalLi = <div key={'goal'}>
|
||||
<strong className="goal-vdash">Prove: </strong>
|
||||
<div className="goal-title">Goal: </div>
|
||||
<LocationsContext.Provider value={goalLocs}>
|
||||
<InteractiveCode fmt={goal.type} />
|
||||
</LocationsContext.Provider>
|
||||
@@ -150,10 +149,12 @@ export const Goal = React.memo((props: GoalProps) => {
|
||||
return <div className={cn}>
|
||||
{goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>}
|
||||
{filter.reverse && goalLi}
|
||||
<div>Objects:</div>
|
||||
{objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
|
||||
<div>Assumptions:</div>
|
||||
{assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
|
||||
{ objectHyps.length > 0 &&
|
||||
<div className="hyp-group"><div className="hyp-group-title">Objects:</div>
|
||||
{objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
|
||||
{ assumptionHyps.length > 0 &&
|
||||
<div className="hyp-group"><div className="hyp-group-title">Assumptions:</div>
|
||||
{assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
|
||||
{!filter.reverse && goalLi}
|
||||
{hints}
|
||||
</div>
|
||||
|
||||
@@ -16,3 +16,12 @@
|
||||
color: #D8000C;
|
||||
background-color: #FFBABA;
|
||||
}
|
||||
|
||||
.hyp-group {
|
||||
margin-bottom: 0.3em;
|
||||
}
|
||||
|
||||
.hyp-group-title, .goal-title {
|
||||
font-family: var(--ff-primary);
|
||||
font-size: 1.2rem;
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user