apply suggestions from PR #206 manually

pull/224/head
Jon Eugster 11 months ago
parent 74059bd5af
commit d456621875

@ -7,7 +7,7 @@
"tactics": "策略", "tactics": "策略",
"regular": "标准", "regular": "标准",
"relaxed": "休闲", "relaxed": "休闲",
"none": "", "none": "自由",
"Rules": "规则", "Rules": "规则",
"Intro": "介绍", "Intro": "介绍",
"Game Introduction": "游戏介绍", "Game Introduction": "游戏介绍",
@ -15,11 +15,11 @@
"Start": "开始", "Start": "开始",
"Inventory": "定理清单", "Inventory": "定理清单",
"next level": "下一关", "next level": "下一关",
"Next": "下一", "Next": "下一",
"back to world selection": "返回世界选择", "back to world selection": "返回世界选择",
"Leave World": "离开世界", "Leave World": "离开世界",
"previous level": "上一关", "previous level": "上一关",
"Previous": "上一", "Previous": "上一",
"Editor mode is enforced!": "编辑器模式开启!", "Editor mode is enforced!": "编辑器模式开启!",
"Editor mode": "编辑器模式", "Editor mode": "编辑器模式",
"Typewriter mode": "打字机模式", "Typewriter mode": "打字机模式",
@ -41,7 +41,7 @@
"Show more help!": "显示更多帮助!", "Show more help!": "显示更多帮助!",
"Goal": "目标", "Goal": "目标",
"Current Goal": "当前目标", "Current Goal": "当前目标",
"Objects": "Objects", "Objects": "对象",
"Assumptions": "假设", "Assumptions": "假设",
"Further Goals": "Further Goals", "Further Goals": "Further Goals",
"No Goals": "无目标", "No Goals": "无目标",

@ -140,6 +140,7 @@ interface GoalProps {
* provided `filter`. */ * provided `filter`. */
export const Goal = React.memo((props: GoalProps) => { export const Goal = React.memo((props: GoalProps) => {
const { goal, filter, showHints, typewriter } = props const { goal, filter, showHints, typewriter } = props
let { t } = useTranslation()
// TODO: Apparently `goal` can be `undefined` // TODO: Apparently `goal` can be `undefined`
if (!goal) {return <></>} if (!goal) {return <></>}
@ -153,7 +154,7 @@ export const Goal = React.memo((props: GoalProps) => {
undefined, undefined,
[locs, goal.mvarId]) [locs, goal.mvarId])
const goalLi = <div key={'goal'}> const goalLi = <div key={'goal'}>
<div className="goal-title">Goal: </div> <div className="goal-title">{t("Goal")}:</div>
<LocationsContext.Provider value={goalLocs}> <LocationsContext.Provider value={goalLocs}>
<InteractiveCode fmt={goal.type} /> <InteractiveCode fmt={goal.type} />
</LocationsContext.Provider> </LocationsContext.Provider>
@ -171,10 +172,10 @@ export const Goal = React.memo((props: GoalProps) => {
{/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */} {/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */}
{filter.reverse && goalLi} {filter.reverse && goalLi}
{! typewriter && objectHyps.length > 0 && {! typewriter && objectHyps.length > 0 &&
<div className="hyp-group"><div className="hyp-group-title">Objects:</div> <div className="hyp-group"><div className="hyp-group-title">{t("Objects")}:</div>
{objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> } {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
{!typewriter && assumptionHyps.length > 0 && {!typewriter && assumptionHyps.length > 0 &&
<div className="hyp-group"><div className="hyp-group-title">Assumptions:</div> <div className="hyp-group"><div className="hyp-group-title">{t("Assumptions")}:</div>
{assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> } {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
{!filter.reverse && goalLi} {!filter.reverse && goalLi}
{/* {showHints && hints} */} {/* {showHints && hints} */}

@ -469,7 +469,7 @@ function IntroductionPanel({gameInfo}) {
{gameInfo.data?.worldSize[worldId] == 0 ? {gameInfo.data?.worldSize[worldId] == 0 ?
<Button to={`/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button> : <Button to={`/${gameId}`}><FontAwesomeIcon icon={faHome} /></Button> :
<Button to={`/${gameId}/world/${worldId}/level/1`}> <Button to={`/${gameId}/world/${worldId}/level/1`}>
Start&nbsp;<FontAwesomeIcon icon={faArrowRight} /> {t("Start")}&nbsp;<FontAwesomeIcon icon={faArrowRight} />
</Button> </Button>
} }
</div> </div>

Loading…
Cancel
Save