diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx index a288a15..0a95825 100644 --- a/client/src/components/infoview/goals.tsx +++ b/client/src/components/infoview/goals.tsx @@ -1,13 +1,17 @@ -/* Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/goals.tsx */ +/** + * @fileOverview + * + * Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/goals.tsx +*/ import * as React from 'react' -import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode' import { InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from '@leanprover/infoview-api' -import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips'; import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'; import { Locations, LocationsContext, SelectableLocation } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation'; -import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle } from './rpc_api'; +import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode' +import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips'; import { InputModeContext } from './context'; +import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle } from './rpc_api'; /** Returns true if `h` is inaccessible according to Lean's default name rendering. */ diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index b00fc67..5bb09bc 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -83,7 +83,6 @@ function PlayableLevel({worldId, levelId}) { const theme = useTheme(); - useEffect(() => { // Scroll to top when loading a new level // TODO: Thats the wrong behaviour probably @@ -416,7 +415,9 @@ function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCo editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections())) editor.setModel(model) if (initialSelections) { - editor.setSelections(initialSelections) + console.debug("Initial Selection: ", initialSelections) + // BUG: Somehow I get an `invalid arguments` bug here + // editor.setSelections(initialSelections) } infoviewApi.serverRestarted(leanClient.initializeResult) diff --git a/client/src/components/privacy_policy.tsx b/client/src/components/privacy_policy.tsx index 228d297..8a883db 100644 --- a/client/src/components/privacy_policy.tsx +++ b/client/src/components/privacy_policy.tsx @@ -1,61 +1,62 @@ +/** + * @fileOverview The impressum/privacy policy +*/ import { faShield } from '@fortawesome/free-solid-svg-icons'; import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'; import * as React from 'react' -function PrivacyPolicyPopup ({handleClose}) { +/** Pop-up that is displayed when opening the privacy policy. + * + * `handleClose` is the function to close it again because it's open/closed state is + * controlled by the containing element. + */ +function PrivacyPolicyPopup (handleClose) { return
Our server collects metadata (such as IP address, browser, operating system) - and the data that the user enters into the editor. The data is used to - compute the Lean output and display it to the user. The information will be stored - as long as the user stays on our website and will be deleted immediately afterwards. - We keep logs to improve our software, but the contained data is anonymized.
- -We do not use cookies, but your game progress is stored in the browser +
+ Our server collects metadata (such as IP address, browser, operating system) + and the data that the user enters into the editor. The data is used to + compute the Lean output and display it to the user. The information will be stored + as long as the user stays on our website and will be deleted immediately afterwards. + We keep logs to improve our software, but the contained data is anonymized. +
++ We do not use cookies, but your game progress is stored in the browser as site data. Your game progress is not saved on the server; if you delete your browser storage, it is completely gone.
-Our server is located in Germany.
- -Contact information:
+
+ Contact information:
Jon Eugster
Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf
Universitätsstr. 1
40225 Düsseldorf
Germany
+ +49 211 81-12173
Contact Details
-
legal
-notes
-legal
+notes
+Select a JSON file with the saved game progress to load your progress.
+Select a JSON file with the saved game progress to load your progress.
-Warning: This will delete your current game progress! - Consider downloading your current progress first!
+Warning: This will delete your current game progress! + Consider downloading your current progress first!
- + - -