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

style

Browse Source
This commit is contained in:
Jon Eugster
2024-06-11 01:37:48 +02:00
parent 72ccdd1478
commit 9f4fe656c8
1 changed files with 1 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/chat.tsx
+1 -2
View File
@@ -8,13 +8,12 @@ import { faArrowRight } from '@fortawesome/free-solid-svg-icons'
import { changedReadIntro, selectCompleted, selectReadIntro } from '../state/progress' import { changedReadIntro, selectCompleted, selectReadIntro } from '../state/progress'
import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api' import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api'
import { useAppDispatch, useAppSelector } from '../hooks' import { useAppDispatch, useAppSelector } from '../hooks'
import { Button, Markdown } from './utils'
import { ChatContext, GameIdContext, PageContext, PreferencesContext, ProofContext } from '../state/context' import { ChatContext, GameIdContext, PageContext, PreferencesContext, ProofContext } from '../state/context'
import { GameHint, InteractiveGoalsWithHints } from './infoview/rpc_api' import { GameHint, InteractiveGoalsWithHints } from './infoview/rpc_api'
import { lastStepHasErrors } from './infoview/goals' import { lastStepHasErrors } from './infoview/goals'
import '../css/chat.css' import '../css/chat.css'
import { Button, Markdown } from './utils'
/** Split a string by double newlines and filters out empty segments. */ /** Split a string by double newlines and filters out empty segments. */
function splitIntro (intro : string) { function splitIntro (intro : string) {