use cytoscape

2 years ago · 50339da74f
parent 5cb0ff4ccf
commit 50339da74f
5 changed files with 148 additions and 12 deletions
--- 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|infoResultType>(null)
+  const worldsRef = useRef<HTMLDivElement>(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 = <Box display="flex" alignItems="center" justifyContent="center" sx={{ height: "calc(100vh - 64px)" }}><CircularProgress /></Box>
  }
-  return <Grid container direction="row" justifyContent="center" alignItems="center">
-    <Grid item xs={12} sm={6}>{content}</Grid>
-  </Grid>
+  return <div>
+    <div>{content}</div>
+    <div ref={worldsRef} style={{"width": "100%","height": "50em"}} />
+  </div>
 }

 export default Welcome
--- 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",
--- 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",
--- 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
+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
--- a/tsconfig.json
+++ b/tsconfig.json
@ -9,6 +9,7 @@
    "moduleResolution": "node",
    "jsx": "react",
    "downlevelIteration": true,
-    "experimentalDecorators": true
+    "experimentalDecorators": true,
+    "allowSyntheticDefaultImports": true,
  }
 }