phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

insert proper keys in lists

Browse Source
This commit is contained in:
Alexander Bentkamp
2022-12-23 09:14:58 +01:00
parent 49159c9761
commit 9f19352047
2 changed files with 15 additions and 16 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/TacticState.tsx
+10 -10
View File
@@ -33,15 +33,15 @@ function Goal({ goal }) {
<Box sx={{ pl: 2 }}>
{hasObject && <Box><Typography>Objects</Typography>
<List>
{goal.objects.map((item) =>
<ListItem key={item.userName}>
{goal.objects.map((item, index) =>
<ListItem key={index}>
<Typography color="primary" sx={{ mr: 1 }}>{item.userName}</Typography> :
<Typography color="secondary" sx={{ ml: 1 }}>{item.type}</Typography>
</ListItem>)}
</List></Box>}
{hasAssumption && <Box><Typography>Assumptions</Typography>
<List>
{goal.assumptions.map((item) => <ListItem key={item}><Typography color="primary" sx={{ mr: 1 }}>{item.userName}</Typography> :
{goal.assumptions.map((item, index) => <ListItem key={index}><Typography color="primary" sx={{ mr: 1 }}>{item.userName}</Typography> :
<Typography color="secondary" sx={{ ml: 1 }}>{item.type}</Typography></ListItem>)}
</List></Box>}
<Typography>Prove:</Typography>
@@ -52,7 +52,7 @@ function Goal({ goal }) {
control={<Switch checked={showHints} onChange={handleHintsChange} />}
label="More Help?"
/>}
{hints.map((hint) => <Collapse in={showHints}><Alert severity="info" sx={{ mt: 1 }}><Markdown>{hint.message}</Markdown></Alert></Collapse>)}
{hints.map((hint, index) => <Collapse key={index} in={showHints}><Alert severity="info" sx={{ mt: 1 }}><Markdown>{hint.message}</Markdown></Alert></Collapse>)}
</Box>)
}
@@ -72,8 +72,8 @@ function OtherGoal({ goal }) {
<Box>
<Typography>Objects</Typography>
<List>
{goal.objects.map((item) =>
<ListItem key={item.userName}>
{goal.objects.map((item, index) =>
<ListItem key={index}>
<Typography color="primary" sx={{ mr: 1 }}>{item.userName}</Typography> :
<Typography color="secondary" sx={{ ml: 1 }}>{item.type}</Typography>
</ListItem>)}
@@ -83,8 +83,8 @@ function OtherGoal({ goal }) {
<Box>
<Typography>Assumptions</Typography>
<List>
{goal.assumptions.map((item) =>
<ListItem key={item}>
{goal.assumptions.map((item, index) =>
<ListItem key={index}>
<Typography color="primary" sx={{ mr: 1 }}>{item.userName}</Typography> :
<Typography color="secondary" sx={{ ml: 1 }}>{item.type}</Typography>
</ListItem>)}
@@ -126,8 +126,8 @@ function TacticState({ goals, diagnostics, completed, globalDiagnostics }) {
{hasError &&
<Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}>
<Typography variant="h5" sx={{ mb: 2 }}>Lean says</Typography>
{diagnostics.map(({severity, message}) =>
<Alert severity={{1: "error", 2:"warning", 3:"info", 4:"success"}[severity]} sx={{ mt: 1 }}>{message}</Alert>
{diagnostics.map(({severity, message}, index) =>
<Alert key={index} severity={{1: "error", 2:"warning", 3:"info", 4:"success"}[severity]} sx={{ mt: 1 }}>{message}</Alert>
// TODO: When does Lean give severity=4? Had colour `gray` before. Make custom theme for that
)}
</Paper>}
client/src/components/Welcome.tsx
+5 -6
View File
@@ -33,16 +33,17 @@ function Welcome() {
const svgElements = []
if (gameInfo.data) {
for (let edge of gameInfo.data.worlds.edges) {
for (let i in gameInfo.data.worlds.edges) {
const edge = gameInfo.data.worlds.edges[i]
svgElements.push(
<line x1={nodes[edge[0]].x} y1={nodes[edge[0]].y} x2={nodes[edge[1]].x} y2={nodes[edge[1]].y} stroke="#1976d2" strokeWidth="1"/>
<line key={`pathway${i}`} x1={nodes[edge[0]].x} y1={nodes[edge[0]].y} x2={nodes[edge[1]].x} y2={nodes[edge[1]].y} stroke="#1976d2" strokeWidth="1"/>
)
}
for (let id in nodes) {
let position: cytoscape.Position = nodes[id]
svgElements.push(
<Link to={`/world/${id}/level/1`}>
<Link key={`world${id}`} to={`/world/${id}/level/1`}>
<circle fill="#61DAFB" cx={position.x} cy={position.y} r="8" />
<text style={{font: "italic 2px sans-serif", textAnchor: "middle", dominantBaseline: "middle"} as any} x={position.x} y={position.y}>{id}</text>
</Link>
@@ -50,7 +51,7 @@ function Welcome() {
for (let i = 1; i <= gameInfo.data.worldSize[id]; i++) {
svgElements.push(
<Link to={`/world/${id}/level/${i}`}>
<Link to={`/world/${id}/level/${i}`} key={`/world/${id}/level/${i}`}>
<circle fill="#aaa" cx={position.x + Math.sin(i/5) * 9} cy={position.y - Math.cos(i/5) * 9} r="0.8" />
</Link>
)
@@ -109,9 +110,7 @@ function computeWorldLayout(worlds) {
let nodes = {}
cy.nodes().forEach((node, id) => {
nodes[node.id()] = node.position()
console.log(node.position())
})
const bounds = cy.nodes().boundingBox()
console.log(bounds)
return { nodes, bounds }
}