diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx index 6af0f62..633fd7f 100644 --- a/client/src/components/Welcome.tsx +++ b/client/src/components/Welcome.tsx @@ -1,5 +1,5 @@ import * as React from 'react'; -import { useState, useEffect } from 'react'; +import { useState, useEffect, useRef } from 'react'; import ReactMarkdown from 'react-markdown'; import { MathJax } from "better-react-mathjax"; import '@fontsource/roboto/300.css'; @@ -7,6 +7,10 @@ import '@fontsource/roboto/400.css'; import '@fontsource/roboto/500.css'; import '@fontsource/roboto/700.css'; import * as rpc from 'vscode-ws-jsonrpc'; +import cytoscape from 'cytoscape' +import klay from 'cytoscape-klay'; + +cytoscape.use( klay ); import { Box, Typography, Button, CircularProgress, Grid } from '@mui/material'; import { LeanClient } from 'lean4web/client/src/editor/leanclient'; @@ -23,11 +27,56 @@ type infoResultType = { title: string, nb_levels: any[], conclusion: string + worlds: {edges: string[][], nodes: string[]} } function Welcome({ leanClient, setNbLevels, setTitle, startGame, setConclusion }: WelcomeProps) { const [leanData, setLeanData] = useState(null) + const worldsRef = useRef(null) + + const drawWorlds = (worlds) => { + let elements = [] + for (let node of worlds.nodes) { + elements.push({ data: { id: node } }) + } + for (let edge of worlds.edges) { + elements.push({ + data: { + id: edge[0] + " --edge-to--> " + edge[1], + source: edge[0], + target: edge[1] + } + }) + } + const layout : any = {name: "klay", klay: {direction: "DOWN"}} + cytoscape({ container: worldsRef.current!, elements, layout, + style: [ // the stylesheet for the graph + { + selector: 'node', + style: { + 'background-color': '#666', + 'label': 'data(id)' + } + }, + + { + selector: 'edge', + style: { + 'width': 3, + 'line-color': '#ccc', + 'target-arrow-color': '#ccc', + 'target-arrow-shape': 'triangle', + 'curve-style': 'bezier' + } + } + ], + userPanningEnabled: false, + userZoomingEnabled: false, + autoungrabify: true, + autounselectify: true, + }) + } useEffect(() => { if (!leanClient) return; @@ -41,6 +90,7 @@ function Welcome({ leanClient, setNbLevels, setTitle, startGame, setConclusion } setTitle(res.title) document.title = res.title setConclusion(res.conclusion) + drawWorlds(res.worlds) }); } getInfo() @@ -61,9 +111,10 @@ function Welcome({ leanClient, setNbLevels, setTitle, startGame, setConclusion } } else { content = } - return - {content} - + return
+
{content}
+
+
} export default Welcome diff --git a/package-lock.json b/package-lock.json index 51723c2..6a1c1dc 100644 --- a/package-lock.json +++ b/package-lock.json @@ -12,7 +12,10 @@ "@fontsource/roboto-mono": "^4.5.8", "@mui/icons-material": "^5.10.6", "@mui/material": "^5.10.9", + "@types/cytoscape": "^3.19.9", "better-react-mathjax": "^2.0.2", + "cytoscape": "^3.23.0", + "cytoscape-klay": "^3.1.4", "express": "^4.18.2", "lean4web": "github:hhu-adam/lean4web", "path-browserify": "^1.0.1", @@ -2157,6 +2160,11 @@ "@types/node": "*" } }, + "node_modules/@types/cytoscape": { + "version": "3.19.9", + "resolved": "https://registry.npmjs.org/@types/cytoscape/-/cytoscape-3.19.9.tgz", + "integrity": "sha512-oqCx0ZGiBO0UESbjgq052vjDAy2X53lZpMrWqiweMpvVwKw/2IiYDdzPFK6+f4tMfdv9YKEM9raO5bAZc3UYBg==" + }, "node_modules/@types/debug": { "version": "4.1.7", "resolved": "https://registry.npmjs.org/@types/debug/-/debug-4.1.7.tgz", @@ -3649,6 +3657,29 @@ "resolved": "https://registry.npmjs.org/csstype/-/csstype-3.1.1.tgz", "integrity": "sha512-DJR/VvkAvSZW9bTouZue2sSxDwdTN92uHjqeKVm+0dAqdfNykRzQ95tay8aXMBAAPpUiq4Qcug2L7neoRh2Egw==" }, + "node_modules/cytoscape": { + "version": "3.23.0", + "resolved": "https://registry.npmjs.org/cytoscape/-/cytoscape-3.23.0.tgz", + "integrity": "sha512-gRZqJj/1kiAVPkrVFvz/GccxsXhF3Qwpptl32gKKypO4IlqnKBjTOu+HbXtEggSGzC5KCaHp3/F7GgENrtsFkA==", + "dependencies": { + "heap": "^0.2.6", + "lodash": "^4.17.21" + }, + "engines": { + "node": ">=0.10" + } + }, + "node_modules/cytoscape-klay": { + "version": "3.1.4", + "resolved": "https://registry.npmjs.org/cytoscape-klay/-/cytoscape-klay-3.1.4.tgz", + "integrity": "sha512-VwPj0VR25GPfy6qXVQRi/MYlZM/zkdvRhHlgqbM//lSvstgM6fhp3ik/uM8Wr8nlhskfqz/M1fIDmR6UckbS2A==", + "dependencies": { + "klayjs": "^0.4.1" + }, + "peerDependencies": { + "cytoscape": "^3.2.0" + } + }, "node_modules/date-fns": { "version": "2.29.3", "resolved": "https://registry.npmjs.org/date-fns/-/date-fns-2.29.3.tgz", @@ -4461,6 +4492,11 @@ "url": "https://opencollective.com/unified" } }, + "node_modules/heap": { + "version": "0.2.7", + "resolved": "https://registry.npmjs.org/heap/-/heap-0.2.7.tgz", + "integrity": "sha512-2bsegYkkHO+h/9MGbn6KWcE45cHZgPANo5LXF7EvWdT0yT2EguSVO1nDgU5c8+ZOPwp2vMNa7YFsJhVcDR9Sdg==" + }, "node_modules/hoist-non-react-statics": { "version": "3.3.2", "resolved": "https://registry.npmjs.org/hoist-non-react-statics/-/hoist-non-react-statics-3.3.2.tgz", @@ -4960,6 +4996,11 @@ "node": ">=0.10.0" } }, + "node_modules/klayjs": { + "version": "0.4.1", + "resolved": "https://registry.npmjs.org/klayjs/-/klayjs-0.4.1.tgz", + "integrity": "sha512-WUNxuO7O79TEkxCj6OIaK5TJBkaWaR/IKNTakgV9PwDn+mrr63MLHed34AcE2yTaDntgO6l0zGFIzhcoTeroTA==" + }, "node_modules/lean4": { "version": "0.0.95", "resolved": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?a51db90", @@ -5080,8 +5121,7 @@ "node_modules/lodash": { "version": "4.17.21", "resolved": "https://registry.npmjs.org/lodash/-/lodash-4.17.21.tgz", - "integrity": "sha512-v2kDEe57lecTulaDIuNTPy3Ry4gLGJ6Z1O3vE1krgXZNrsQ+LFTGHVxVjcXPs17LhbZVGedAJv8XZ1tvj5FvSg==", - "devOptional": true + "integrity": "sha512-v2kDEe57lecTulaDIuNTPy3Ry4gLGJ6Z1O3vE1krgXZNrsQ+LFTGHVxVjcXPs17LhbZVGedAJv8XZ1tvj5FvSg==" }, "node_modules/loose-envify": { "version": "1.4.0", @@ -10096,6 +10136,11 @@ "@types/node": "*" } }, + "@types/cytoscape": { + "version": "3.19.9", + "resolved": "https://registry.npmjs.org/@types/cytoscape/-/cytoscape-3.19.9.tgz", + "integrity": "sha512-oqCx0ZGiBO0UESbjgq052vjDAy2X53lZpMrWqiweMpvVwKw/2IiYDdzPFK6+f4tMfdv9YKEM9raO5bAZc3UYBg==" + }, "@types/debug": { "version": "4.1.7", "resolved": "https://registry.npmjs.org/@types/debug/-/debug-4.1.7.tgz", @@ -11303,6 +11348,23 @@ "resolved": "https://registry.npmjs.org/csstype/-/csstype-3.1.1.tgz", "integrity": "sha512-DJR/VvkAvSZW9bTouZue2sSxDwdTN92uHjqeKVm+0dAqdfNykRzQ95tay8aXMBAAPpUiq4Qcug2L7neoRh2Egw==" }, + "cytoscape": { + "version": "3.23.0", + "resolved": "https://registry.npmjs.org/cytoscape/-/cytoscape-3.23.0.tgz", + "integrity": "sha512-gRZqJj/1kiAVPkrVFvz/GccxsXhF3Qwpptl32gKKypO4IlqnKBjTOu+HbXtEggSGzC5KCaHp3/F7GgENrtsFkA==", + "requires": { + "heap": "^0.2.6", + "lodash": "^4.17.21" + } + }, + "cytoscape-klay": { + "version": "3.1.4", + "resolved": "https://registry.npmjs.org/cytoscape-klay/-/cytoscape-klay-3.1.4.tgz", + "integrity": "sha512-VwPj0VR25GPfy6qXVQRi/MYlZM/zkdvRhHlgqbM//lSvstgM6fhp3ik/uM8Wr8nlhskfqz/M1fIDmR6UckbS2A==", + "requires": { + "klayjs": "^0.4.1" + } + }, "date-fns": { "version": "2.29.3", "resolved": "https://registry.npmjs.org/date-fns/-/date-fns-2.29.3.tgz", @@ -11905,6 +11967,11 @@ "resolved": "https://registry.npmjs.org/hast-util-whitespace/-/hast-util-whitespace-2.0.0.tgz", "integrity": "sha512-Pkw+xBHuV6xFeJprJe2BBEoDV+AvQySaz3pPDRUs5PNZEMQjpXJJueqrpcHIXxnWTcAGi/UOCgVShlkY6kLoqg==" }, + "heap": { + "version": "0.2.7", + "resolved": "https://registry.npmjs.org/heap/-/heap-0.2.7.tgz", + "integrity": "sha512-2bsegYkkHO+h/9MGbn6KWcE45cHZgPANo5LXF7EvWdT0yT2EguSVO1nDgU5c8+ZOPwp2vMNa7YFsJhVcDR9Sdg==" + }, "hoist-non-react-statics": { "version": "3.3.2", "resolved": "https://registry.npmjs.org/hoist-non-react-statics/-/hoist-non-react-statics-3.3.2.tgz", @@ -12265,6 +12332,11 @@ "integrity": "sha512-dcS1ul+9tmeD95T+x28/ehLgd9mENa3LsvDTtzm3vyBEO7RPptvAD+t44WVXaUjTBRcrpFeFlC8WCruUR456hw==", "dev": true }, + "klayjs": { + "version": "0.4.1", + "resolved": "https://registry.npmjs.org/klayjs/-/klayjs-0.4.1.tgz", + "integrity": "sha512-WUNxuO7O79TEkxCj6OIaK5TJBkaWaR/IKNTakgV9PwDn+mrr63MLHed34AcE2yTaDntgO6l0zGFIzhcoTeroTA==" + }, "lean4": { "version": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?a51db90", "integrity": "sha512-eKDMAR/1LvozI+Zhw4smMerwhYi2aZR1Yf0v5jbxu3g5z4YMMhYJpYhbtVhf4Za0boSsol2+z2dxc8fBI/1LOg==", @@ -12297,7 +12369,7 @@ }, "lean4web": { "version": "git+ssh://git@github.com/hhu-adam/lean4web.git#465694da60e2afbf7d188b41af173998ae75d915", - "from": "lean4web@git+https://github.com/hhu-adam/lean4web.git", + "from": "lean4web@github:hhu-adam/lean4web", "requires": { "@fontsource/roboto": "^4.5.8", "@fontsource/roboto-mono": "^4.5.8", @@ -12360,8 +12432,7 @@ "lodash": { "version": "4.17.21", "resolved": "https://registry.npmjs.org/lodash/-/lodash-4.17.21.tgz", - "integrity": "sha512-v2kDEe57lecTulaDIuNTPy3Ry4gLGJ6Z1O3vE1krgXZNrsQ+LFTGHVxVjcXPs17LhbZVGedAJv8XZ1tvj5FvSg==", - "devOptional": true + "integrity": "sha512-v2kDEe57lecTulaDIuNTPy3Ry4gLGJ6Z1O3vE1krgXZNrsQ+LFTGHVxVjcXPs17LhbZVGedAJv8XZ1tvj5FvSg==" }, "loose-envify": { "version": "1.4.0", diff --git a/package.json b/package.json index a63fe73..e30428a 100644 --- a/package.json +++ b/package.json @@ -8,7 +8,10 @@ "@fontsource/roboto-mono": "^4.5.8", "@mui/icons-material": "^5.10.6", "@mui/material": "^5.10.9", + "@types/cytoscape": "^3.19.9", "better-react-mathjax": "^2.0.2", + "cytoscape": "^3.23.0", + "cytoscape-klay": "^3.1.4", "express": "^4.18.2", "lean4web": "github:hhu-adam/lean4web", "path-browserify": "^1.0.1", diff --git a/server/testgame/TestGame/Metadata.lean b/server/testgame/TestGame/Metadata.lean index 6ae4946..3882c7f 100644 --- a/server/testgame/TestGame/Metadata.lean +++ b/server/testgame/TestGame/Metadata.lean @@ -20,5 +20,15 @@ with a level 1 spell book. Good luck." Conclusion "There is nothing else so far. Thanks for rescuing natural numbers!" -Path w1 → w2 → w3 -Path w1 → v2 → w3 \ No newline at end of file +World "w1" +World "w2" +World "w3" +World "v1" +World "v2" +World "v3" +World "v4" + + +Path TestWorld → w1 → w2 → w3 +Path w1 → v1 → v2 → v3 → w3 +Path v3 → v4 \ No newline at end of file diff --git a/tsconfig.json b/tsconfig.json index 8952160..c09f51d 100644 --- a/tsconfig.json +++ b/tsconfig.json @@ -9,6 +9,7 @@ "moduleResolution": "node", "jsx": "react", "downlevelIteration": true, - "experimentalDecorators": true + "experimentalDecorators": true, + "allowSyntheticDefaultImports": true, } }