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

use ReactMarkdown plugins

Browse Source
This commit is contained in:
Alexander Bentkamp
2022-12-15 13:40:45 +01:00
parent ada40dcf34
commit bbfb6f8f5e
9 changed files with 554 additions and 176 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/App.tsx
-15
View File
@@ -1,6 +1,5 @@
import * as React from 'react';
import { useState, useEffect } from 'react';
import { MathJaxContext } from "better-react-mathjax";
import { Outlet } from "react-router-dom";
import '@fontsource/roboto/300.css';
@@ -19,18 +18,6 @@ function App() {
const [curLevel, setCurLevel] = useState(0)
const [finished, setFinished] = useState(false)
const mathJaxConfig = {
loader: {
load: ['input/tex-base', 'output/svg']
},
tex: {
inlineMath: [['$', '$'], ['\\(', '\\)']]
},
svg: {
fontCache: 'global'
}
}
function startGame() {
setCurLevel(1)
}
@@ -39,7 +26,6 @@ function App() {
return (
<div className="App">
<MathJaxContext config={mathJaxConfig}>
<CssBaseline />
<AppBar className="AppBar" position="sticky" sx={{ zIndex: (theme) => theme.zIndex.drawer + 1 }}>
<Toolbar sx={{ justifyContent: "space-between" }}>
@@ -52,7 +38,6 @@ function App() {
</Toolbar>
</AppBar>
<Outlet />
</MathJaxContext>
</div>
)
}
client/src/components/LeftPanel.tsx
+3 -7
View File
@@ -1,7 +1,6 @@
import * as React from 'react';
import { useState, useEffect } from 'react';
import ReactMarkdown from 'react-markdown';
import { MathJax } from "better-react-mathjax";
import '@fontsource/roboto/300.css';
import '@fontsource/roboto/400.css';
import '@fontsource/roboto/500.css';
@@ -12,6 +11,7 @@ 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'
import Markdown from './Markdown';
function TacticDoc(props) {
return (
@@ -20,9 +20,7 @@ function TacticDoc(props) {
<Typography>{props.tactic.name}</Typography>
</AccordionSummary>
<AccordionDetails>
<MathJax>
<ReactMarkdown>{props.tactic.content}</ReactMarkdown>
</MathJax>
<Markdown>{props.tactic.content}</Markdown>
</AccordionDetails>
</Accordion>)
}
@@ -34,9 +32,7 @@ function LemmaDoc({ lemma }) {
<Typography>{lemma.userName}</Typography>
</AccordionSummary>
<AccordionDetails>
<MathJax>
<ReactMarkdown>{lemma.content}</ReactMarkdown>
</MathJax>
<Markdown>{lemma.content}</Markdown>
</AccordionDetails>
</Accordion>)
}
client/src/components/Level.tsx
+3 -4
View File
@@ -4,8 +4,6 @@ import '@fontsource/roboto/300.css';
import '@fontsource/roboto/400.css';
import '@fontsource/roboto/500.css';
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, IconButton } from '@mui/material';
import MuiDrawer from '@mui/material/Drawer';
@@ -33,6 +31,7 @@ import { faUpload, faArrowRotateRight, faChevronLeft, faChevronRight, faBook, fa
import { styled, useTheme, Theme, CSSObject } from '@mui/material/styles';
import { AppBarProps as MuiAppBarProps } from '@mui/material/AppBar';
import Divider from '@mui/material/Divider';
import Markdown from './Markdown';
@@ -149,11 +148,11 @@ function Level() {
<Grid container columnSpacing={{ xs: 1, sm: 2, md: 3 }} sx={{ flexGrow: 1, p: 3 }} className="main-grid">
<Grid xs={8} className="main-panel">
<div ref={messagePanelRef} className="message-panel">
<MathJax><ReactMarkdown>{level?.data?.introduction}</ReactMarkdown></MathJax>
<Markdown>{level?.data?.introduction}</Markdown>
</div>
<div className="exercise">
<h4>Aufgabe:</h4>
<MathJax><ReactMarkdown>{level?.data?.descrText}</ReactMarkdown></MathJax>
<Markdown>{level?.data?.descrText}</Markdown>
<div className="statement"><code>{level?.data?.descrFormat}</code></div>
<div ref={codeviewRef} className="codeview"></div>
</div>
client/src/components/Markdown.tsx
+18
View File
@@ -0,0 +1,18 @@
import * as React from 'react';
import ReactMarkdown from 'react-markdown';
import remarkMath from 'remark-math'
import rehypeKatex from 'rehype-katex'
import 'katex/dist/katex.min.css' // `rehype-katex` does not import the CSS for you
function Markdown(props) {
const newProps = {
...props,
remarkPlugins: [...props.remarkPlugins ?? [], remarkMath],
rehypePlugins: [...props.remarkPlugins ?? [], rehypeKatex],
};
return (
<ReactMarkdown {...newProps} />
);
}
export default Markdown
client/src/components/Message.tsx
+3 -4
View File
@@ -1,12 +1,11 @@
import * as React from 'react';
import ReactMarkdown from 'react-markdown';
import { MathJax } from "better-react-mathjax";
import '@fontsource/roboto/300.css';
import '@fontsource/roboto/400.css';
import '@fontsource/roboto/500.css';
import '@fontsource/roboto/700.css';
import { Button, Dialog, DialogContent, DialogContentText, DialogActions } from '@mui/material';
import Markdown from './Markdown';
function Message({ isOpen, content, close }) {
@@ -14,7 +13,7 @@ function Message({ isOpen, content, close }) {
<Dialog open={isOpen} onClose={close}>
<DialogContent>
<DialogContentText id="alert-dialog-description">
<MathJax><ReactMarkdown>{content}</ReactMarkdown></MathJax>
<Markdown>{content}</Markdown>
</DialogContentText>
</DialogContent>
<DialogActions>
@@ -26,4 +25,4 @@ function Message({ isOpen, content, close }) {
)
}
export default Message
export default Message
client/src/components/TacticState.tsx
+3 -4
View File
@@ -3,8 +3,6 @@ import '@fontsource/roboto/300.css';
import '@fontsource/roboto/400.css';
import '@fontsource/roboto/500.css';
import '@fontsource/roboto/700.css';
import ReactMarkdown from 'react-markdown';
import { MathJax } from "better-react-mathjax";
import List from '@mui/material/List';
import ListItem from '@mui/material/ListItem';
@@ -14,6 +12,7 @@ import ExpandMoreIcon from '@mui/icons-material/ExpandMore';
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
import { faArrowPointer } from '@fortawesome/free-solid-svg-icons'
import Markdown from './Markdown';
// TODO: Dead variables (x✝) are not displayed correctly.
@@ -47,13 +46,13 @@ function Goal({ goal }) {
</List></Box>}
<Typography>Prove:</Typography>
<Typography color="primary" sx={{ ml: 2 }}>{goal.goal}</Typography>
{openMessages.map((message) => <Alert severity="info" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{message.message}</ReactMarkdown></MathJax></Alert>)}
{openMessages.map((message) => <Alert severity="info" sx={{ mt: 1 }}><Markdown>{message.message}</Markdown></Alert>)}
{hasHints &&
<FormControlLabel
control={<Switch checked={showHints} onChange={handleHintsChange} />}
label="More Help?"
/>}
{hints.map((hint) => <Collapse in={showHints}><Alert severity="info" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{hint.message}</ReactMarkdown></MathJax></Alert></Collapse>)}
{hints.map((hint) => <Collapse in={showHints}><Alert severity="info" sx={{ mt: 1 }}><Markdown>{hint.message}</Markdown></Alert></Collapse>)}
</Box>)
}
client/src/components/Welcome.tsx
+2 -5
View File
@@ -1,7 +1,5 @@
import * as React from 'react';
import { useState, useEffect, useRef } from 'react';
import ReactMarkdown from 'react-markdown';
import { MathJax } from "better-react-mathjax";
import '@fontsource/roboto/300.css';
import '@fontsource/roboto/400.css';
import '@fontsource/roboto/500.css';
@@ -16,6 +14,7 @@ cytoscape.use( klay );
import { Box, Typography, Button, CircularProgress, Grid } from '@mui/material';
import { useGetGameInfoQuery } from '../state/api';
import { Link } from 'react-router-dom';
import Markdown from './Markdown';
function Welcome() {
@@ -38,9 +37,7 @@ function Welcome() {
<div>
<Box sx={{ m: 3 }}>
<Typography variant="body1" component="div">
<MathJax>
<ReactMarkdown>{gameInfo.data.introduction}</ReactMarkdown>
</MathJax>
<Markdown>{gameInfo.data.introduction}</Markdown>
</Typography>
</Box>
<Box textAlign='center' sx={{ m: 5 }}>