feat: image support in Markdown text (leanprover-community#359)

Author: joneugster

client/src/components/hints.tsx

@@ -1,6 +1,6 @@
 import { GameHint, InteractiveGoalsWithHints, ProofState } from "./infoview/rpc_api";
 import * as React from 'react';
-import Markdown from './markdown';
+import { Markdown } from './markdown';
 import { DeletedChatContext, ProofContext } from "./infoview/context";
 import { lastStepHasErrors } from "./infoview/goals";
 import { Button } from "./button";

client/src/components/infoview/main.tsx

@@ -22,7 +22,7 @@ import { GameIdContext } from '../../app';
 import { useAppDispatch, useAppSelector } from '../../hooks';
 import { LevelInfo, useGetGameInfoQuery } from '../../state/api';
 import { changedInventory, levelCompleted, selectCode, selectCompleted, selectInventory } from '../../state/progress';
-import Markdown from '../markdown';
+import { Markdown } from '../markdown';
 
 import { Infos } from './infos';
 import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages';

client/src/components/inventory.tsx

@@ -5,7 +5,7 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faLock, faBan, faCheck } from '@fortawesome/free-solid-svg-icons'
 import { faClipboard } from '@fortawesome/free-regular-svg-icons'
 import { GameIdContext } from '../app';
-import Markdown from './markdown';
+import { Markdown } from './markdown';
 import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery } from '../state/api';
 import { selectDifficulty, selectInventory } from '../state/progress';
 import { store } from '../state/store';

client/src/components/landing_page.tsx

@@ -10,7 +10,7 @@ import '@fontsource/roboto/700.css';
 import '../css/landing_page.css'
 import bgImage from '../assets/bg.jpg'
 
-import Markdown from './markdown';
+import { Markdown } from './markdown';
 import {PrivacyPolicyPopup} from './popup/privacy_policy'
 import { GameTile, useGetGameInfoQuery } from '../state/api'
 import path from 'path';

client/src/components/level.tsx

@@ -25,7 +25,7 @@ import { changedSelection, codeEdited, selectCode, selectSelections, selectCompl
   selectHelp, selectDifficulty, selectInventory, selectTypewriterMode, changeTypewriterMode } from '../state/progress'
 import { store } from '../state/store'
 import { Button } from './button'
-import Markdown from './markdown'
+import { Markdown } from './markdown'
 import {InventoryPanel} from './inventory'
 import { hasInteractiveErrors } from './infoview/typewriter'
 import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext,

client/src/components/markdown.tsx

@@ -1,19 +1,31 @@
 import * as React from 'react';
+import { useContext } 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
 import gfm from "remark-gfm";
+import { GameIdContext } from '../app';
 
-function Markdown(props) {
-    const newProps = {
-        ...props,
-        remarkPlugins: [...props.remarkPlugins ?? [], remarkMath, gfm],
-        rehypePlugins: [...props.remarkPlugins ?? [], rehypeKatex],
-      };
-      return (
-        <ReactMarkdown {...newProps} className="markdown" />
-      );
-}
+export function Markdown(props: any) {
+  const gameId = useContext(GameIdContext)
+  // Prefix image URLs of the form  `![...](images/...)` with the game ID
+  let children = props?.children
+
+  if (typeof children === "string") {
+    children = children.replace(
+      /!\[([^\]]+)\]\((images\/[^\)]+)\)/g,
+      (match, text, url) => `![${text}](data/${gameId}/${url})`
+    );
+  }
 
-export default Markdown
+  const newProps = {
+    ...props,
+    children,
+    remarkPlugins: [...props.remarkPlugins ?? [], remarkMath, gfm],
+    rehypePlugins: [...props.remarkPlugins ?? [], rehypeKatex],
+  };
+  return (
+    <ReactMarkdown {...newProps} className="markdown" />
+  );
+}

client/src/components/message.tsx

@@ -5,7 +5,7 @@ import '@fontsource/roboto/500.css';
 import '@fontsource/roboto/700.css';
 
 import { Button, Dialog, DialogContent, DialogContentText, DialogActions } from '@mui/material';
-import Markdown from './markdown';
+import { Markdown } from './markdown';
 
 function Message({ isOpen, content, close }) {
 

client/src/components/popup/game_info.tsx

@@ -3,7 +3,7 @@
 */
 import * as React from 'react'
 import { Typography } from '@mui/material'
-import Markdown from '../markdown'
+import { Markdown } from '../markdown'
 import { useTranslation } from 'react-i18next'
 import { GameIdContext } from '../../app'
 

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 '../markdown'
 import { Switch, Button, ButtonGroup } from '@mui/material';
 import Box from '@mui/material/Box';
 import Slider from '@mui/material/Slider';

doc/create_game.md

@@ -282,6 +282,8 @@ in one of the files you created in 2), 3), or 4) (i.e. game/world/level).
 
 NOTE: At present, only the images for a world are displayed. They appear in the introduction of the world.
 
+You can also embed images in the text as descriped in [Markdown](markdown.md).
+
 ## 7. Update your game
 
 In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](update_game.md).
@@ -311,6 +313,15 @@ CoverImage "images/cover.png"
 
 ## 10. Advanced Topics
 
+### Markdown
+
+Texts should generally support markdown. For some tips on how to use markdown, see
+[Markdown styling](markdown.md).
+
+In particular, you can embed images in texts, see the specific instructions in that file.
+
+
+
 ### Escaping
 
 Inside strings, you need to escape backslashes, but not inside doc-strings, therefore you