diff --git a/client/src/components/button.tsx b/client/src/components/button.tsx
deleted file mode 100644
index 57fe728..0000000
--- a/client/src/components/button.tsx
+++ /dev/null
@@ -1,15 +0,0 @@
-import * as React from 'react';
-import { Link, LinkProps } from "react-router-dom";
-
-export interface ButtonProps extends LinkProps {
- disabled?: boolean
- inverted?: string // Apparently "inverted" in DOM cannot be `boolean` but must be `inverted`
-}
-
-export function Button(props: ButtonProps) {
- if (props.disabled) {
- return {props.children}
- } else {
- return {props.children}
- }
-}
diff --git a/client/src/components/chat.tsx b/client/src/components/chat.tsx
index e915d79..5e1c4d9 100644
--- a/client/src/components/chat.tsx
+++ b/client/src/components/chat.tsx
@@ -5,10 +5,6 @@ import { useTranslation } from 'react-i18next'
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
import { faArrowRight } from '@fortawesome/free-solid-svg-icons'
-
-import Markdown from './markdown'
-import { Button } from './button'
-
import { changedReadIntro, selectCompleted, selectReadIntro } from '../state/progress'
import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api'
import { useAppDispatch, useAppSelector } from '../hooks'
@@ -18,6 +14,7 @@ import { GameHint, InteractiveGoalsWithHints } from './infoview/rpc_api'
import { lastStepHasErrors } from './infoview/goals'
import '../css/chat.css'
+import { Button, Markdown } from './utils'
/** Split a string by double newlines and filters out empty segments. */
function splitIntro (intro : string) {
diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
index 298bb38..3247405 100644
--- a/client/src/components/infoview/main.tsx
+++ b/client/src/components/infoview/main.tsx
@@ -21,7 +21,6 @@ import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
import { useAppDispatch, useAppSelector } from '../../hooks';
import { LevelInfo, useGetGameInfoQuery, useLoadLevelQuery } from '../../state/api';
import { changedInventory, levelCompleted, selectCode, selectCompleted, selectInventory } from '../../state/progress';
-import Markdown from '../markdown';
import { Infos } from './infos';
import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages';
@@ -29,7 +28,6 @@ import { Goal, isLastStepWithErrors, lastStepHasErrors, loadGoals } from './goal
import { ChatContext, PageContext, PreferencesContext, MonacoEditorContext, ProofContext, GameIdContext } from '../../state/context';
import { Typewriter, getInteractiveDiagsAt, hasErrors, hasInteractiveErrors } from './typewriter';
import { InteractiveDiagnostic } from '@leanprover/infoview/*';
-import { Button } from '../button';
import { CircularProgress } from '@mui/material';
import { GameHint, InteractiveGoalsWithHints, ProofState } from './rpc_api';
import { store } from '../../state/store';
@@ -39,6 +37,7 @@ import { useTranslation } from 'react-i18next';
import path from 'path';
import { useContext } from 'react';
import { Hints, MoreHelpButton, filterHints } from '../chat';
+import { Button, Markdown } from '../utils'
/** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is
diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx
index d6150b0..66cfe78 100644
--- a/client/src/components/inventory.tsx
+++ b/client/src/components/inventory.tsx
@@ -4,7 +4,6 @@ import '../css/inventory.css'
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
import { faLock, faBan, faCheck, faXmark } from '@fortawesome/free-solid-svg-icons'
import { faClipboard } from '@fortawesome/free-regular-svg-icons'
-import Markdown from './markdown';
import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api';
import { selectDifficulty, selectInventory } from '../state/progress';
import { store } from '../state/store';
@@ -12,7 +11,7 @@ import { useSelector } from 'react-redux';
import { useTranslation } from 'react-i18next';
import { t } from 'i18next';
import { NavButton } from './navigation';
-import { LoadingIcon } from './utils';
+import { LoadingIcon, Markdown } from './utils';
import { GameIdContext } from '../state/context';
diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx
index 720e1b6..2cc1c56 100644
--- a/client/src/components/landing_page.tsx
+++ b/client/src/components/landing_page.tsx
@@ -10,7 +10,6 @@ import '@fontsource/roboto/700.css';
import '../css/landing_page.css'
import bgImage from '../assets/bg.jpg'
-import Markdown from './markdown';
import { GameTile, useGetGameInfoQuery } from '../state/api'
import path from 'path';
@@ -20,6 +19,7 @@ import i18next from 'i18next';
import { useContext } from 'react';
import { PopupContext } from './popup/popup';
import { Flag } from './flag';
+import { Markdown } from './utils';
function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
let { t } = useTranslation()
diff --git a/client/src/components/markdown.tsx b/client/src/components/markdown.tsx
deleted file mode 100644
index 804c9c1..0000000
--- a/client/src/components/markdown.tsx
+++ /dev/null
@@ -1,20 +0,0 @@
-import * as React from 'react';
-import ReactMarkdown from 'react-markdown';
-import remarkMath from 'remark-math'
-import rehypeKatex from 'rehype-katex'
-import rehypeRaw from 'rehype-raw'
-import 'katex/dist/katex.min.css' // `rehype-katex` does not import the CSS for you
-import gfm from "remark-gfm";
-
-function Markdown(props) {
- const newProps = {
- ...props,
- remarkPlugins: [...props.remarkPlugins ?? [], remarkMath, gfm],
- rehypePlugins: [...props.remarkPlugins ?? [], rehypeKatex, rehypeRaw],
- };
- return (
-
- );
-}
-
-export default Markdown
diff --git a/client/src/components/popup/erase.tsx b/client/src/components/popup/erase.tsx
index 3fc67e1..afda0ca 100644
--- a/client/src/components/popup/erase.tsx
+++ b/client/src/components/popup/erase.tsx
@@ -3,7 +3,7 @@ import { useSelector } from 'react-redux'
import { useAppDispatch } from '../../hooks'
import { deleteProgress, selectProgress } from '../../state/progress'
import { downloadFile } from '../world_tree'
-import { Button } from '../button'
+import { Button } from '../utils'
import { Trans, useTranslation } from 'react-i18next'
import { useContext } from 'react'
import { PopupContext } from './popup'
diff --git a/client/src/components/popup/info.tsx b/client/src/components/popup/info.tsx
index 7ff4f90..ddc9bd4 100644
--- a/client/src/components/popup/info.tsx
+++ b/client/src/components/popup/info.tsx
@@ -1,6 +1,6 @@
import * as React from 'react'
import { Typography } from '@mui/material'
-import Markdown from '../markdown'
+import { Markdown } from '../utils'
import { Trans, useTranslation } from 'react-i18next'
import { useGetGameInfoQuery } from '../../state/api'
import { GameIdContext } from '../../state/context'
diff --git a/client/src/components/popup/preferences.tsx b/client/src/components/popup/preferences.tsx
index ac6d8ed..8390c15 100644
--- a/client/src/components/popup/preferences.tsx
+++ b/client/src/components/popup/preferences.tsx
@@ -1,6 +1,6 @@
import * as React from 'react'
import { Input, MenuItem, Select, SelectChangeEvent, Typography } from '@mui/material'
-import Markdown from '../markdown'
+import { Markdown } from '../utils'
import { Switch, Button, ButtonGroup } from '@mui/material';
import Box from '@mui/material/Box';
import Slider from '@mui/material/Slider';
diff --git a/client/src/components/popup/upload.tsx b/client/src/components/popup/upload.tsx
index 5269e29..85511c3 100644
--- a/client/src/components/popup/upload.tsx
+++ b/client/src/components/popup/upload.tsx
@@ -6,7 +6,7 @@ import { useSelector } from 'react-redux'
import { useAppDispatch } from '../../hooks'
import { GameProgressState, loadProgress, selectProgress } from '../../state/progress'
import { downloadFile } from '../world_tree'
-import { Button } from '../button'
+import { Button } from '../utils'
import { Trans, useTranslation } from 'react-i18next'
import { PopupContext } from './popup'
import { useContext } from 'react'
diff --git a/client/src/components/utils.tsx b/client/src/components/utils.tsx
index c4756eb..d564380 100644
--- a/client/src/components/utils.tsx
+++ b/client/src/components/utils.tsx
@@ -1,8 +1,43 @@
-import * as React from 'react';
-import { Box, CircularProgress } from "@mui/material";
+import * as React from 'react'
+import { Link, LinkProps } from "react-router-dom"
+import { Box, CircularProgress } from "@mui/material"
+import ReactMarkdown from 'react-markdown'
+import remarkMath from 'remark-math'
+import rehypeKatex from 'rehype-katex'
+import rehypeRaw from 'rehype-raw'
+import 'katex/dist/katex.min.css' // `rehype-katex` does not import the CSS for you
+import gfm from "remark-gfm"
+/** Simple loading icon */
export function LoadingIcon () {
return
}
+
+export interface ButtonProps extends LinkProps {
+ disabled?: boolean
+ inverted?: string // Apparently "inverted" in DOM cannot be `boolean` but must be `inverted`
+}
+
+
+/** Our own button class */
+export function Button(props: ButtonProps) {
+ if (props.disabled) {
+ return {props.children}
+ } else {
+ return {props.children}
+ }
+}
+
+/** Spiced-up markdown */
+export function Markdown(props) {
+ const newProps = {
+ ...props,
+ remarkPlugins: [...props.remarkPlugins ?? [], remarkMath, gfm],
+ rehypePlugins: [...props.remarkPlugins ?? [], rehypeKatex, rehypeRaw],
+ };
+ return (
+
+ );
+}