move Button and Markdown

client/src/components/button.tsx

@@ -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 <span className={`btn btn-disabled ${props.inverted === "true" ? 'btn-inverted' : ''}`} {...props}>{props.children}</span>
-  } else {
-    return <Link className={`btn ${props.inverted === "true" ? 'btn-inverted' : ''}`} {...props}>{props.children}</Link>
-  }
-}

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) {

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

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';
 
 

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()

client/src/components/markdown.tsx

@@ -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 (
-        <ReactMarkdown {...newProps} className="markdown" />
-      );
-}
-
-export default Markdown

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'

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'

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';

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'

client/src/components/utils.tsx

@@ -1,8 +1,43 @@
-import * as React from 'react';
+import * as React from 'react'
-import { Box, CircularProgress } from "@mui/material";
+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 <Box display="flex" alignItems="center" justifyContent="center" sx={{ flex: 1, height: "calc(100vh - 64px)" }}>
     <CircularProgress />
   </Box>
 }
+
+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 <span className={`btn btn-disabled ${props.inverted === "true" ? 'btn-inverted' : ''}`} {...props}>{props.children}</span>
+  } else {
+    return <Link className={`btn ${props.inverted === "true" ? 'btn-inverted' : ''}`} {...props}>{props.children}</Link>
+  }
+}
+
+/** Spiced-up markdown */
+export function Markdown(props) {
+  const newProps = {
+      ...props,
+      remarkPlugins: [...props.remarkPlugins ?? [], remarkMath, gfm],
+      rehypePlugins: [...props.remarkPlugins ?? [], rehypeKatex, rehypeRaw],
+    };
+    return (
+      <ReactMarkdown {...newProps} className="markdown" />
+    );
+}