From 802d748bf441c1ce9ac2e9966970bf28f8886732 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 14 Dec 2022 14:39:37 +0100 Subject: [PATCH] collapsable side panel --- client/src/components/LeftPanel.tsx | 48 ++++-- client/src/components/Level.tsx | 151 ++++++++++++++---- client/src/components/level.css | 17 +- server/testgame/TestGame/LemmaDocs.lean | 19 ++- .../TestGame/Levels/Logic/L01_Rfl.lean | 2 - .../TestGame/Levels/Logic/L02_Rfl.lean | 1 + 6 files changed, 183 insertions(+), 55 deletions(-) diff --git a/client/src/components/LeftPanel.tsx b/client/src/components/LeftPanel.tsx index 9457b38..85662f5 100644 --- a/client/src/components/LeftPanel.tsx +++ b/client/src/components/LeftPanel.tsx @@ -7,9 +7,11 @@ import '@fontsource/roboto/400.css'; import '@fontsource/roboto/500.css'; import '@fontsource/roboto/700.css'; -import { Paper, Box, Typography, Accordion, AccordionSummary, AccordionDetails, Tabs, Tab } from '@mui/material'; +import { Paper, Box, Typography, Accordion, AccordionSummary, AccordionDetails, Tabs, Tab, Divider, Button, List, ListItem, ListItemButton, ListItemIcon, ListItemText } from '@mui/material'; import ExpandMoreIcon from '@mui/icons-material/ExpandMore'; +import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' +import { faUpload, faArrowRotateRight, faChevronLeft, faChevronRight, faBook, faHammer } from '@fortawesome/free-solid-svg-icons' function TacticDoc(props) { return ( @@ -54,8 +56,7 @@ function LemmaDocs({ lemmas }) { }, [lemmas]); return ( - - Inventory +
{curCategory && categories.get(curCategory).map((lemma) => )} - - ) +
) } -function LeftPanel({ spells, inventory }) { +function LeftPanel({ spells, inventory, showSidePanel, setShowSidePanel }) { + return ( - - {spells && spells.length > 0 && - - Spell book - {spells.map((spell) => )} - } - {inventory && inventory.length > 0 && } - ) + + + setShowSidePanel(true)}> + + + + + + {spells && spells.length > 0 && + + {spells.map((spell) => )} + } + + + + + + + + + {inventory && inventory.length > 0 && + + + } + + + ) } export default LeftPanel; diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index fc4723f..a14622c 100644 --- a/client/src/components/Level.tsx +++ b/client/src/components/Level.tsx @@ -7,7 +7,8 @@ import '@fontsource/roboto/700.css'; import ReactMarkdown from 'react-markdown'; import { MathJax } from "better-react-mathjax"; import { Link as RouterLink } from 'react-router-dom'; -import { Box, Button, CircularProgress, FormControlLabel, FormGroup, Switch } from '@mui/material'; +import { Box, Button, CircularProgress, FormControlLabel, FormGroup, Switch, IconButton } from '@mui/material'; +import MuiDrawer from '@mui/material/Drawer'; import Grid from '@mui/material/Unstable_Grid2'; import LeftPanel from './LeftPanel'; import { LeanTaskGutter } from 'lean4web/client/src/editor/taskgutter'; @@ -22,6 +23,82 @@ import { ConnectionContext } from '../connection'; import Infoview from './Infoview'; import { useParams } from 'react-router-dom'; import { useLoadLevelQuery } from '../game/api'; +import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' +import { faUpload, faArrowRotateRight, faChevronLeft, faChevronRight, faBook, faDownload } from '@fortawesome/free-solid-svg-icons' + +import { styled, useTheme, Theme, CSSObject } from '@mui/material/styles'; +import MuiAppBar, { AppBarProps as MuiAppBarProps } from '@mui/material/AppBar'; +import Toolbar from '@mui/material/Toolbar'; +import List from '@mui/material/List'; +import CssBaseline from '@mui/material/CssBaseline'; +import Typography from '@mui/material/Typography'; +import Divider from '@mui/material/Divider'; +import MenuIcon from '@mui/icons-material/Menu'; +import ChevronLeftIcon from '@mui/icons-material/ChevronLeft'; +import ChevronRightIcon from '@mui/icons-material/ChevronRight'; +import ListItem from '@mui/material/ListItem'; +import ListItemButton from '@mui/material/ListItemButton'; +import ListItemIcon from '@mui/material/ListItemIcon'; +import ListItemText from '@mui/material/ListItemText'; +import InboxIcon from '@mui/icons-material/MoveToInbox'; +import MailIcon from '@mui/icons-material/Mail'; + + +/** Drawer Test */ +const drawerWidth = 400; + +const openedMixin = (theme: Theme): CSSObject => ({ + width: drawerWidth, + transition: theme.transitions.create('width', { + easing: theme.transitions.easing.sharp, + duration: theme.transitions.duration.enteringScreen, + }), + overflowX: 'hidden', +}); + +const closedMixin = (theme: Theme): CSSObject => ({ + transition: theme.transitions.create('width', { + easing: theme.transitions.easing.sharp, + duration: theme.transitions.duration.leavingScreen, + }), + overflowX: 'hidden', + width: `calc(${theme.spacing(7)} + 1px)`, + [theme.breakpoints.up('sm')]: { + width: `calc(${theme.spacing(8)} + 1px)`, + }, +}); + +const DrawerHeader = styled('div')(({ theme }) => ({ + display: 'flex', + alignItems: 'center', + justifyContent: 'flex-end', + padding: theme.spacing(0, 1), + // necessary for content to be below app bar + ...theme.mixins.toolbar, +})); + +interface AppBarProps extends MuiAppBarProps { + open?: boolean; +} + +const Drawer = styled(MuiDrawer, { shouldForwardProp: (prop) => prop !== 'open' })( + ({ theme, open }) => ({ + width: drawerWidth, + flexShrink: 0, + whiteSpace: 'nowrap', + boxSizing: 'border-box', + ...(open && { + ...openedMixin(theme), + '& .MuiDrawer-paper': openedMixin(theme), + }), + ...(!open && { + ...closedMixin(theme), + '& .MuiDrawer-paper': closedMixin(theme), + }), + }), +); + +/** End Drawer Test */ @@ -37,6 +114,14 @@ function Level() { const infoviewRef = useRef(null) const messagePanelRef = useRef(null) + const [showSidePanel, setShowSidePanel] = useState(true) + + const toggleSidePanel = () => { + setShowSidePanel(!showSidePanel) + } + + const theme = useTheme(); + useEffect(() => { // Scroll to top when loading a new level messagePanelRef.current!.scrollTo(0,0) @@ -49,35 +134,43 @@ function Level() { return <> - - - - - -
- {level?.data?.introduction} -
-
-

Aufgabe:

- {level?.data?.descrText} -
{level?.data?.descrFormat}
-
-
- - - - - - -
-
- -
- - { setExpertInfoview(!expertInfoview) }} control={} label="Expert mode" /> - + + + + + + + + + + + + +
+ {level?.data?.introduction} +
+
+

Aufgabe:

+ {level?.data?.descrText} +
{level?.data?.descrFormat}
+
+
+ + + + + + +
+
+ +
+ + { setExpertInfoview(!expertInfoview) }} control={} label="Expert mode" /> + + - + } diff --git a/client/src/components/level.css b/client/src/components/level.css index 845d27d..37d5a1b 100644 --- a/client/src/components/level.css +++ b/client/src/components/level.css @@ -4,7 +4,7 @@ min-height: 0; } -.main-panel, .info-panel, .doc-panel { +.main-panel, .info-panel { height: 100%; overflow: auto; } @@ -35,10 +35,18 @@ margin-bottom: 0; } +.doc-panel li { + border-bottom: 1px solid rgba(0, 0, 0, 0.12); /* This should be teh same colour as `divider` in LeftPanel.tsx */ +} + +.doc-panel li:first-of-type { + border-top: 1px solid rgb(0, 0, 0, 0.12); /* This should be teh same colour as `divider` in LeftPanel.tsx */ +} + /***************************************/ /* TODO: For development purposes only */ /***************************************/ -.doc-panel { +/* .doc-panel { border: 1px solid red; } @@ -61,3 +69,8 @@ .codeview { border: 1px solid rgb(98, 148, 255); } + +.main-grid { + border: 1px solid rgb(255, 0, 0); + margin: 1px; +} */ diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean index 123fed1..4f9d4b0 100644 --- a/server/testgame/TestGame/LemmaDocs.lean +++ b/server/testgame/TestGame/LemmaDocs.lean @@ -1,17 +1,17 @@ import GameServer.Commands -- import TestGame.MyNat --- LemmaDoc zero_add as zero_add in "Addition" --- "This lemma says `∀ a : ℕ, 0 + a = a`." +LemmaDoc zero_add as zero_add in "Addition" +"This lemma says `∀ a : ℕ, 0 + a = a`." --- LemmaDoc add_zero as add_zero in "Addition" --- "This lemma says `∀ a : ℕ, a + 0 = a`." +LemmaDoc add_zero as add_zero in "Addition" +"This lemma says `∀ a : ℕ, a + 0 = a`." --- LemmaDoc add_succ as add_succ in "Addition" --- "This lemma says `∀ a b : ℕ, a + succ b = succ (a + b)`." +LemmaDoc add_succ as add_succ in "Addition" +"This lemma says `∀ a b : ℕ, a + succ b = succ (a + b)`." --- LemmaSet addition : "Addition lemmas" := --- zero_add add_zero +LemmaSet addition : "Addition lemmas" := +zero_add add_zero LemmaDoc not_not as not_not in "Logic" "`∀ (A : Prop), ¬¬A ↔ A`." @@ -44,3 +44,6 @@ LemmaDoc even_square as even_square in "Nat" LemmaSet natural : "Natürliche Zahlen" := even odd not_odd not_even + +LemmaSet logic : "Logik" := +not_not diff --git a/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean b/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean index 4ed4443..91655db 100644 --- a/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean +++ b/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean @@ -31,5 +31,3 @@ Hint : 42 = 42 => "Man schreibt eine Taktik pro Zeile, also gib 'rfl' ein gefolgt von ENTER." Conclusion "Bravo!" - -Tactics rfl diff --git a/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean b/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean index 96b187b..aa67cb4 100644 --- a/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean +++ b/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean @@ -26,3 +26,4 @@ deshalb musst du dieses häufig gar nicht mehr schreiben. " Tactics rfl +Lemmas zero_add