From d2fd1c59150cd501573f96ed55cf2d9405efc9ba Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Fri, 21 Oct 2022 14:39:01 +0200 Subject: [PATCH] convert tabs to spaces --- client/src/App.tsx | 96 ++++++------- client/src/components/GoodBye.tsx | 20 +-- client/src/components/LeftPanel.tsx | 110 +++++++-------- client/src/components/Level.tsx | 186 +++++++++++++------------- client/src/components/TacticState.tsx | 102 +++++++------- client/src/components/Welcome.tsx | 72 +++++----- 6 files changed, 293 insertions(+), 293 deletions(-) diff --git a/client/src/App.tsx b/client/src/App.tsx index 400eb2b..ec5e56a 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -16,67 +16,67 @@ import GoodBye from './components/GoodBye'; import useWebSocket from 'react-use-websocket'; function App() { - const [title, setTitle] = useState("") - const [conclusion, setConclusion] = useState("") - const [levelTitle, setLevelTitle] = useState("") - const [nbLevels, setNbLevels] = useState(0) - const [curLevel, setCurLevel] = useState(0) - const [finished, setFinished] = useState(false) - const [rpcConnection, setRpcConnection] = useState(null) + const [title, setTitle] = useState("") + const [conclusion, setConclusion] = useState("") + const [levelTitle, setLevelTitle] = useState("") + const [nbLevels, setNbLevels] = useState(0) + const [curLevel, setCurLevel] = useState(0) + const [finished, setFinished] = useState(false) + const [rpcConnection, setRpcConnection] = useState(null) - const socketUrl = 'ws://' + window.location.host + '/websocket/' + const socketUrl = 'ws://' + window.location.host + '/websocket/' - useWebSocket(socketUrl, { - onOpen: function (ev) { - const logger = new rpc.ConsoleLogger(); + useWebSocket(socketUrl, { + onOpen: function (ev) { + const logger = new rpc.ConsoleLogger(); const socket = rpc.toSocket(ev.target as WebSocket); - let rpcConnection = rpc.createWebSocketConnection(socket, logger) + let rpcConnection = rpc.createWebSocketConnection(socket, logger) setRpcConnection(rpcConnection); - rpcConnection.listen(); - } - }) + rpcConnection.listen(); + } + }) - const mathJaxConfig = { - loader: { - load: ['input/tex-base', 'output/svg'] - }, + const mathJaxConfig = { + loader: { + load: ['input/tex-base', 'output/svg'] + }, tex: { - inlineMath: [['$', '$'], ['\\(', '\\)']] - }, - svg: { - fontCache: 'global' - } + inlineMath: [['$', '$'], ['\\(', '\\)']] + }, + svg: { + fontCache: 'global' + } } - function startGame() { - setCurLevel(1) - } + function startGame() { + setCurLevel(1) + } - let mainComponent; - if (finished) { - mainComponent = - } else if (curLevel > 0) { - mainComponent = - } else { + let mainComponent; + if (finished) { + mainComponent = + } else if (curLevel > 0) { + mainComponent = + } else { mainComponent = - } + } return (
- - - theme.zIndex.drawer + 1 }}> - - - {title} - - - {levelTitle} - - - - {mainComponent} - + + + theme.zIndex.drawer + 1 }}> + + + {title} + + + {levelTitle} + + + + {mainComponent} +
) } diff --git a/client/src/components/GoodBye.tsx b/client/src/components/GoodBye.tsx index e6d135f..7dbf6de 100644 --- a/client/src/components/GoodBye.tsx +++ b/client/src/components/GoodBye.tsx @@ -8,16 +8,16 @@ import { Box, Typography, Grid } from '@mui/material'; function GoodBye({ message }) { - return ( - - - {message} - - - ) + return ( + + + {message} + + + ) } export default GoodBye diff --git a/client/src/components/LeftPanel.tsx b/client/src/components/LeftPanel.tsx index 3f4132d..b46ddb3 100644 --- a/client/src/components/LeftPanel.tsx +++ b/client/src/components/LeftPanel.tsx @@ -12,72 +12,72 @@ import ExpandMoreIcon from '@mui/icons-material/ExpandMore'; function TacticDoc(props) { - return ( - - }> - {props.tactic.name} - - - - {props.tactic.content} - - - ) + return ( + + }> + {props.tactic.name} + + + + {props.tactic.content} + + + ) } function LemmaDoc({ lemma }) { - return ( - - }> - {lemma.userName} - - - - {lemma.content} - - - ) + return ( + + }> + {lemma.userName} + + + + {lemma.content} + + + ) } function LemmaDocs({ lemmas }) { - const [categories, setCategories] = useState(new Map()) - const [curCategory, setCurCategory] = useState("") + const [categories, setCategories] = useState(new Map()) + const [curCategory, setCurCategory] = useState("") - useEffect(() => { - const cats = new Map() - lemmas.forEach(function (item) { - const category = item.category - cats.set(category, (cats.get(category) || []).concat([item])) - }); - setCategories(cats) - setCurCategory(cats.keys().next().value) - }, [lemmas]); + useEffect(() => { + const cats = new Map() + lemmas.forEach(function (item) { + const category = item.category + cats.set(category, (cats.get(category) || []).concat([item])) + }); + setCategories(cats) + setCurCategory(cats.keys().next().value) + }, [lemmas]); - return ( - - Inventory - - - {(Array.from(categories)).map(([category, _]) => )} - - - {curCategory && categories.get(curCategory).map((lemma) => )} - - ) + return ( + + Inventory + + + {(Array.from(categories)).map(([category, _]) => )} + + + {curCategory && categories.get(curCategory).map((lemma) => )} + + ) } function LeftPanel({ spells, inventory }) { - return ( - - {spells.length > 0 && - - Spell book - {spells.map((spell) => )} - } - {inventory.length > 0 && } - ) + return ( + + {spells.length > 0 && + + Spell book + {spells.map((spell) => )} + } + {inventory.length > 0 && } + ) } export default LeftPanel; diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index b2ae295..ebdd271 100644 --- a/client/src/components/Level.tsx +++ b/client/src/components/Level.tsx @@ -16,102 +16,102 @@ import * as rpc from 'vscode-ws-jsonrpc'; interface LevelProps { rpcConnection: null|rpc.MessageConnection; nbLevels: any; - level: any; - setCurLevel: any; - setLevelTitle: any; - setFinished: any + level: any; + setCurLevel: any; + setLevelTitle: any; + setFinished: any } function Level({ rpcConnection, nbLevels, level, setCurLevel, setLevelTitle, setFinished }: LevelProps) { - const [index, setIndex] = useState(level) // Level number - const [tacticDocs, setTacticDocs] = useState([]) - const [lemmaDocs, setLemmaDocs] = useState([]) - - const [leanData, setLeanData] = useState({goals: []}) - const [history, setHistory] = useState([]) - const [lastTactic, setLastTactic] = useState("") - const [errors, setErrors] = useState([]) - - const [message, setMessage] = useState("") - const [messageOpen, setMessageOpen] = useState(false) - - - const [completed, setCompleted] = useState(false) - - const processResponse = (res:any) => { - setLeanData(res); - setErrors(res.errors); - if (res.message !== "" && res.errors?.length === 0) { - setMessage(res.message) - setMessageOpen(true) - } - if (res.goals?.length === 0 && res.errors?.length === 0) { - setCompleted(true) - } - } - - // The next function will be called when the level changes - useEffect(() => { - if (rpcConnection) { - rpcConnection.sendRequest("loadLevel", {number: level}).then((res) => { - setLevelTitle("Level " + res["index"] + ": " + res["title"]) - setIndex(parseInt(res["index"])) - setTacticDocs(res["tactics"]) - setLemmaDocs(res["lemmas"]) - processResponse(res) - }); - } - }, [level, rpcConnection]) - - function sendTactic(input) { - rpcConnection.sendRequest("runTactic", {tactic: input}).then(processResponse); - setLastTactic(input); - setHistory(history.concat([input])); - } - - function undo() { - if (errors.length === 0) { - rpcConnection.sendRequest('undo').then(processResponse); - } - if (history.length > 1) { - setLastTactic(history[history.length - 1]); - } else { - setLastTactic(""); - }; - setErrors([]); - setHistory(history.slice(0, -1)); - } - - function loadNextLevel() { - setCompleted(false) - setHistory([]) - setCurLevel(index + 1) - } - - function closeMessage() { - setMessageOpen(false) - } - - function finishGame() { - setLevelTitle("") - setFinished(true) - } - - return ( - - - - - - - - - - - - - ) + const [index, setIndex] = useState(level) // Level number + const [tacticDocs, setTacticDocs] = useState([]) + const [lemmaDocs, setLemmaDocs] = useState([]) + + const [leanData, setLeanData] = useState({goals: []}) + const [history, setHistory] = useState([]) + const [lastTactic, setLastTactic] = useState("") + const [errors, setErrors] = useState([]) + + const [message, setMessage] = useState("") + const [messageOpen, setMessageOpen] = useState(false) + + + const [completed, setCompleted] = useState(false) + + const processResponse = (res:any) => { + setLeanData(res); + setErrors(res.errors); + if (res.message !== "" && res.errors?.length === 0) { + setMessage(res.message) + setMessageOpen(true) + } + if (res.goals?.length === 0 && res.errors?.length === 0) { + setCompleted(true) + } + } + + // The next function will be called when the level changes + useEffect(() => { + if (rpcConnection) { + rpcConnection.sendRequest("loadLevel", {number: level}).then((res) => { + setLevelTitle("Level " + res["index"] + ": " + res["title"]) + setIndex(parseInt(res["index"])) + setTacticDocs(res["tactics"]) + setLemmaDocs(res["lemmas"]) + processResponse(res) + }); + } + }, [level, rpcConnection]) + + function sendTactic(input) { + rpcConnection.sendRequest("runTactic", {tactic: input}).then(processResponse); + setLastTactic(input); + setHistory(history.concat([input])); + } + + function undo() { + if (errors.length === 0) { + rpcConnection.sendRequest('undo').then(processResponse); + } + if (history.length > 1) { + setLastTactic(history[history.length - 1]); + } else { + setLastTactic(""); + }; + setErrors([]); + setHistory(history.slice(0, -1)); + } + + function loadNextLevel() { + setCompleted(false) + setHistory([]) + setCurLevel(index + 1) + } + + function closeMessage() { + setMessageOpen(false) + } + + function finishGame() { + setLevelTitle("") + setFinished(true) + } + + return ( + + + + + + + + + + + + + ) } export default Level diff --git a/client/src/components/TacticState.tsx b/client/src/components/TacticState.tsx index b2f3c5b..2e158c6 100644 --- a/client/src/components/TacticState.tsx +++ b/client/src/components/TacticState.tsx @@ -11,59 +11,59 @@ import { Paper, Box, Typography } from '@mui/material'; const errorRegex = /:1:(?[^:]*): (?.*)/; function Goal({ goal }) { - const hasObject = typeof goal.objects === "object" && goal.objects.length > 0 - const hasAssumption = typeof goal.assumptions === "object" && goal.assumptions.length > 0 - return ( - - {hasObject && Objects - - {goal.objects.map((item) => - - {item[0]} : - {item[1]} - )} - } - {hasAssumption && Assumptions - - {goal.assumptions.map((item) => {item[0]} : - {item[1]})} - } - Prove: - {goal.goal} - ) + const hasObject = typeof goal.objects === "object" && goal.objects.length > 0 + const hasAssumption = typeof goal.assumptions === "object" && goal.assumptions.length > 0 + return ( + + {hasObject && Objects + + {goal.objects.map((item) => + + {item[0]} : + {item[1]} + )} + } + {hasAssumption && Assumptions + + {goal.assumptions.map((item) => {item[0]} : + {item[1]})} + } + Prove: + {goal.goal} + ) } function TacticState({ goals, errors, lastTactic, completed }) { - const hasError = typeof errors === "object" && errors.length > 0 - const hasGoal = typeof goals === "object" && goals.length > 0 - const hasManyGoal = hasGoal && goals.length > 1 - var col = "" - var msg = "" - if (hasError) { - const m = errors[0].match(errorRegex) - if (m) { - col = `Column ${m.groups.col}: ` - msg = m.groups.msg - } else { - msg = errors[0] - if (msg === "Unrecognized tactic") { msg = "Unknown spell!" } - } - } - return ( - - {hasGoal && Current goal } - {completed && Level completed ! 🎉} - {hasError && Spell invocation failed - {lastTactic} - {col}{msg} - Use the undo button to go back to a sane state. - } - {hasManyGoal && - Other goals - {goals.slice(1).map((goal, index) => )} - } - - ) + const hasError = typeof errors === "object" && errors.length > 0 + const hasGoal = typeof goals === "object" && goals.length > 0 + const hasManyGoal = hasGoal && goals.length > 1 + var col = "" + var msg = "" + if (hasError) { + const m = errors[0].match(errorRegex) + if (m) { + col = `Column ${m.groups.col}: ` + msg = m.groups.msg + } else { + msg = errors[0] + if (msg === "Unrecognized tactic") { msg = "Unknown spell!" } + } + } + return ( + + {hasGoal && Current goal } + {completed && Level completed ! 🎉} + {hasError && Spell invocation failed + {lastTactic} + {col}{msg} + Use the undo button to go back to a sane state. + } + {hasManyGoal && + Other goals + {goals.slice(1).map((goal, index) => )} + } + + ) } -export default TacticState \ No newline at end of file +export default TacticState diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx index 47ebb74..4c21806 100644 --- a/client/src/components/Welcome.tsx +++ b/client/src/components/Welcome.tsx @@ -13,53 +13,53 @@ import { Box, Typography, Button, CircularProgress, Grid } from '@mui/material'; interface WelcomeProps { rpcConnection: null|rpc.MessageConnection; setNbLevels: any; - setTitle: any; - startGame: any; - setConclusion: any; + setTitle: any; + startGame: any; + setConclusion: any; } type infoResultType = { - title: string, - nb_levels: any[], - conclusion: string + title: string, + nb_levels: any[], + conclusion: string } const infoRequestType = new rpc.RequestType0("info") function Welcome({ rpcConnection, setNbLevels, setTitle, startGame, setConclusion }: WelcomeProps) { - const [leanData, setLeanData] = useState(null) + const [leanData, setLeanData] = useState(null) - useEffect(() => { - if (rpcConnection) { // Will run in the beginning as soon as RPC connection is established - rpcConnection.sendRequest(infoRequestType).then((res: infoResultType) =>{ - setLeanData(res) - setNbLevels(res.nb_levels) - setTitle(res.title) - document.title = res.title - setConclusion(res.conclusion) - }); - } - }, [rpcConnection, setLeanData, setNbLevels, setTitle, setConclusion]) + useEffect(() => { + if (rpcConnection) { // Will run in the beginning as soon as RPC connection is established + rpcConnection.sendRequest(infoRequestType).then((res: infoResultType) =>{ + setLeanData(res) + setNbLevels(res.nb_levels) + setTitle(res.title) + document.title = res.title + setConclusion(res.conclusion) + }); + } + }, [rpcConnection, setLeanData, setNbLevels, setTitle, setConclusion]) - let content - if (leanData) { - content = ( - - - {leanData["introduction"]} - - - - - - ) - } else { - content = - } - return - {content} - + let content + if (leanData) { + content = ( + + + {leanData["introduction"]} + + + + + + ) + } else { + content = + } + return + {content} + } export default Welcome