-
Notifications
You must be signed in to change notification settings - Fork 40
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
06aa5d5
commit 0c65a2e
Showing
10 changed files
with
221 additions
and
124 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,60 @@ | ||
| /** | ||
| * @fileOverview | ||
| */ | ||
| import * as React from 'react' | ||
| import { useSelector } from 'react-redux' | ||
| import { GameIdContext } from '../../app' | ||
| import { useAppDispatch } from '../../hooks' | ||
| import { deleteProgress, selectProgress } from '../../state/progress' | ||
| import { downloadFile } from '../world_tree' | ||
| import { Button } from '../button' | ||
|
|
||
|
|
||
| /** Pop-up to delete game progress. | ||
| * | ||
| * `handleClose` is the function to close it again because it's open/closed state is | ||
| * controlled by the containing element. | ||
| */ | ||
| export function ErasePopup ({handleClose}) { | ||
| const gameId = React.useContext(GameIdContext) | ||
| const gameProgress = useSelector(selectProgress(gameId)) | ||
| const dispatch = useAppDispatch() | ||
|
|
||
| /** Download the current progress (i.e. what's saved in the browser store) */ | ||
| const downloadProgress = (e) => { | ||
| e.preventDefault() | ||
| downloadFile({ | ||
| data: JSON.stringify(gameProgress, null, 2), | ||
| fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`, | ||
| fileType: 'text/json', | ||
| }) | ||
| } | ||
|
|
||
| const eraseProgress = () => { | ||
| dispatch(deleteProgress({game: gameId})) | ||
| handleClose() | ||
| } | ||
|
|
||
| const downloadAndErase = (e) => { | ||
| downloadProgress(e) | ||
| eraseProgress() | ||
| } | ||
|
|
||
| return <div className="modal-wrapper"> | ||
| <div className="modal-backdrop" onClick={handleClose} /> | ||
| <div className="modal"> | ||
| <div className="codicon codicon-close modal-close" onClick={handleClose}></div> | ||
| <h2>Delete Progress?</h2> | ||
|
|
||
| <p>Do you want to delete your saved progress irreversibly?</p> | ||
| <p> | ||
| (This deletes your proofs and your collected inventory. | ||
| Saves from other games are not deleted.) | ||
| </p> | ||
|
|
||
| <Button onClick={eraseProgress} to="">Delete</Button> | ||
| <Button onClick={downloadAndErase} to="">Download & Delete</Button> | ||
| <Button onClick={handleClose} to="">Cancel</Button> | ||
| </div> | ||
| </div> | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,23 @@ | ||
| /** | ||
| * @fileOverview | ||
| */ | ||
| import * as React from 'react' | ||
| import { Typography } from '@mui/material' | ||
| import Markdown from '../markdown' | ||
|
|
||
| /** Pop-up that is displaying the Game Info. | ||
| * | ||
| * `handleClose` is the function to close it again because it's open/closed state is | ||
| * controlled by the containing element. | ||
| */ | ||
| export function InfoPopup ({info, handleClose}: {info: string, handleClose: () => void}) { | ||
| return <div className="modal-wrapper"> | ||
| <div className="modal-backdrop" onClick={handleClose} /> | ||
| <div className="modal"> | ||
| <div className="codicon codicon-close modal-close" onClick={handleClose}></div> | ||
| <Typography variant="body1" component="div" className="welcome-text"> | ||
| <Markdown>{info}</Markdown> | ||
| </Typography> | ||
| </div> | ||
| </div> | ||
| } |
File renamed without changes.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,55 @@ | ||
| /** | ||
| * @fileOverview | ||
| */ | ||
| import * as React from 'react' | ||
|
|
||
| /** Pop-up that is displayed when opening the help explaining the game rules. | ||
| * | ||
| * `handleClose` is the function to close it again because it's open/closed state is | ||
| * controlled by the containing element. | ||
| */ | ||
| export function RulesHelpPopup ({handleClose}: {handleClose: () => void}) { | ||
| return <div className="privacy-policy modal-wrapper"> | ||
| <div className="modal-backdrop" onClick={handleClose} /> | ||
| <div className="modal"> | ||
| <div className="codicon codicon-close modal-close" onClick={handleClose}></div> | ||
| <h2>Game Rules</h2> | ||
| <p> | ||
| Game rules determine if it is allowed to skip levels and if the games runs checks to only | ||
| allow unlocked tactics and theorems in proofs. | ||
| </p> | ||
| <p> | ||
| Note: "Unlocked" tactics (or theorems) are determined by two things: The set of minimal | ||
| tactics needed to solve a level, plus any tactics you unlocked in another level. That means | ||
| if you unlock <code>simp</code> in a level, you can use it henceforth in any level. | ||
| </p> | ||
| <p>The options are:</p> | ||
| <table> | ||
| <thead> | ||
| <tr> | ||
| <th scope="col"></th> | ||
| <th scope="col">levels</th> | ||
| <th scope="col">tactics</th> | ||
| </tr> | ||
| </thead> | ||
| <tbody> | ||
| <tr> | ||
| <th scope="row">regular</th> | ||
| <td>🔐</td> | ||
| <td>🔐</td> | ||
| </tr> | ||
| <tr> | ||
| <th scope="row">relaxed</th> | ||
| <td>🔓</td> | ||
| <td>🔐</td> | ||
| </tr> | ||
| <tr> | ||
| <th scope="row">none</th> | ||
| <td>🔓</td> | ||
| <td>🔓</td> | ||
| </tr> | ||
| </tbody> | ||
| </table> | ||
| </div> | ||
| </div> | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,70 @@ | ||
| /** | ||
| * @fileOverview | ||
| */ | ||
| import * as React from 'react' | ||
| import { useSelector } from 'react-redux' | ||
| import { GameIdContext } from '../../app' | ||
| import { useAppDispatch } from '../../hooks' | ||
| import { GameProgressState, loadProgress, selectProgress } from '../../state/progress' | ||
| import { downloadFile } from '../world_tree' | ||
| import { Button } from '../button' | ||
|
|
||
| /** Pop-up that is displaying the Game Info. | ||
| * | ||
| * `handleClose` is the function to close it again because it's open/closed state is | ||
| * controlled by the containing element. | ||
| */ | ||
| export function UploadPopup ({handleClose}) { | ||
| const [file, setFile] = React.useState<File>(); | ||
| const gameId = React.useContext(GameIdContext) | ||
| const gameProgress = useSelector(selectProgress(gameId)) | ||
| const dispatch = useAppDispatch() | ||
|
|
||
| const handleFileChange = (e) => { | ||
| if (e.target.files) { | ||
| setFile(e.target.files[0]) | ||
| } | ||
| } | ||
|
|
||
| /** Upload progress from a */ | ||
| const uploadProgress = (e) => { | ||
| if (!file) {return} | ||
| const fileReader = new FileReader() | ||
| fileReader.readAsText(file, "UTF-8") | ||
| fileReader.onload = (e) => { | ||
| const data = JSON.parse(e.target.result.toString()) as GameProgressState | ||
| console.debug("Json Data", data) | ||
| dispatch(loadProgress({game: gameId, data: data})) | ||
| } | ||
| handleClose() | ||
| } | ||
|
|
||
| /** Download the current progress (i.e. what's saved in the browser store) */ | ||
| const downloadProgress = (e) => { | ||
| e.preventDefault() | ||
| downloadFile({ | ||
| data: JSON.stringify(gameProgress, null, 2), | ||
| fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`, | ||
| fileType: 'text/json', | ||
| }) | ||
| } | ||
|
|
||
|
|
||
| return <div className="modal-wrapper"> | ||
| <div className="modal-backdrop" onClick={handleClose} /> | ||
| <div className="modal"> | ||
| <div className="codicon codicon-close modal-close" onClick={handleClose}></div> | ||
| <h2>Upload Saved Progress</h2> | ||
|
|
||
| <p>Select a JSON file with the saved game progress to load your progress.</p> | ||
|
|
||
| <p><b>Warning:</b> This will delete your current game progress! | ||
| Consider <a className="download-link" onClick={downloadProgress} >downloading your current progress</a> first!</p> | ||
| <p> | ||
| <input type="file" onChange={handleFileChange}/> | ||
| </p> | ||
|
|
||
| <Button to="" onClick={uploadProgress}>Load selected file</Button> | ||
| </div> | ||
| </div> | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.