prettier hints

client/src/components/infoview/goals.tsx

@@ -7,6 +7,7 @@ import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/
 import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
 import { Locations, LocationsContext, SelectableLocation } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation';
 import { GameInteractiveGoal, GameInteractiveGoals } from './rpcApi';
+import { Hints } from './hints';
 
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
 function isInaccessibleName(h: string): boolean {
@@ -142,8 +143,7 @@ export const Goal = React.memo((props: GoalProps) => {
     if (props.goal.goal.isInserted) cn += 'b--inserted '
     if (props.goal.goal.isRemoved) cn += 'b--removed '
 
-    // TODO: make this prettier
-    const hints = goal.hints.map((m) => <div>{m.text}</div>)
+    const hints = <Hints hints={goal.hints} />
 
     if (goal.goal.userName) {
         return <details open className={cn}>

client/src/components/infoview/hints.tsx

@@ -0,0 +1,29 @@
+import { GameHint } from "./rpcApi";
+import * as React from 'react';
+import { Alert, FormControlLabel, Switch } from '@mui/material';
+import Markdown from '../Markdown';
+
+function Hint({hint} : {hint: GameHint}) {
+  return <Alert severity="info" sx={{ mt: 1 }}><Markdown>{hint.text}</Markdown></Alert>
+}
+
+export function Hints({hints} : {hints: GameHint[]}) {
+
+
+  const [showHints, setShowHints] = React.useState(false);
+  const hasHints = hints.length > 0
+
+
+  const openHints = hints.filter(hint => !hint.hidden)
+  const hiddenHints = hints.filter(hint => hint.hidden)
+
+  return <>
+    {openHints.map(hint => <Hint hint={hint} />)}
+    {hasHints &&
+        <FormControlLabel
+          control={<Switch checked={showHints} onChange={() => setShowHints((prev) => !prev)} />}
+          label="More Help?"
+        />}
+    {showHints && hiddenHints.map(hint => <Hint hint={hint} />)}
+  </>
+}