Compare commits
77 Commits
| Author | SHA1 | Date |
|---|---|---|
|
|
92acdb7f85 | 2 years ago |
|
|
64ad36dd4f | 2 years ago |
|
|
3a885245ae | 2 years ago |
|
|
545ac8b0f7 | 2 years ago |
|
|
5a09776b5b | 2 years ago |
|
|
38cac494ab | 2 years ago |
|
|
5b6f5f0db7 | 2 years ago |
|
|
fbe48d26c5 | 2 years ago |
|
|
d05767d74c | 2 years ago |
|
|
aab6dbb329 | 2 years ago |
|
|
5310e69d98 | 2 years ago |
|
|
67090f53fa | 2 years ago |
|
|
2896237772 | 2 years ago |
|
|
30d9b881b9 | 2 years ago |
|
|
937c4714dd | 2 years ago |
|
|
75b367e3d1 | 2 years ago |
|
|
b815b86c0d | 2 years ago |
|
|
8b4215e407 | 2 years ago |
|
|
a0ecaeeece | 2 years ago |
|
|
dea5fd0558 | 2 years ago |
|
|
c03e2f123e | 2 years ago |
|
|
b1cdcfc113 | 2 years ago |
|
|
503ea51f95 | 2 years ago |
|
|
aed2899fb6 | 2 years ago |
|
|
1f14ad185f | 2 years ago |
|
|
17d2ba5a2c | 2 years ago |
|
|
2a070332f2 | 2 years ago |
|
|
aedf073a33 | 2 years ago |
|
|
d684f260bb | 2 years ago |
|
|
925d729725 | 2 years ago |
|
|
9f4fe656c8 | 2 years ago |
|
|
72ccdd1478 | 2 years ago |
|
|
b66954248f | 2 years ago |
|
|
096bd55f9b | 2 years ago |
|
|
02d0d57453 | 2 years ago |
|
|
762c1ef0c4 | 2 years ago |
|
|
4652f6d50f | 2 years ago |
|
|
f158250341 | 2 years ago |
|
|
7dc0a507ed | 2 years ago |
|
|
80d4b88f5a | 2 years ago |
|
|
714b4f45b1 | 2 years ago |
|
|
6da902aede | 2 years ago |
|
|
cdffe03f9a | 2 years ago |
|
|
adeed03da8 | 2 years ago |
|
|
8e3dfdea30 | 2 years ago |
|
|
71fad5699e | 2 years ago |
|
|
a7d746a8e5 | 2 years ago |
|
|
c735211cd8 | 2 years ago |
|
|
369b77f00f | 2 years ago |
|
|
895c71dc91 | 2 years ago |
|
|
8b5d6ff2f3 | 2 years ago |
|
|
c1642cf09b | 2 years ago |
|
|
d82ef8af8f | 2 years ago |
|
|
08875e4415 | 2 years ago |
|
|
5765c78a1d | 2 years ago |
|
|
b9112bfb09 | 2 years ago |
|
|
05fbee9365 | 2 years ago |
|
|
1daef0d80f | 2 years ago |
|
|
06cc52bb7e | 2 years ago |
|
|
eac945e7b5 | 2 years ago |
|
|
a1b1a33a9b | 2 years ago |
|
|
02978a38ed | 2 years ago |
|
|
8cf358e17b | 2 years ago |
|
|
3ddcc35137 | 2 years ago |
|
|
4e7c958348 | 2 years ago |
|
|
237371a77f | 2 years ago |
|
|
f308e1ad49 | 2 years ago |
|
|
62f1fb87d1 | 2 years ago |
|
|
c5df85ce66 | 2 years ago |
|
|
848b2cddc8 | 2 years ago |
|
|
3d9d244b31 | 2 years ago |
|
|
ded9c38170 | 2 years ago |
|
|
af5426856e | 2 years ago |
|
|
470a184cac | 2 years ago |
|
|
1006097e32 | 2 years ago |
|
|
1431ff8b49 | 2 years ago |
|
|
d3a55a4dd3 | 2 years ago |
Binary file not shown.
|
After Width: | Height: | Size: 607 KiB |
Binary file not shown.
@ -0,0 +1,93 @@
|
||||
Copyright (c) 2020 - 2023, cormullion
|
||||
with Reserved Font Name JuliaMono.
|
||||
|
||||
This Font Software is licensed under the SIL Open Font License, Version 1.1.
|
||||
This license is copied below, and is also available with a FAQ at:
|
||||
http://scripts.sil.org/OFL
|
||||
|
||||
-----------------------------------------------------------
|
||||
SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007
|
||||
-----------------------------------------------------------
|
||||
|
||||
PREAMBLE
|
||||
The goals of the Open Font License (OFL) are to stimulate worldwide
|
||||
development of collaborative font projects, to support the font creation
|
||||
efforts of academic and linguistic communities, and to provide a free and
|
||||
open framework in which fonts may be shared and improved in partnership
|
||||
with others.
|
||||
|
||||
The OFL allows the licensed fonts to be used, studied, modified and
|
||||
redistributed freely as long as they are not sold by themselves. The
|
||||
fonts, including any derivative works, can be bundled, embedded,
|
||||
redistributed and/or sold with any software provided that any reserved
|
||||
names are not used by derivative works. The fonts and derivatives,
|
||||
however, cannot be released under any other type of license. The
|
||||
requirement for fonts to remain under this license does not apply
|
||||
to any document created using the fonts or their derivatives.
|
||||
|
||||
DEFINITIONS
|
||||
"Font Software" refers to the set of files released by the Copyright
|
||||
Holder(s) under this license and clearly marked as such. This may
|
||||
include source files, build scripts and documentation.
|
||||
|
||||
"Reserved Font Name" refers to any names specified as such after the
|
||||
copyright statement(s).
|
||||
|
||||
"Original Version" refers to the collection of Font Software components as
|
||||
distributed by the Copyright Holder(s).
|
||||
|
||||
"Modified Version" refers to any derivative made by adding to, deleting,
|
||||
or substituting -- in part or in whole -- any of the components of the
|
||||
Original Version, by changing formats or by porting the Font Software to a
|
||||
new environment.
|
||||
|
||||
"Author" refers to any designer, engineer, programmer, technical
|
||||
writer or other person who contributed to the Font Software.
|
||||
|
||||
PERMISSION & CONDITIONS
|
||||
Permission is hereby granted, free of charge, to any person obtaining
|
||||
a copy of the Font Software, to use, study, copy, merge, embed, modify,
|
||||
redistribute, and sell modified and unmodified copies of the Font
|
||||
Software, subject to the following conditions:
|
||||
|
||||
1) Neither the Font Software nor any of its individual components,
|
||||
in Original or Modified Versions, may be sold by itself.
|
||||
|
||||
2) Original or Modified Versions of the Font Software may be bundled,
|
||||
redistributed and/or sold with any software, provided that each copy
|
||||
contains the above copyright notice and this license. These can be
|
||||
included either as stand-alone text files, human-readable headers or
|
||||
in the appropriate machine-readable metadata fields within text or
|
||||
binary files as long as those fields can be easily viewed by the user.
|
||||
|
||||
3) No Modified Version of the Font Software may use the Reserved Font
|
||||
Name(s) unless explicit written permission is granted by the corresponding
|
||||
Copyright Holder. This restriction only applies to the primary font name as
|
||||
presented to the users.
|
||||
|
||||
4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font
|
||||
Software shall not be used to promote, endorse or advertise any
|
||||
Modified Version, except to acknowledge the contribution(s) of the
|
||||
Copyright Holder(s) and the Author(s) or with their explicit written
|
||||
permission.
|
||||
|
||||
5) The Font Software, modified or unmodified, in part or in whole,
|
||||
must be distributed entirely under this license, and must not be
|
||||
distributed under any other license. The requirement for fonts to
|
||||
remain under this license does not apply to any document created
|
||||
using the Font Software.
|
||||
|
||||
TERMINATION
|
||||
This license becomes null and void if any of the above conditions are
|
||||
not met.
|
||||
|
||||
DISCLAIMER
|
||||
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
|
||||
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
|
||||
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
|
||||
OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE
|
||||
COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
|
||||
INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
|
||||
DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
|
||||
FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
|
||||
OTHER DEALINGS IN THE FONT SOFTWARE.
|
||||
@ -0,0 +1,93 @@
|
||||
Copyright 2021 Google Inc. All Rights Reserved.
|
||||
|
||||
This Font Software is licensed under the SIL Open Font License, Version 1.1.
|
||||
This license is copied below, and is also available with a FAQ at:
|
||||
https://openfontlicense.org
|
||||
|
||||
|
||||
-----------------------------------------------------------
|
||||
SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007
|
||||
-----------------------------------------------------------
|
||||
|
||||
PREAMBLE
|
||||
The goals of the Open Font License (OFL) are to stimulate worldwide
|
||||
development of collaborative font projects, to support the font creation
|
||||
efforts of academic and linguistic communities, and to provide a free and
|
||||
open framework in which fonts may be shared and improved in partnership
|
||||
with others.
|
||||
|
||||
The OFL allows the licensed fonts to be used, studied, modified and
|
||||
redistributed freely as long as they are not sold by themselves. The
|
||||
fonts, including any derivative works, can be bundled, embedded,
|
||||
redistributed and/or sold with any software provided that any reserved
|
||||
names are not used by derivative works. The fonts and derivatives,
|
||||
however, cannot be released under any other type of license. The
|
||||
requirement for fonts to remain under this license does not apply
|
||||
to any document created using the fonts or their derivatives.
|
||||
|
||||
DEFINITIONS
|
||||
"Font Software" refers to the set of files released by the Copyright
|
||||
Holder(s) under this license and clearly marked as such. This may
|
||||
include source files, build scripts and documentation.
|
||||
|
||||
"Reserved Font Name" refers to any names specified as such after the
|
||||
copyright statement(s).
|
||||
|
||||
"Original Version" refers to the collection of Font Software components as
|
||||
distributed by the Copyright Holder(s).
|
||||
|
||||
"Modified Version" refers to any derivative made by adding to, deleting,
|
||||
or substituting -- in part or in whole -- any of the components of the
|
||||
Original Version, by changing formats or by porting the Font Software to a
|
||||
new environment.
|
||||
|
||||
"Author" refers to any designer, engineer, programmer, technical
|
||||
writer or other person who contributed to the Font Software.
|
||||
|
||||
PERMISSION & CONDITIONS
|
||||
Permission is hereby granted, free of charge, to any person obtaining
|
||||
a copy of the Font Software, to use, study, copy, merge, embed, modify,
|
||||
redistribute, and sell modified and unmodified copies of the Font
|
||||
Software, subject to the following conditions:
|
||||
|
||||
1) Neither the Font Software nor any of its individual components,
|
||||
in Original or Modified Versions, may be sold by itself.
|
||||
|
||||
2) Original or Modified Versions of the Font Software may be bundled,
|
||||
redistributed and/or sold with any software, provided that each copy
|
||||
contains the above copyright notice and this license. These can be
|
||||
included either as stand-alone text files, human-readable headers or
|
||||
in the appropriate machine-readable metadata fields within text or
|
||||
binary files as long as those fields can be easily viewed by the user.
|
||||
|
||||
3) No Modified Version of the Font Software may use the Reserved Font
|
||||
Name(s) unless explicit written permission is granted by the corresponding
|
||||
Copyright Holder. This restriction only applies to the primary font name as
|
||||
presented to the users.
|
||||
|
||||
4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font
|
||||
Software shall not be used to promote, endorse or advertise any
|
||||
Modified Version, except to acknowledge the contribution(s) of the
|
||||
Copyright Holder(s) and the Author(s) or with their explicit written
|
||||
permission.
|
||||
|
||||
5) The Font Software, modified or unmodified, in part or in whole,
|
||||
must be distributed entirely under this license, and must not be
|
||||
distributed under any other license. The requirement for fonts to
|
||||
remain under this license does not apply to any document created
|
||||
using the Font Software.
|
||||
|
||||
TERMINATION
|
||||
This license becomes null and void if any of the above conditions are
|
||||
not met.
|
||||
|
||||
DISCLAIMER
|
||||
THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
|
||||
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF
|
||||
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT
|
||||
OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE
|
||||
COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
|
||||
INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL
|
||||
DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
|
||||
FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM
|
||||
OTHER DEALINGS IN THE FONT SOFTWARE.
|
||||
@ -0,0 +1,202 @@
|
||||
|
||||
Apache License
|
||||
Version 2.0, January 2004
|
||||
http://www.apache.org/licenses/
|
||||
|
||||
TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
|
||||
|
||||
1. Definitions.
|
||||
|
||||
"License" shall mean the terms and conditions for use, reproduction,
|
||||
and distribution as defined by Sections 1 through 9 of this document.
|
||||
|
||||
"Licensor" shall mean the copyright owner or entity authorized by
|
||||
the copyright owner that is granting the License.
|
||||
|
||||
"Legal Entity" shall mean the union of the acting entity and all
|
||||
other entities that control, are controlled by, or are under common
|
||||
control with that entity. For the purposes of this definition,
|
||||
"control" means (i) the power, direct or indirect, to cause the
|
||||
direction or management of such entity, whether by contract or
|
||||
otherwise, or (ii) ownership of fifty percent (50%) or more of the
|
||||
outstanding shares, or (iii) beneficial ownership of such entity.
|
||||
|
||||
"You" (or "Your") shall mean an individual or Legal Entity
|
||||
exercising permissions granted by this License.
|
||||
|
||||
"Source" form shall mean the preferred form for making modifications,
|
||||
including but not limited to software source code, documentation
|
||||
source, and configuration files.
|
||||
|
||||
"Object" form shall mean any form resulting from mechanical
|
||||
transformation or translation of a Source form, including but
|
||||
not limited to compiled object code, generated documentation,
|
||||
and conversions to other media types.
|
||||
|
||||
"Work" shall mean the work of authorship, whether in Source or
|
||||
Object form, made available under the License, as indicated by a
|
||||
copyright notice that is included in or attached to the work
|
||||
(an example is provided in the Appendix below).
|
||||
|
||||
"Derivative Works" shall mean any work, whether in Source or Object
|
||||
form, that is based on (or derived from) the Work and for which the
|
||||
editorial revisions, annotations, elaborations, or other modifications
|
||||
represent, as a whole, an original work of authorship. For the purposes
|
||||
of this License, Derivative Works shall not include works that remain
|
||||
separable from, or merely link (or bind by name) to the interfaces of,
|
||||
the Work and Derivative Works thereof.
|
||||
|
||||
"Contribution" shall mean any work of authorship, including
|
||||
the original version of the Work and any modifications or additions
|
||||
to that Work or Derivative Works thereof, that is intentionally
|
||||
submitted to Licensor for inclusion in the Work by the copyright owner
|
||||
or by an individual or Legal Entity authorized to submit on behalf of
|
||||
the copyright owner. For the purposes of this definition, "submitted"
|
||||
means any form of electronic, verbal, or written communication sent
|
||||
to the Licensor or its representatives, including but not limited to
|
||||
communication on electronic mailing lists, source code control systems,
|
||||
and issue tracking systems that are managed by, or on behalf of, the
|
||||
Licensor for the purpose of discussing and improving the Work, but
|
||||
excluding communication that is conspicuously marked or otherwise
|
||||
designated in writing by the copyright owner as "Not a Contribution."
|
||||
|
||||
"Contributor" shall mean Licensor and any individual or Legal Entity
|
||||
on behalf of whom a Contribution has been received by Licensor and
|
||||
subsequently incorporated within the Work.
|
||||
|
||||
2. Grant of Copyright License. Subject to the terms and conditions of
|
||||
this License, each Contributor hereby grants to You a perpetual,
|
||||
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
|
||||
copyright license to reproduce, prepare Derivative Works of,
|
||||
publicly display, publicly perform, sublicense, and distribute the
|
||||
Work and such Derivative Works in Source or Object form.
|
||||
|
||||
3. Grant of Patent License. Subject to the terms and conditions of
|
||||
this License, each Contributor hereby grants to You a perpetual,
|
||||
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
|
||||
(except as stated in this section) patent license to make, have made,
|
||||
use, offer to sell, sell, import, and otherwise transfer the Work,
|
||||
where such license applies only to those patent claims licensable
|
||||
by such Contributor that are necessarily infringed by their
|
||||
Contribution(s) alone or by combination of their Contribution(s)
|
||||
with the Work to which such Contribution(s) was submitted. If You
|
||||
institute patent litigation against any entity (including a
|
||||
cross-claim or counterclaim in a lawsuit) alleging that the Work
|
||||
or a Contribution incorporated within the Work constitutes direct
|
||||
or contributory patent infringement, then any patent licenses
|
||||
granted to You under this License for that Work shall terminate
|
||||
as of the date such litigation is filed.
|
||||
|
||||
4. Redistribution. You may reproduce and distribute copies of the
|
||||
Work or Derivative Works thereof in any medium, with or without
|
||||
modifications, and in Source or Object form, provided that You
|
||||
meet the following conditions:
|
||||
|
||||
(a) You must give any other recipients of the Work or
|
||||
Derivative Works a copy of this License; and
|
||||
|
||||
(b) You must cause any modified files to carry prominent notices
|
||||
stating that You changed the files; and
|
||||
|
||||
(c) You must retain, in the Source form of any Derivative Works
|
||||
that You distribute, all copyright, patent, trademark, and
|
||||
attribution notices from the Source form of the Work,
|
||||
excluding those notices that do not pertain to any part of
|
||||
the Derivative Works; and
|
||||
|
||||
(d) If the Work includes a "NOTICE" text file as part of its
|
||||
distribution, then any Derivative Works that You distribute must
|
||||
include a readable copy of the attribution notices contained
|
||||
within such NOTICE file, excluding those notices that do not
|
||||
pertain to any part of the Derivative Works, in at least one
|
||||
of the following places: within a NOTICE text file distributed
|
||||
as part of the Derivative Works; within the Source form or
|
||||
documentation, if provided along with the Derivative Works; or,
|
||||
within a display generated by the Derivative Works, if and
|
||||
wherever such third-party notices normally appear. The contents
|
||||
of the NOTICE file are for informational purposes only and
|
||||
do not modify the License. You may add Your own attribution
|
||||
notices within Derivative Works that You distribute, alongside
|
||||
or as an addendum to the NOTICE text from the Work, provided
|
||||
that such additional attribution notices cannot be construed
|
||||
as modifying the License.
|
||||
|
||||
You may add Your own copyright statement to Your modifications and
|
||||
may provide additional or different license terms and conditions
|
||||
for use, reproduction, or distribution of Your modifications, or
|
||||
for any such Derivative Works as a whole, provided Your use,
|
||||
reproduction, and distribution of the Work otherwise complies with
|
||||
the conditions stated in this License.
|
||||
|
||||
5. Submission of Contributions. Unless You explicitly state otherwise,
|
||||
any Contribution intentionally submitted for inclusion in the Work
|
||||
by You to the Licensor shall be under the terms and conditions of
|
||||
this License, without any additional terms or conditions.
|
||||
Notwithstanding the above, nothing herein shall supersede or modify
|
||||
the terms of any separate license agreement you may have executed
|
||||
with Licensor regarding such Contributions.
|
||||
|
||||
6. Trademarks. This License does not grant permission to use the trade
|
||||
names, trademarks, service marks, or product names of the Licensor,
|
||||
except as required for reasonable and customary use in describing the
|
||||
origin of the Work and reproducing the content of the NOTICE file.
|
||||
|
||||
7. Disclaimer of Warranty. Unless required by applicable law or
|
||||
agreed to in writing, Licensor provides the Work (and each
|
||||
Contributor provides its Contributions) on an "AS IS" BASIS,
|
||||
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
|
||||
implied, including, without limitation, any warranties or conditions
|
||||
of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
|
||||
PARTICULAR PURPOSE. You are solely responsible for determining the
|
||||
appropriateness of using or redistributing the Work and assume any
|
||||
risks associated with Your exercise of permissions under this License.
|
||||
|
||||
8. Limitation of Liability. In no event and under no legal theory,
|
||||
whether in tort (including negligence), contract, or otherwise,
|
||||
unless required by applicable law (such as deliberate and grossly
|
||||
negligent acts) or agreed to in writing, shall any Contributor be
|
||||
liable to You for damages, including any direct, indirect, special,
|
||||
incidental, or consequential damages of any character arising as a
|
||||
result of this License or out of the use or inability to use the
|
||||
Work (including but not limited to damages for loss of goodwill,
|
||||
work stoppage, computer failure or malfunction, or any and all
|
||||
other commercial damages or losses), even if such Contributor
|
||||
has been advised of the possibility of such damages.
|
||||
|
||||
9. Accepting Warranty or Additional Liability. While redistributing
|
||||
the Work or Derivative Works thereof, You may choose to offer,
|
||||
and charge a fee for, acceptance of support, warranty, indemnity,
|
||||
or other liability obligations and/or rights consistent with this
|
||||
License. However, in accepting such obligations, You may act only
|
||||
on Your own behalf and on Your sole responsibility, not on behalf
|
||||
of any other Contributor, and only if You agree to indemnify,
|
||||
defend, and hold each Contributor harmless for any liability
|
||||
incurred by, or claims asserted against, such Contributor by reason
|
||||
of your accepting any such warranty or additional liability.
|
||||
|
||||
END OF TERMS AND CONDITIONS
|
||||
|
||||
APPENDIX: How to apply the Apache License to your work.
|
||||
|
||||
To apply the Apache License to your work, attach the following
|
||||
boilerplate notice, with the fields enclosed by brackets "[]"
|
||||
replaced with your own identifying information. (Don't include
|
||||
the brackets!) The text should be enclosed in the appropriate
|
||||
comment syntax for the file format. We also recommend that a
|
||||
file or class name and description of purpose be included on the
|
||||
same "printed page" as the copyright notice for easier
|
||||
identification within third-party archives.
|
||||
|
||||
Copyright [yyyy] [name of copyright owner]
|
||||
|
||||
Licensed under the Apache License, Version 2.0 (the "License");
|
||||
you may not use this file except in compliance with the License.
|
||||
You may obtain a copy of the License at
|
||||
|
||||
http://www.apache.org/licenses/LICENSE-2.0
|
||||
|
||||
Unless required by applicable law or agreed to in writing, software
|
||||
distributed under the License is distributed on an "AS IS" BASIS,
|
||||
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
See the License for the specific language governing permissions and
|
||||
limitations under the License.
|
||||
Binary file not shown.
Binary file not shown.
@ -0,0 +1,95 @@
|
||||
{
|
||||
"Intro": "",
|
||||
"Game Introduction": "",
|
||||
"World selection": "",
|
||||
"Start": "",
|
||||
"Inventory": "",
|
||||
"next level": "",
|
||||
"Next": "",
|
||||
"back to world selection": "",
|
||||
"Leave World": "",
|
||||
"previous level": "",
|
||||
"Previous": "",
|
||||
"Editor mode is enforced!": "",
|
||||
"Editor mode": "",
|
||||
"Typewriter mode": "",
|
||||
"information, Impressum, privacy policy": "",
|
||||
"Preferences": "",
|
||||
"Game Info & Credits": "",
|
||||
"Game Info": "",
|
||||
"Clear Progress": "",
|
||||
"Erase": "",
|
||||
"Download Progress": "",
|
||||
"Download": "",
|
||||
"Load Progress from JSON": "",
|
||||
"Upload": "",
|
||||
"Home": "",
|
||||
"back to games selection": "",
|
||||
"close inventory": "",
|
||||
"show inventory": "",
|
||||
"World": "",
|
||||
"Show more help!": "",
|
||||
"Goal": "",
|
||||
"Objects": "",
|
||||
"Assumptions": "",
|
||||
"Current Goal": "",
|
||||
"Further Goals": "",
|
||||
"No Goals": "",
|
||||
"Loading goal…": "",
|
||||
"Click somewhere in the Lean file to enable the infoview.": "",
|
||||
"Waiting for Lean server to start…": "",
|
||||
"Level completed! 🎉": "",
|
||||
"Level completed with warnings 🎭": "",
|
||||
"Failed command": "",
|
||||
"Retry proof from here": "",
|
||||
"Retry": "",
|
||||
"Active Goal": "",
|
||||
"Crashed! Go to editor mode and fix your proof! Last server response:": "",
|
||||
"Line": "",
|
||||
"Character": "",
|
||||
"Loading messages…": "",
|
||||
"Execute": "",
|
||||
"Tactics": "",
|
||||
"Definitions": "",
|
||||
"Theorems": "",
|
||||
"Not unlocked yet": "",
|
||||
"Not available in this level": "",
|
||||
"A repository of learning games for the proof assistant <1>Lean</1> <i>(Lean 4)</i> and its mathematical library <5>mathlib</5>": "",
|
||||
"No Games loaded. Use <1>http://localhost:3000/#/g/local/FOLDER</1> to open a game directly from a local folder.": "",
|
||||
"<p>As this server runs lean on our university machines, it has a limited capacity. Our current estimate is about 70 simultaneous games. We hope to address and test this limitation better in the future.</p><1>Most aspects of the games and the infrastructure are still in development. Feel free to file a <1>GitHub Issue</1> about any problems you experience!</1>": "",
|
||||
"<0>If you are considering writing your own game, you should use the <1>GameSkeleton Github Repo</1> as a template and read <3>How to Create a Game</3>.</0><1>You can directly load your games into the server and play it using the correct URL. The <1>instructions above</1> also explain the details for how to load your game to the server. We'd like to encourage you to contact us if you have any questions.</1><p>Featured games on this page are added manually. Please get in contact and we'll happily add yours.</p>": "",
|
||||
"This server has been developed as part of the project <1>ADAM : Anticipating the Digital Age of Mathematics</1> at Heinrich-Heine-Universität in Düsseldorf.": "",
|
||||
"view the Lean game server on Github": "",
|
||||
"Prerequisites": "",
|
||||
"Worlds": "",
|
||||
"Levels": "",
|
||||
"Language": "",
|
||||
"Lean Game Server": "",
|
||||
"Development notes": "",
|
||||
"Adding new games": "",
|
||||
"Funding": "",
|
||||
"Level": "",
|
||||
"Introduction": "",
|
||||
"<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>": "",
|
||||
"Delete Progress?": "",
|
||||
"Delete": "",
|
||||
"Download & Delete": "",
|
||||
"Cancel": "",
|
||||
"Mobile": "",
|
||||
"Auto": "",
|
||||
"Desktop": "",
|
||||
"Layout": "",
|
||||
"Always visible": "",
|
||||
"Save my settings (in the browser store)": "",
|
||||
"<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><1>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 <1>simp</1> in a level, you can use it henceforth in any level.</1><p>The options are:</p>": "",
|
||||
"Game Rules": "",
|
||||
"levels": "",
|
||||
"tactics": "",
|
||||
"regular": "",
|
||||
"relaxed": "",
|
||||
"none": "",
|
||||
"<p>Select a JSON file with the saved game progress to load your progress.</p><1><0>Warning:</0> This will delete your current game progress! Consider <2>downloading your current progress</2> first!</1>": "",
|
||||
"Upload Saved Progress": "",
|
||||
"Load selected file": "",
|
||||
"Rules": ""
|
||||
}
|
||||
@ -1,311 +0,0 @@
|
||||
/**
|
||||
* @file contains the navigation bars of the app.
|
||||
*/
|
||||
import * as React from 'react'
|
||||
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
|
||||
import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome,
|
||||
faArrowRight, faArrowLeft, faXmark, faBars, faCode,
|
||||
faCircleInfo, faTerminal, faGear } from '@fortawesome/free-solid-svg-icons'
|
||||
import { GameIdContext } from "../app"
|
||||
import { InputModeContext, PreferencesContext, WorldLevelIdContext } from "./infoview/context"
|
||||
import { GameInfo, useGetGameInfoQuery } from '../state/api'
|
||||
import { changedOpenedIntro, selectCompleted, selectDifficulty, selectProgress } from '../state/progress'
|
||||
import { useAppDispatch, useAppSelector } from '../hooks'
|
||||
import { Button } from './button'
|
||||
import { downloadProgress } from './popup/erase'
|
||||
import { useTranslation } from 'react-i18next'
|
||||
|
||||
/** navigation buttons for mobile welcome page to switch between intro/tree/inventory. */
|
||||
function MobileNavButtons({pageNumber, setPageNumber}:
|
||||
{ pageNumber: number,
|
||||
setPageNumber: any}) {
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
const { t } = useTranslation()
|
||||
const dispatch = useAppDispatch()
|
||||
|
||||
// if `prevText` or `prevIcon` is set, show a button to go back
|
||||
let prevText = {0: null, 1: t("Intro"), 2: null}[pageNumber]
|
||||
let prevIcon = {0: null, 1: null, 2: faBookOpen}[pageNumber]
|
||||
let prevTitle = {0: null, 1: t("Game Introduction"), 2: t("World selection")}[pageNumber]
|
||||
// if `nextText` or `nextIcon` is set, show a button to go forward
|
||||
let nextText = {0: t("Start"), 1: null, 2: null}[pageNumber]
|
||||
let nextIcon = {0: null, 1: faBook, 2: null}[pageNumber]
|
||||
let nextTitle = {0: t("World selection"), 1: t("Inventory"), 2: null}[pageNumber]
|
||||
|
||||
return <>
|
||||
{(prevText || prevIcon) &&
|
||||
<Button className="btn btn-inverted toggle-width" to={pageNumber == 0 ? "/" : ""}
|
||||
inverted="true" title={prevTitle}
|
||||
onClick={() => {pageNumber == 0 ? null : setPageNumber(pageNumber - 1)}}>
|
||||
{prevIcon && <FontAwesomeIcon icon={prevIcon} />}
|
||||
{prevText && `${prevText}`}
|
||||
</Button>
|
||||
}
|
||||
{(nextText || nextIcon) &&
|
||||
<Button className="btn btn-inverted toggle-width" to="" inverted="true"
|
||||
title={nextTitle} onClick={() => {
|
||||
console.log(`page number: ${pageNumber}`)
|
||||
setPageNumber(pageNumber+1);
|
||||
dispatch(changedOpenedIntro({game: gameId, openedIntro: true}))}}>
|
||||
{nextText && `${nextText}`}
|
||||
{nextIcon && <FontAwesomeIcon icon={nextIcon} />}
|
||||
</Button>
|
||||
}
|
||||
</>
|
||||
}
|
||||
|
||||
/** button to toggle dropdown menu. */
|
||||
export function MenuButton({navOpen, setNavOpen}) {
|
||||
return <Button to="" className="btn toggle-width" id="menu-btn" onClick={(ev) => {setNavOpen(!navOpen)}}>
|
||||
{navOpen ? <FontAwesomeIcon icon={faXmark} /> : <FontAwesomeIcon icon={faBars} />}
|
||||
</Button>
|
||||
}
|
||||
|
||||
/** button to go one level futher.
|
||||
* for the last level, this button turns into a button going back to the welcome page.
|
||||
*/
|
||||
function NextButton({worldSize, difficulty, completed, setNavOpen}) {
|
||||
const { t } = useTranslation()
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
const {worldId, levelId} = React.useContext(WorldLevelIdContext)
|
||||
return (levelId < worldSize ?
|
||||
<Button inverted="true"
|
||||
to={`/${gameId}/world/${worldId}/level/${levelId + 1}`} title={t("next level")}
|
||||
disabled={difficulty >= 2 && !(completed || levelId == 0)}
|
||||
onClick={() => setNavOpen(false)}>
|
||||
<FontAwesomeIcon icon={faArrowRight} /> {levelId ? t("Next") : t("Start")}
|
||||
</Button>
|
||||
:
|
||||
<Button to={`/${gameId}`} inverted="true" title={t("back to world selection")} id="home-btn">
|
||||
<FontAwesomeIcon icon={faHome} /> {t("Leave World")}
|
||||
</Button>
|
||||
)
|
||||
}
|
||||
|
||||
/** button to go one level back.
|
||||
* only renders if the current level id is > 0.
|
||||
*/
|
||||
function PreviousButton({setNavOpen}) {
|
||||
const { t } = useTranslation()
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
const {worldId, levelId} = React.useContext(WorldLevelIdContext)
|
||||
return (levelId > 0 && <>
|
||||
<Button disabled={levelId <= 0} inverted="true"
|
||||
to={`/${gameId}/world/${worldId}/level/${levelId - 1}`}
|
||||
title={t("previous level")}
|
||||
onClick={() => setNavOpen(false)}>
|
||||
<FontAwesomeIcon icon={faArrowLeft} /> {t("Previous")}
|
||||
</Button>
|
||||
</>)
|
||||
}
|
||||
|
||||
/** button to toggle between editor and typewriter */
|
||||
function InputModeButton({setNavOpen, isDropdown}) {
|
||||
const { t } = useTranslation()
|
||||
const {levelId} = React.useContext(WorldLevelIdContext)
|
||||
const {typewriterMode, setTypewriterMode, lockEditorMode} = React.useContext(InputModeContext)
|
||||
|
||||
/** toggle input mode if allowed */
|
||||
function toggleInputMode(ev: React.MouseEvent) {
|
||||
if (!lockEditorMode){
|
||||
setTypewriterMode(!typewriterMode)
|
||||
setNavOpen(false)
|
||||
}
|
||||
}
|
||||
|
||||
return <Button
|
||||
className={`btn btn-inverted ${isDropdown? '' : 'toggle-width'}`} disabled={levelId <= 0 || lockEditorMode}
|
||||
inverted="true" to=""
|
||||
onClick={(ev) => toggleInputMode(ev)}
|
||||
title={lockEditorMode ? t("Editor mode is enforced!") : typewriterMode ? t("Editor mode") : t("Typewriter mode")}>
|
||||
<FontAwesomeIcon icon={(typewriterMode && !lockEditorMode) ? faCode : faTerminal} />
|
||||
{isDropdown && ((typewriterMode && !lockEditorMode) ? <> {t("Editor mode")}</> : <> {t("Typewriter mode")}</>)}
|
||||
</Button>
|
||||
}
|
||||
|
||||
/** button to toggle iimpressum popup
|
||||
*
|
||||
* Note: Do not translate the word "Impressum"! German GDPR needs this.
|
||||
*/
|
||||
export function ImpressumButton({setNavOpen, toggleImpressum, isDropdown}) {
|
||||
const { t } = useTranslation()
|
||||
return <Button className="btn btn-inverted"
|
||||
title={t("information, Impressum, privacy policy")} inverted="true" to="" onClick={(ev) => {toggleImpressum(ev); setNavOpen(false)}}>
|
||||
<FontAwesomeIcon icon={faCircleInfo} />
|
||||
{isDropdown && <> Impressum</>}
|
||||
</Button>
|
||||
}
|
||||
|
||||
export function PreferencesButton({setNavOpen, togglePreferencesPopup}) {
|
||||
const { t } = useTranslation()
|
||||
return <Button title={t("Preferences")} inverted="true" to="" onClick={() => {togglePreferencesPopup(); setNavOpen(false)}}>
|
||||
<FontAwesomeIcon icon={faGear} /> {t("Preferences")}
|
||||
</Button>
|
||||
}
|
||||
|
||||
function GameInfoButton({setNavOpen, toggleInfo}) {
|
||||
const { t } = useTranslation()
|
||||
return <Button className="btn btn-inverted"
|
||||
title={t("Game Info & Credits")} inverted="true" to="" onClick={() => {toggleInfo(); setNavOpen(false)}}>
|
||||
<FontAwesomeIcon icon={faCircleInfo} /> {t("Game Info")}
|
||||
</Button>
|
||||
}
|
||||
|
||||
function EraseButton ({setNavOpen, toggleEraseMenu}) {
|
||||
const { t } = useTranslation()
|
||||
return <Button title={t("Clear Progress")} inverted="true" to="" onClick={() => {toggleEraseMenu(); setNavOpen(false)}}>
|
||||
<FontAwesomeIcon icon={faEraser} /> {t("Erase")}
|
||||
</Button>
|
||||
}
|
||||
|
||||
function DownloadButton ({setNavOpen, gameId, gameProgress}) {
|
||||
const { t } = useTranslation()
|
||||
return <Button title={t("Download Progress")} inverted="true" to="" onClick={(ev) => {downloadProgress(gameId, gameProgress, ev); setNavOpen(false)}}>
|
||||
<FontAwesomeIcon icon={faDownload} /> {t("Download")}
|
||||
</Button>
|
||||
}
|
||||
|
||||
function UploadButton ({setNavOpen, toggleUploadMenu}) {
|
||||
const { t } = useTranslation()
|
||||
return <Button title={t("Load Progress from JSON")} inverted="true" to="" onClick={() => {toggleUploadMenu(); setNavOpen(false)}}>
|
||||
<FontAwesomeIcon icon={faUpload} /> {t("Upload")}
|
||||
</Button>
|
||||
}
|
||||
|
||||
/** button to go back to welcome page */
|
||||
function HomeButton({isDropdown}) {
|
||||
const { t } = useTranslation()
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
return <Button to={`/${gameId}`} inverted="true" title={t("back to world selection")} id="home-btn">
|
||||
<FontAwesomeIcon icon={faHome} />
|
||||
{isDropdown && <> {t("Home")}</>}
|
||||
</Button>
|
||||
}
|
||||
|
||||
function LandingPageButton() {
|
||||
const { t } = useTranslation()
|
||||
return <Button inverted="false" title={t("back to games selection")} to="/">
|
||||
<FontAwesomeIcon icon={faArrowLeft} /> <FontAwesomeIcon icon={faGlobe} />
|
||||
</Button>
|
||||
}
|
||||
|
||||
/** button in mobile level to toggle inventory.
|
||||
* only displays a button if `setPageNumber` is set.
|
||||
*/
|
||||
function InventoryButton({pageNumber, setPageNumber}) {
|
||||
const { t } = useTranslation()
|
||||
return (setPageNumber &&
|
||||
<Button to="" className="btn btn-inverted toggle-width"
|
||||
title={pageNumber ? t("close inventory") : t("show inventory")}
|
||||
inverted="true" onClick={() => {setPageNumber(pageNumber ? 0 : 1)}}>
|
||||
<FontAwesomeIcon icon={pageNumber ? faBookOpen : faBook} />
|
||||
</Button>
|
||||
)
|
||||
}
|
||||
|
||||
/** the navigation bar on the welcome page */
|
||||
export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, toggleEraseMenu, toggleUploadMenu, toggleInfo, togglePreferencesPopup} : {
|
||||
pageNumber: number,
|
||||
setPageNumber: any,
|
||||
gameInfo: GameInfo,
|
||||
toggleImpressum: any,
|
||||
toggleEraseMenu: any,
|
||||
toggleUploadMenu: any,
|
||||
toggleInfo: any,
|
||||
togglePreferencesPopup: () => void;
|
||||
}) {
|
||||
const { t } = useTranslation()
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
const gameProgress = useAppSelector(selectProgress(gameId))
|
||||
const {mobile} = React.useContext(PreferencesContext)
|
||||
const [navOpen, setNavOpen] = React.useState(false)
|
||||
|
||||
return <div className="app-bar">
|
||||
<div className='app-bar-left'>
|
||||
<LandingPageButton />
|
||||
<span className="app-bar-title"></span>
|
||||
</div>
|
||||
<div>
|
||||
{!mobile && <span className="app-bar-title">{t(gameInfo?.title, {ns: gameId})}</span>}
|
||||
</div>
|
||||
<div className="nav-btns">
|
||||
{mobile && <MobileNavButtons pageNumber={pageNumber} setPageNumber={setPageNumber} />}
|
||||
<MenuButton navOpen={navOpen} setNavOpen={setNavOpen} />
|
||||
</div>
|
||||
<div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
|
||||
<GameInfoButton setNavOpen={setNavOpen} toggleInfo={toggleInfo}/>
|
||||
<EraseButton setNavOpen={setNavOpen} toggleEraseMenu={toggleEraseMenu}/>
|
||||
<DownloadButton setNavOpen={setNavOpen} gameId={gameId} gameProgress={gameProgress}/>
|
||||
<UploadButton setNavOpen={setNavOpen} toggleUploadMenu={toggleUploadMenu}/>
|
||||
<ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
|
||||
<PreferencesButton setNavOpen={setNavOpen} togglePreferencesPopup={togglePreferencesPopup}/>
|
||||
</div>
|
||||
</div>
|
||||
}
|
||||
|
||||
/** the navigation bar in a level */
|
||||
export function LevelAppBar({isLoading, levelTitle, toggleImpressum, toggleInfo, togglePreferencesPopup, pageNumber=undefined, setPageNumber=undefined} : {
|
||||
isLoading: boolean,
|
||||
levelTitle: string,
|
||||
toggleImpressum: any,
|
||||
toggleInfo: any,
|
||||
togglePreferencesPopup: any,
|
||||
pageNumber?: number,
|
||||
setPageNumber?: any,
|
||||
}) {
|
||||
const { t } = useTranslation()
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
const {worldId, levelId} = React.useContext(WorldLevelIdContext)
|
||||
const {mobile} = React.useContext(PreferencesContext)
|
||||
const [navOpen, setNavOpen] = React.useState(false)
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
|
||||
const difficulty = useAppSelector(selectDifficulty(gameId))
|
||||
|
||||
let worldTitle = gameInfo.data?.worlds.nodes[worldId].title
|
||||
|
||||
return <div className="app-bar" style={isLoading ? {display: "none"} : null} >
|
||||
{mobile ?
|
||||
<>
|
||||
{/* MOBILE VERSION */}
|
||||
<div>
|
||||
<span className="app-bar-title">{levelTitle}</span>
|
||||
</div>
|
||||
<div className="nav-btns">
|
||||
<InventoryButton pageNumber={pageNumber} setPageNumber={setPageNumber}/>
|
||||
<MenuButton navOpen={navOpen} setNavOpen={setNavOpen}/>
|
||||
</div>
|
||||
<div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
|
||||
<NextButton worldSize={gameInfo.data?.worldSize[worldId]} difficulty={difficulty} completed={completed} setNavOpen={setNavOpen} />
|
||||
<PreviousButton setNavOpen={setNavOpen} />
|
||||
<HomeButton isDropdown={true} />
|
||||
<InputModeButton setNavOpen={setNavOpen} isDropdown={true}/>
|
||||
<GameInfoButton setNavOpen={setNavOpen} toggleInfo={toggleInfo}/>
|
||||
<ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
|
||||
<PreferencesButton setNavOpen={setNavOpen} togglePreferencesPopup={togglePreferencesPopup}/>
|
||||
</div>
|
||||
</> :
|
||||
<>
|
||||
{/* DESKTOP VERSION */}
|
||||
<div className='app-bar-left'>
|
||||
<HomeButton isDropdown={false} />
|
||||
<span className="app-bar-title">{worldTitle && `${t("World")}: ${t(worldTitle, {ns: gameId})}`}</span>
|
||||
</div>
|
||||
<div>
|
||||
<span className="app-bar-title">{levelTitle}</span>
|
||||
</div>
|
||||
<div className="nav-btns">
|
||||
<PreviousButton setNavOpen={setNavOpen} />
|
||||
<NextButton worldSize={gameInfo.data?.worldSize[worldId]} difficulty={difficulty} completed={completed} setNavOpen={setNavOpen} />
|
||||
<InputModeButton setNavOpen={setNavOpen} isDropdown={false}/>
|
||||
<MenuButton navOpen={navOpen} setNavOpen={setNavOpen}/>
|
||||
</div>
|
||||
<div className={'menu dropdown' + (navOpen ? '' : ' hidden')}>
|
||||
<GameInfoButton setNavOpen={setNavOpen} toggleInfo={toggleInfo}/>
|
||||
<ImpressumButton setNavOpen={setNavOpen} toggleImpressum={toggleImpressum} isDropdown={true} />
|
||||
<PreferencesButton setNavOpen={setNavOpen} togglePreferencesPopup={togglePreferencesPopup}/>
|
||||
</div>
|
||||
</>
|
||||
}
|
||||
</div>
|
||||
}
|
||||
@ -1,15 +0,0 @@
|
||||
import * as React from 'react';
|
||||
import { Link, LinkProps } from "react-router-dom";
|
||||
|
||||
export interface ButtonProps extends LinkProps {
|
||||
disabled?: boolean
|
||||
inverted?: string // Apparently "inverted" in DOM cannot be `boolean` but must be `inverted`
|
||||
}
|
||||
|
||||
export function Button(props: ButtonProps) {
|
||||
if (props.disabled) {
|
||||
return <span className={`btn btn-disabled ${props.inverted === "true" ? 'btn-inverted' : ''}`} {...props}>{props.children}</span>
|
||||
} else {
|
||||
return <Link className={`btn ${props.inverted === "true" ? 'btn-inverted' : ''}`} {...props}>{props.children}</Link>
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,450 @@
|
||||
import * as React from 'react'
|
||||
import { useContext, useEffect, useRef, useState } from 'react'
|
||||
import { useSelector } from 'react-redux'
|
||||
import { useTranslation } from 'react-i18next'
|
||||
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
|
||||
import { faArrowRight } from '@fortawesome/free-solid-svg-icons'
|
||||
|
||||
import { changedReadIntro, selectCompleted, selectReadIntro } from '../state/progress'
|
||||
import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api'
|
||||
import { useAppDispatch, useAppSelector } from '../hooks'
|
||||
import { Button, Markdown } from './utils'
|
||||
import { ChatContext, GameIdContext, PageContext, PreferencesContext, ProofContext } from '../state/context'
|
||||
import { GameHint, InteractiveGoalsWithHints } from './infoview/rpc_api'
|
||||
// import { lastStepHasErrors } from './infoview/goals'
|
||||
// import { AllMessages } from '../../../node_modules/@leanprover/infoview/dist/infoview/messages'
|
||||
// import { LeanDiagnostic, RpcErrorCode, getInteractiveDiagnostics, InteractiveDiagnostic, TaggedText_stripTags } from '@leanprover/infoview-api'
|
||||
import { Location, DocumentUri, Diagnostic, DiagnosticSeverity, PublishDiagnosticsParams } from 'vscode-languageserver-protocol'
|
||||
// import { InteractiveMessage } from '../../../node_modules/lean4-infoview/src/infoview/traceExplorer'
|
||||
|
||||
import '../css/chat.css'
|
||||
import { faHome } from '@fortawesome/free-solid-svg-icons'
|
||||
|
||||
|
||||
/** Split a string by double newlines and filters out empty segments. */
|
||||
function splitIntro (intro : string) {
|
||||
return intro.split(/\n(\s*\n)+/).filter(t => t.trim())
|
||||
}
|
||||
|
||||
/** Helper to check if a step has any hidden hints. */
|
||||
function hasHiddenHints(step: InteractiveGoalsWithHints): boolean {
|
||||
return step?.goals[0]?.hints.some((hint) => hint.hidden)
|
||||
}
|
||||
|
||||
/** Button which only appears if the current step has hidden hints that are not shown yet. */
|
||||
export function MoreHelpButton({selected=null} : {selected?: number}) {
|
||||
|
||||
const { t } = useTranslation()
|
||||
|
||||
const { proof } = React.useContext(ProofContext)
|
||||
const { showHelp, setShowHelp } = React.useContext(ChatContext)
|
||||
|
||||
let k = 0
|
||||
// let k = proof?.steps.length ?
|
||||
// ((selected === null) ? (proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected)
|
||||
// : 0
|
||||
|
||||
const activateHiddenHints = (ev) => {
|
||||
// If the last step (`k`) has errors, we want the hidden hints from the
|
||||
// second-to-last step to be affected
|
||||
if (!(proof?.steps.length)) {return <></>}
|
||||
|
||||
// state must not be mutated, therefore we need to clone the set
|
||||
let tmp = new Set(showHelp)
|
||||
if (tmp.has(k)) {
|
||||
tmp.delete(k)
|
||||
} else {
|
||||
tmp.add(k)
|
||||
}
|
||||
setShowHelp(tmp)
|
||||
console.debug(`help: ${Array.from(tmp.values())}`)
|
||||
}
|
||||
|
||||
if (hasHiddenHints(proof?.steps[k]) && !showHelp.has(k)) {
|
||||
return <Button to="" onClick={activateHiddenHints}>
|
||||
{t("Show more help!")}
|
||||
</Button>
|
||||
}
|
||||
return <></>
|
||||
}
|
||||
|
||||
/** Placeholder that takes the same space as a button. */
|
||||
function ButtonPlaceholder() {
|
||||
return <div className='btn-placeholder'/>
|
||||
}
|
||||
|
||||
/** The buttons at the bottom of chat. */
|
||||
export function ChatButtons ({counter=undefined, setCounter=()=>{}, introMessages=[]} : {
|
||||
counter?: number
|
||||
setCounter?: React.Dispatch<React.SetStateAction<number>>
|
||||
introMessages?: GameHintWithStep[]
|
||||
}) {
|
||||
let { t } = useTranslation()
|
||||
|
||||
const { mobile } = useContext(PreferencesContext)
|
||||
const { gameId, worldId, levelId } = useContext(GameIdContext)
|
||||
const {setPage} = useContext(PageContext)
|
||||
const dispatch = useAppDispatch()
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
const { proof } = useContext(ProofContext)
|
||||
|
||||
const readIntro = useSelector(selectReadIntro(gameId, worldId))
|
||||
|
||||
return <div className="button-row">
|
||||
{!levelId && (readIntro || (counter >= introMessages.length) ?
|
||||
((worldId || mobile) &&
|
||||
<>
|
||||
<ButtonPlaceholder />
|
||||
<Button className="btn"
|
||||
title=""
|
||||
to={worldId ? `/${gameId}/world/${worldId}/level/1` : ''}
|
||||
onClick={() => {
|
||||
if (!worldId) {
|
||||
console.log('setting `readIntro` to true')
|
||||
setPage(1)
|
||||
}
|
||||
}} >
|
||||
Start <FontAwesomeIcon icon={faArrowRight}/>
|
||||
</Button>
|
||||
</>
|
||||
)
|
||||
:
|
||||
<>
|
||||
<Button className="btn"
|
||||
title=""
|
||||
to=""
|
||||
onClick={() => {
|
||||
if (counter + 1 >= introMessages.length) {
|
||||
dispatch(changedReadIntro({game: gameId, world: worldId, readIntro: true}))
|
||||
}
|
||||
setCounter(counter + 1)
|
||||
}} >
|
||||
{"Read"}
|
||||
</Button>
|
||||
<Button className="btn"
|
||||
title=""
|
||||
to=""
|
||||
onClick={() => {
|
||||
dispatch(changedReadIntro({game: gameId, world: worldId, readIntro: true}))
|
||||
setCounter(introMessages.length)
|
||||
}} >
|
||||
Skip all
|
||||
</Button>
|
||||
</>
|
||||
)}
|
||||
{ (worldId && levelId) ? <MoreHelpButton /> : <></> }
|
||||
{ (worldId && levelId && proof?.completed) ?
|
||||
(levelId == gameInfo.data?.worldSize[worldId] ?
|
||||
<Button className="btn"
|
||||
title=""
|
||||
to={`/${gameId}`} >
|
||||
<FontAwesomeIcon icon={faHome} /> {t("Home")}
|
||||
</Button> :
|
||||
<Button className="btn"
|
||||
title=""
|
||||
to={`/${gameId}/world/${worldId}/level/${levelId + 1}`} >
|
||||
{t("Next")} <FontAwesomeIcon icon={faArrowRight} />
|
||||
|
||||
</Button>
|
||||
) : <></> }
|
||||
</div>
|
||||
}
|
||||
|
||||
/** Insert the variable names in a hint. We do this client-side to prepare
|
||||
* for i18n in the future. i.e. one should be able translate the `rawText`
|
||||
* and have the variables substituted just before displaying.
|
||||
*/
|
||||
function getHintText(hint: GameHint): string {
|
||||
const {gameId} = React.useContext(GameIdContext)
|
||||
let { t } = useTranslation()
|
||||
if (hint.rawText) {
|
||||
// Replace the variable names used in the hint with the ones used by the player
|
||||
// variable names are marked like `«{g}»` inside the text.
|
||||
return t(hint.rawText, {ns: gameId}).replaceAll(/«\{(.*?)\}»/g, ((_, v) =>
|
||||
// `hint.varNames` contains tuples `[oldName, newName]`
|
||||
(hint.varNames.find(x => x[0] == v))[1]))
|
||||
} else {
|
||||
// hints created in the frontend do not have a `rawText`
|
||||
// TODO: `hint.text` could be removed in theory.
|
||||
return t(hint.text, {ns: gameId})
|
||||
}
|
||||
}
|
||||
|
||||
/** Hint kinds. Note that number 1-4 are matching the numbers from `DiagnosticSeverity`
|
||||
* from the vscode language server protocol.
|
||||
*/
|
||||
enum HintKind {
|
||||
Error = 1,
|
||||
Warning = 2,
|
||||
Information = 3,
|
||||
Hint = 4,
|
||||
GameHint = 5,
|
||||
Conclusion = 7,
|
||||
}
|
||||
|
||||
/** Bundling a hint with the proof-step it comes from. */
|
||||
type GameHintWithStep = {
|
||||
hint: GameHint
|
||||
kind: HintKind
|
||||
step?: number
|
||||
}
|
||||
|
||||
/** Filter hints to not show consequtive identical hints twice.
|
||||
* Hidden hints are not filtered.
|
||||
*/
|
||||
export function filterHints(hints: GameHint[], prevHints: GameHint[]): GameHint[] {
|
||||
if (!hints) {
|
||||
return []
|
||||
} else if (!prevHints) {
|
||||
return [...hints.filter((hint) => !hint.hidden), ...hints.filter((hint) => hint.hidden)]
|
||||
} else {
|
||||
return [...hints.filter((hint) => !hint.hidden &&
|
||||
(prevHints.find(x => (x.text == hint.text && x.hidden == hint.hidden)) === undefined)
|
||||
), ...hints.filter((hint) => hint.hidden)]
|
||||
}
|
||||
}
|
||||
|
||||
// TODO
|
||||
// function helper(step, proof, kind, typewriterMode, selectedStep) {
|
||||
// return (step == proof?.steps?.length - (lastStepHasErrors(proof) ? 2 : 1) ? ' recent' : '') +
|
||||
// (!(kind == HintKind.Conclusion) && step >= (typewriterMode ? proof?.steps?.length : selectedStep+1) ? ' deleted-hint' : '')
|
||||
// }
|
||||
|
||||
/** A hint as it is displayed in the chat. */
|
||||
export function Hint({hint, kind, step=null} : GameHintWithStep) {
|
||||
const { levelId } = useContext(GameIdContext)
|
||||
const { selectedStep, setSelectedStep } = useContext(ChatContext)
|
||||
|
||||
const { proof } = useContext(ProofContext)
|
||||
const { typewriterMode } = useContext(PageContext)
|
||||
|
||||
function toggleSelection () {
|
||||
if (!levelId) {return}
|
||||
|
||||
if (selectedStep !== null && selectedStep == step) {
|
||||
setSelectedStep(null)
|
||||
} else if (step < proof?.steps?.length) {
|
||||
setSelectedStep(step)
|
||||
}
|
||||
}
|
||||
|
||||
// "Deleted hints" are marked in grey. They are used two-fold:
|
||||
// In typewriter, deleting parts of the proof stores the removed hints as `deletedChat`
|
||||
// until the next command is submitted; in editor, moving the cursor through the proof will
|
||||
// render all hints
|
||||
return <div className={`message kind-${kind} step-${step}` +
|
||||
((selectedStep !== null && step == selectedStep) ? ' selected' : '') //+ helper(step, proof, kind, typewriterMode, selectedStep)
|
||||
} onClick={toggleSelection}>
|
||||
<Markdown>{getHintText(hint)}</Markdown>
|
||||
</div>
|
||||
}
|
||||
|
||||
/** A collection of hints. If the `counter` is defined, only the first elements will be
|
||||
* shown up to the value of the `counter`.
|
||||
*
|
||||
* Set `conclusion` to true to trigger different style and disable selecting/deleting.
|
||||
*/
|
||||
export function Hints({ hints, counter=undefined } : {
|
||||
hints: GameHintWithStep[],
|
||||
counter?: number
|
||||
}) {
|
||||
|
||||
const { showHelp } = useContext(ChatContext)
|
||||
|
||||
if (!hints) {
|
||||
return <></>
|
||||
}
|
||||
|
||||
// NOTE: This builds on the fact that `.slice(0, undefined)` returns the whole array!
|
||||
// TODO: Should not use index as key.
|
||||
return <>
|
||||
{ hints.slice(0, counter).map((hint, j) =>
|
||||
((!hint.hint.hidden || showHelp.has(hint.step)) &&
|
||||
<Hint key={`hint-${hint.step}-${j}`} hint={hint.hint} kind={hint.kind} step={hint.step} />
|
||||
)
|
||||
)}
|
||||
{/* { //showHelp.has(hint.step) &&
|
||||
hints.filter(hint => hint.hint.hidden).map((hint, j) =>
|
||||
<Hint
|
||||
key={`hidden-hint-${hint.step}-${j}`}
|
||||
hint={hint.hint}
|
||||
step={hint.step}
|
||||
conclusion={hint.conclusion} />
|
||||
)} */}
|
||||
</>
|
||||
}
|
||||
|
||||
/** the panel showing the game's introduction text */
|
||||
export function ChatPanel ({visible = true}) {
|
||||
|
||||
let { t } = useTranslation()
|
||||
|
||||
const { mobile } = useContext(PreferencesContext)
|
||||
const { gameId, worldId, levelId } = useContext(GameIdContext)
|
||||
|
||||
const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
|
||||
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
|
||||
|
||||
const [counter, setCounter] = useState(1)
|
||||
|
||||
const [introText, setIntroText] = useState<Array<GameHintWithStep>>([])
|
||||
const { chatRef, deletedChat, showHelp, selectedStep } = useContext(ChatContext)
|
||||
const { proof } = useContext(ProofContext)
|
||||
|
||||
const readIntro = useSelector(selectReadIntro(gameId, worldId))
|
||||
|
||||
useEffect(() => {
|
||||
setCounter(1)
|
||||
}, [gameId, worldId, levelId])
|
||||
|
||||
// load and display the correct intro text
|
||||
useEffect(() => {
|
||||
if (levelId > 0) {
|
||||
let introText = t(levelInfo.data?.introduction, {ns : gameId}).trim()
|
||||
let introHint: GameHintWithStep = {hint: {text: introText, hidden: false, rawText: introText }, kind: HintKind.GameHint, step: 0}
|
||||
|
||||
// playable level: show the level's intro
|
||||
if (levelInfo.data?.introduction) {
|
||||
setIntroText([introHint])
|
||||
// messages = messages.concat([introHint])
|
||||
}
|
||||
else {
|
||||
setIntroText([])
|
||||
}
|
||||
} else {
|
||||
if (worldId) {
|
||||
let introText = t(gameInfo.data?.worlds.nodes[worldId].introduction, {ns: gameId}).trim()
|
||||
let introHints: GameHintWithStep[] = splitIntro(introText).map( txt => ({hint: {text: txt, hidden: false, rawText: txt }, kind: HintKind.GameHint, step: 0}))
|
||||
|
||||
// Level 0: show the world's intro
|
||||
if (gameInfo.data?.worlds.nodes[worldId].introduction) {
|
||||
// messages = messages.concat(introHints)
|
||||
setIntroText(introHints)
|
||||
} else {
|
||||
setIntroText([])
|
||||
}
|
||||
} else {
|
||||
let introText = t(gameInfo.data?.introduction, {ns : gameId}).trim()
|
||||
let introHints: GameHintWithStep[] = splitIntro(introText).map( txt => ({hint: {text: txt, hidden: false, rawText: txt }, kind: HintKind.GameHint, step: 0}))
|
||||
|
||||
// world overview: show the game's intro
|
||||
if (gameInfo.data?.introduction) {
|
||||
// messages = messages.concat(introHints)
|
||||
setIntroText(introHints)
|
||||
} else {
|
||||
setIntroText([])
|
||||
}
|
||||
}
|
||||
}
|
||||
}, [gameInfo, levelInfo, gameId, worldId, levelId, proof])
|
||||
|
||||
// Scroll the chat
|
||||
useEffect(() => {
|
||||
if (levelId > 0) {
|
||||
|
||||
if (proof) {
|
||||
if (proof?.completed) {
|
||||
// proof currently completed: scroll down
|
||||
console.debug('scroll chat: down to conclusion')
|
||||
chatRef.current!.lastElementChild?.scrollIntoView({block: "center"})
|
||||
} else {
|
||||
// proof currently not completed: first message of last step
|
||||
let lastStep = proof?.steps.length //- (lastStepHasErrors(proof) ? 2 : 1)
|
||||
console.debug(`scroll chat: first message of step ${lastStep}`)
|
||||
chatRef.current?.getElementsByClassName(`step-${lastStep}`)[0]?.scrollIntoView({block: "center"})
|
||||
}
|
||||
} else {
|
||||
// no proof available: scroll to top.
|
||||
console.debug(`scroll chat: top`)
|
||||
chatRef.current!.scrollTo(0,0)
|
||||
}
|
||||
} else {
|
||||
// introduction: scroll to last message
|
||||
console.debug('scroll chat: down')
|
||||
chatRef.current!.lastElementChild?.scrollIntoView({block: "center"})
|
||||
}
|
||||
}, [counter, introText, gameId, worldId, levelId])
|
||||
|
||||
// Scroll down when new hidden hints are triggered
|
||||
useEffect(() => {
|
||||
if (levelId > 0) {
|
||||
let lastStep = proof?.steps.length //- (lastStepHasErrors(proof) ? 2 : 1)
|
||||
if (showHelp.has(lastStep)) {
|
||||
console.debug('scroll chat: down to hidden hints')
|
||||
// TODO: last element of hidden hints?
|
||||
chatRef.current!.lastElementChild?.scrollIntoView({block: "center"})
|
||||
}
|
||||
}
|
||||
}, [showHelp, gameId, worldId, levelId])
|
||||
|
||||
// Scroll to corresponding messages if selected step changes
|
||||
useEffect(() => {
|
||||
if (levelId > 0 && selectedStep !== null) {
|
||||
console.debug(`scroll chat: first message of selected step ${selectedStep}`)
|
||||
chatRef.current?.getElementsByClassName(`step-${selectedStep}`)[0]?.scrollIntoView({block: "center"})
|
||||
// Array.from(chatRef.current?.getElementsByClassName(`step-${selectedStep}`)).map((elem) => {
|
||||
// elem.scrollIntoView({block: "center"})
|
||||
// })
|
||||
}
|
||||
}, [selectedStep, gameId, worldId, levelId])
|
||||
|
||||
/** TODO: What's the magic here? Only needed if diags are displayed in chat. */
|
||||
function diagToString (diag) {
|
||||
// Hide "unsolved goals" messages
|
||||
let message;
|
||||
if ("append" in diag.message && "text" in diag.message.append[0] &&
|
||||
diag.message?.append[0].text === "unsolved goals") {
|
||||
message = diag.message.append[0]
|
||||
} else {
|
||||
message = diag.message
|
||||
}
|
||||
return message
|
||||
}
|
||||
|
||||
return <div className={`column chat-panel${visible ? '' : ' hidden'}`}>
|
||||
<div ref={chatRef} className="chat" >
|
||||
{ gameInfo.error &&
|
||||
<div className="message error">
|
||||
Could not find the game!
|
||||
</div>
|
||||
}
|
||||
<Hints hints={introText} counter={readIntro ? undefined : counter}/>
|
||||
{proof?.steps.map((step, i) => {
|
||||
let x = [].concat(
|
||||
filterHints(step.goals[0]?.hints, proof.steps[i-1]?.goals[0]?.hints).map(hint => ({hint: hint, kind: HintKind.GameHint, step: i})),
|
||||
// // TODO: Uncomment this if you want to see the diags in chat
|
||||
// step.diags.map(diag => ({hint: diagToString(diag), kind: diag.severity, step: i}))
|
||||
)
|
||||
|
||||
return <Hints key={`hints-step-${i}`} hints={x}/>
|
||||
})}
|
||||
|
||||
{/* <Hints hints={chatMessages}/> */}
|
||||
{/* {proof?.steps.map((step, i) =>
|
||||
<Hints hints={step.goals[0]?.hints.map(hint => ({hint: hint, step: i}))}/>
|
||||
)} */}
|
||||
{/* <Hints hints={proof?.steps[proof?.steps?.length - 1]?.goals[0].hints.map(hint => ({hint: hint, step: proof?.steps?.length - 1}))} /> */}
|
||||
|
||||
{ deletedChat &&
|
||||
<Hints hints={deletedChat.map(hint => ({hint: hint, kind: HintKind.GameHint, step: proof?.steps?.length}))} />
|
||||
}
|
||||
{ completed && levelInfo.data?.conclusion &&
|
||||
<Hints hints={[
|
||||
{hint: {text: t("Level completed! 🎉"), rawText: t("Level completed! 🎉"), hidden: false}, kind: HintKind.Conclusion, step: proof?.steps?.length},
|
||||
{hint: {text: levelInfo.data?.conclusion, rawText: levelInfo.data?.conclusion, hidden: false}, kind: HintKind.GameHint, step: proof?.steps?.length}
|
||||
]} />
|
||||
}
|
||||
|
||||
{/* {chatMessages.map(((t, i) =>
|
||||
t.trim() ?
|
||||
<Hint key={`intro-p-${i}`}
|
||||
hint={{text: t, hidden: false, rawText: t, varNames: []}}
|
||||
step={0} />
|
||||
: <></>
|
||||
))} */}
|
||||
</div>
|
||||
{ <ChatButtons counter={counter} setCounter={setCounter} introMessages={introText}/> }
|
||||
</div>
|
||||
}
|
||||
@ -0,0 +1,104 @@
|
||||
import * as React from 'react';
|
||||
import Split from 'react-split'
|
||||
import { useContext, useEffect, useRef, useState } from 'react'
|
||||
import { useTranslation } from "react-i18next"
|
||||
import { GameIdContext, MonacoEditorContext } from '../../state/context';
|
||||
import { useLoadLevelQuery } from '../../state/api';
|
||||
import { Markdown } from '../utils';
|
||||
import * as monaco from 'monaco-editor'
|
||||
import { LeanMonaco, LeanMonacoEditor, LeanMonacoOptions } from 'lean4monaco'
|
||||
|
||||
import '../../css/editor.css'
|
||||
import { useSelector } from 'react-redux';
|
||||
import { selectTypewriterMode } from '../../state/progress';
|
||||
import { TypewriterInterFace } from './Typewriter';
|
||||
|
||||
export function Editor() {
|
||||
let { t } = useTranslation()
|
||||
const {gameId, worldId, levelId } = useContext(GameIdContext)
|
||||
|
||||
const typewriterMode = useSelector(selectTypewriterMode(gameId))
|
||||
|
||||
const editorRef = useRef<HTMLDivElement>(null)
|
||||
const infoviewRef = useRef<HTMLDivElement>(null)
|
||||
const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor>()
|
||||
const [leanMonaco, setLeanMonaco] = useState<LeanMonaco>()
|
||||
const [code, setCode] = useState<string>('')
|
||||
|
||||
const [options, setOptions] = useState<LeanMonacoOptions>({
|
||||
// placeholder. gets set below
|
||||
websocket: {
|
||||
url: ''
|
||||
}
|
||||
})
|
||||
|
||||
// Update LeanMonaco options when preferences are loaded or change
|
||||
useEffect(() => {
|
||||
var socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") +
|
||||
window.location.host + `/websocket/${gameId}`
|
||||
console.log(`[LeanGame] socket url: ${socketUrl}`)
|
||||
var _options: LeanMonacoOptions = {
|
||||
websocket: {
|
||||
url: socketUrl,
|
||||
// @ts-ignore
|
||||
difficulty: 1,
|
||||
inventory: []
|
||||
},
|
||||
// Restrict monaco's extend (e.g. context menu) to the editor itself
|
||||
htmlElement: editorRef.current ?? undefined,
|
||||
vscode: {
|
||||
/* To add settings here, you can open your settings in VSCode (Ctrl+,), search
|
||||
* for the desired setting, select "Copy Setting as JSON" from the "More Actions"
|
||||
* menu next to the selected setting, and paste the copied string here.
|
||||
*/
|
||||
// "workbench.colorTheme": preferences.theme,
|
||||
"editor.tabSize": 2,
|
||||
// "editor.rulers": [100],
|
||||
"editor.lightbulb.enabled": "on",
|
||||
"editor.wordWrap": "on",
|
||||
"editor.wrappingStrategy": "advanced",
|
||||
"editor.semanticHighlighting.enabled": true,
|
||||
"editor.acceptSuggestionOnEnter": "off",
|
||||
"lean4.input.eagerReplacementEnabled": true,
|
||||
// "lean4.input.leader": preferences.abbreviationCharacter
|
||||
}
|
||||
}
|
||||
setOptions(_options)
|
||||
}, [editorRef])
|
||||
|
||||
// Setting up the editor and infoview
|
||||
useEffect(() => {
|
||||
console.debug('[LeanGame] Restarting Editor!')
|
||||
var _leanMonaco = new LeanMonaco()
|
||||
var leanMonacoEditor = new LeanMonacoEditor()
|
||||
|
||||
_leanMonaco.setInfoviewElement(infoviewRef.current!)
|
||||
;(async () => {
|
||||
await _leanMonaco.start(options)
|
||||
console.warn('gameId', gameId)
|
||||
await leanMonacoEditor.start(editorRef.current!, `/${worldId}/L_${levelId}.lean`, code)
|
||||
|
||||
setEditor(leanMonacoEditor.editor)
|
||||
setLeanMonaco(_leanMonaco)
|
||||
|
||||
// Keeping the `code` state up-to-date with the changes in the editor
|
||||
leanMonacoEditor.editor?.onDidChangeModelContent(() => {
|
||||
setCode(leanMonacoEditor.editor?.getModel()?.getValue()!)
|
||||
})
|
||||
})()
|
||||
return () => {
|
||||
leanMonacoEditor.dispose()
|
||||
_leanMonaco.dispose()
|
||||
}
|
||||
}, [options, infoviewRef, editorRef, gameId, worldId, levelId])
|
||||
|
||||
return <MonacoEditorContext.Provider value={editor}>
|
||||
<div className="editor-wrapper"><Split direction='vertical' minSize={200} sizes={[50, 50]}
|
||||
className={`editor-split ${typewriterMode ? 'hidden' : ''}`} >
|
||||
<div ref={editorRef} id="editor" />
|
||||
<div ref={infoviewRef} id="infoview" />
|
||||
</Split>
|
||||
{typewriterMode && <TypewriterInterFace />}
|
||||
</div>
|
||||
</MonacoEditorContext.Provider>
|
||||
}
|
||||
@ -0,0 +1,37 @@
|
||||
import * as React from 'react';
|
||||
import { useContext, useEffect, useRef, useState } from 'react'
|
||||
import { useTranslation } from "react-i18next"
|
||||
import { GameIdContext } from '../../state/context';
|
||||
import { useLoadLevelQuery } from '../../state/api';
|
||||
import { Markdown } from '../utils';
|
||||
|
||||
/** The mathematical formulation of the statement, supporting e.g. Latex
|
||||
* It takes three forms, depending on the precence of name and description:
|
||||
* - Theorem xyz: description
|
||||
* - Theorem xyz
|
||||
* - Exercises: description
|
||||
*
|
||||
* If `showLeanStatement` is true, it will additionally display the lean code.
|
||||
*/
|
||||
export function ExerciseStatement({ showLeanStatement = false }) {
|
||||
let { t } = useTranslation()
|
||||
const {gameId, worldId, levelId } = useContext(GameIdContext)
|
||||
const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
|
||||
|
||||
if (!(levelInfo.data?.descrText || levelInfo.data?.descrFormat)) { return <></> }
|
||||
return <>
|
||||
<div className="exercise-statement">
|
||||
{levelInfo.data?.descrText ?
|
||||
<Markdown>
|
||||
{(levelInfo.data?.displayName ? `**${t("Theorem")}** \`${levelInfo.data?.displayName}\`: ` : '') + t(levelInfo.data?.descrText, {ns: gameId})}
|
||||
</Markdown> : levelInfo.data?.displayName &&
|
||||
<Markdown>
|
||||
{`**${t("Theorem")}** \`${levelInfo.data?.displayName}\``}
|
||||
</Markdown>
|
||||
}
|
||||
{levelInfo.data?.descrFormat && showLeanStatement &&
|
||||
<p><code className="lean-code">{levelInfo.data?.descrFormat}</code></p>
|
||||
}
|
||||
</div>
|
||||
</>
|
||||
}
|
||||
@ -0,0 +1,443 @@
|
||||
import * as React from 'react'
|
||||
import { useContext } from 'react'
|
||||
import { useRef, useState, useEffect } from 'react'
|
||||
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
|
||||
import { faArrowRight, faHome, faWandMagicSparkles } from '@fortawesome/free-solid-svg-icons'
|
||||
import { DiagnosticSeverity, PublishDiagnosticsParams, DocumentUri } from 'vscode-languageserver-protocol';
|
||||
import { useTranslation } from 'react-i18next'
|
||||
import * as monaco from 'monaco-editor'
|
||||
import { ChatContext, GameIdContext, InputModeContext, MonacoEditorContext, PageContext, PreferencesContext, ProofContext } from '../../state/context';
|
||||
|
||||
import { RpcContext, WithRpcSessions, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
|
||||
import { useServerNotificationEffect } from '../../../../node_modules/lean4-infoview/src/infoview/util';
|
||||
|
||||
import '../../css/infoview.css'
|
||||
import { useGetGameInfoQuery } from '../../state/api'
|
||||
import { GameHint } from './Defs'
|
||||
import { MoreHelpButton, filterHints } from '../chat'
|
||||
import { isLastStepWithErrors, lastStepHasErrors, loadGoals } from '../infoview/goals'
|
||||
import { getInteractiveDiagsAt, hasInteractiveErrors } from '../infoview/typewriter'
|
||||
import { Errors } from '../infoview/messages'
|
||||
import { Button, Markdown } from '../utils'
|
||||
import { Command, GoalsTabs } from '../infoview/main'
|
||||
import { CircularProgress } from '@mui/material'
|
||||
|
||||
/** The input field */
|
||||
export function TypewriterInput({disabled}: {disabled?: boolean}) {
|
||||
let { t } = useTranslation()
|
||||
|
||||
/** Reference to the hidden multi-line editor */
|
||||
// const editor = React.useContext(MonacoEditorContext)
|
||||
// const model = editor.getModel()
|
||||
// const uri = model.uri.toString()
|
||||
|
||||
const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
|
||||
const [processing, setProcessing] = useState(false)
|
||||
|
||||
// const {typewriterInput, setTypewriterInput} = React.useContext(InputModeContext)
|
||||
|
||||
const inputRef = useRef()
|
||||
|
||||
// // The context storing all information about the current proof
|
||||
const {proof, setProof, interimDiags, setInterimDiags, setCrashed} = React.useContext(ProofContext)
|
||||
|
||||
// // state to store the last batch of deleted messages
|
||||
// const {setDeletedChat} = React.useContext(DeletedChatContext)
|
||||
|
||||
// const rpcSess = React.useContext(RpcContext)
|
||||
|
||||
// // Run the command
|
||||
// const runCommand = React.useCallback(() => {
|
||||
// if (processing) {return}
|
||||
|
||||
// // TODO: Desired logic is to only reset this after a new *error-free* command has been entered
|
||||
// setDeletedChat([])
|
||||
|
||||
// const pos = editor.getPosition()
|
||||
// if (typewriterInput) {
|
||||
// setProcessing(true)
|
||||
// editor.executeEdits("typewriter", [{
|
||||
// range: monaco.Selection.fromPositions(
|
||||
// pos,
|
||||
// editor.getModel().getFullModelRange().getEndPosition()
|
||||
// ),
|
||||
// text: typewriterInput.trim() + "\n",
|
||||
// forceMoveMarkers: false
|
||||
// }])
|
||||
// setTypewriterInput('')
|
||||
// // Load proof after executing edits
|
||||
// loadGoals(rpcSess, uri, setProof, setCrashed)
|
||||
// }
|
||||
|
||||
// editor.setPosition(pos)
|
||||
// }, [typewriterInput, editor])
|
||||
|
||||
// useEffect(() => {
|
||||
// if (oneLineEditor && oneLineEditor.getValue() !== typewriterInput) {
|
||||
// oneLineEditor.setValue(typewriterInput)
|
||||
// }
|
||||
// }, [typewriterInput])
|
||||
|
||||
// /* Load proof on start/switching to typewriter */
|
||||
// useEffect(() => {
|
||||
// loadGoals(rpcSess, uri, setProof, setCrashed)
|
||||
// }, [])
|
||||
|
||||
// /** If the last step has an error, add the command to the typewriter. */
|
||||
// useEffect(() => {
|
||||
// if (lastStepHasErrors(proof)) {
|
||||
// setTypewriterInput(proof?.steps[proof?.steps.length - 1].command)
|
||||
// }
|
||||
// }, [proof])
|
||||
|
||||
// // React when answer from the server comes back
|
||||
// useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
|
||||
// if (params.uri == uri) {
|
||||
// setProcessing(false)
|
||||
|
||||
// console.log('Received lean diagnostics')
|
||||
// console.log(params.diagnostics)
|
||||
// setInterimDiags(params.diagnostics)
|
||||
|
||||
// //loadGoals(rpcSess, uri, setProof)
|
||||
|
||||
// // TODO: loadAllGoals()
|
||||
// if (!hasErrors(params.diagnostics)) {
|
||||
// //setTypewriterInput("")
|
||||
// editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
|
||||
// }
|
||||
// } else {
|
||||
// // console.debug(`expected uri: ${uri}, got: ${params.uri}`)
|
||||
// // console.debug(params)
|
||||
// }
|
||||
// // TODO: This is the wrong place apparently. Where do wee need to load them?
|
||||
// // TODO: instead of loading all goals every time, we could only load the last one
|
||||
// // loadAllGoals()
|
||||
// }, [uri]);
|
||||
|
||||
// // // React when answer from the server comes back
|
||||
// // useServerNotificationEffect('$/game/publishDiagnostics', (params: GameDiagnosticsParams) => {
|
||||
// // console.log('Received game diagnostics')
|
||||
// // console.log(`diag. uri : ${params.uri}`)
|
||||
// // console.log(params.diagnostics)
|
||||
|
||||
// // }, [uri]);
|
||||
|
||||
|
||||
// useEffect(() => {
|
||||
// const myEditor = monaco.editor.create(inputRef.current!, {
|
||||
// value: typewriterInput,
|
||||
// language: "lean4cmd",
|
||||
// quickSuggestions: false,
|
||||
// lightbulb: {
|
||||
// enabled: true
|
||||
// },
|
||||
// unicodeHighlight: {
|
||||
// ambiguousCharacters: false,
|
||||
// },
|
||||
// automaticLayout: true,
|
||||
// minimap: {
|
||||
// enabled: false
|
||||
// },
|
||||
// lineNumbers: 'off',
|
||||
// tabSize: 2,
|
||||
// glyphMargin: false,
|
||||
// folding: false,
|
||||
// lineDecorationsWidth: 0,
|
||||
// lineNumbersMinChars: 0,
|
||||
// 'semanticHighlighting.enabled': true,
|
||||
// overviewRulerLanes: 0,
|
||||
// hideCursorInOverviewRuler: true,
|
||||
// scrollbar: {
|
||||
// vertical: 'hidden',
|
||||
// horizontalScrollbarSize: 3
|
||||
// },
|
||||
// overviewRulerBorder: false,
|
||||
// theme: 'vs-code-theme-converted',
|
||||
// contextmenu: false
|
||||
// })
|
||||
|
||||
// setOneLineEditor(myEditor)
|
||||
|
||||
// const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), myEditor.getModel(), myEditor)
|
||||
|
||||
// return () => {abbrevRewriter.dispose(); myEditor.dispose()}
|
||||
// }, [])
|
||||
|
||||
// useEffect(() => {
|
||||
// if (!oneLineEditor) return
|
||||
// // Ensure that our one-line editor can only have a single line
|
||||
// const l = oneLineEditor.getModel().onDidChangeContent((e) => {
|
||||
// const value = oneLineEditor.getValue()
|
||||
// setTypewriterInput(value)
|
||||
// const newValue = value.replace(/[\n\r]/g, '')
|
||||
// if (value != newValue) {
|
||||
// oneLineEditor.setValue(newValue)
|
||||
// }
|
||||
// })
|
||||
// return () => { l.dispose() }
|
||||
// }, [oneLineEditor, setTypewriterInput])
|
||||
|
||||
// useEffect(() => {
|
||||
// if (!oneLineEditor) return
|
||||
// // Run command when pressing enter
|
||||
// const l = oneLineEditor.onKeyUp((ev) => {
|
||||
// if (ev.code === "Enter") {
|
||||
// runCommand()
|
||||
// }
|
||||
// })
|
||||
// return () => { l.dispose() }
|
||||
// }, [oneLineEditor, runCommand])
|
||||
|
||||
// // BUG: Causes `file closed` error
|
||||
// //TODO: Intention is to run once when loading, does that work?
|
||||
// useEffect(() => {
|
||||
// console.debug(`time to update: ${uri} \n ${rpcSess}`)
|
||||
// console.debug(rpcSess)
|
||||
// // console.debug('LOAD ALL GOALS')
|
||||
// // TODO: loadAllGoals()
|
||||
// }, [rpcSess])
|
||||
|
||||
/** Process the entered command */
|
||||
const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
|
||||
// ev.preventDefault()
|
||||
// runCommand()
|
||||
}
|
||||
|
||||
// do not display if the proof is completed (with potential warnings still present)
|
||||
return <div className={`typewriter-cmd${proof?.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
|
||||
<form onSubmit={handleSubmit}>
|
||||
<div className="typewriter-input-wrapper">
|
||||
<div ref={inputRef} className="typewriter-input" />
|
||||
</div>
|
||||
<button type="submit" disabled={processing} className="btn btn-inverted">
|
||||
<FontAwesomeIcon icon={faWandMagicSparkles} /> {t("Execute")}
|
||||
</button>
|
||||
</form>
|
||||
</div>
|
||||
}
|
||||
|
||||
export function TypewriterInterFace() {
|
||||
let { t } = useTranslation()
|
||||
const {gameId, worldId, levelId} = useContext(GameIdContext)
|
||||
const editor = useContext(MonacoEditorContext)
|
||||
const model = editor.getModel()
|
||||
const uri = model.uri.toString()
|
||||
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
let image: string = gameInfo.data?.worlds.nodes[worldId].image
|
||||
|
||||
|
||||
const [disableInput, setDisableInput] = useState<boolean>(false)
|
||||
const [loadingProgress, setLoadingProgress] = useState<number>(0)
|
||||
const { selectedStep, setSelectedStep, setDeletedChat, showHelp, setShowHelp } = useContext(ChatContext)
|
||||
const {mobile} = useContext(PreferencesContext)
|
||||
const { proof, setProof, crashed, setCrashed, interimDiags } = useContext(ProofContext)
|
||||
const { setTypewriterInput } = useContext(PageContext)
|
||||
|
||||
const proofPanelRef = React.useRef<HTMLDivElement>(null)
|
||||
// const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
|
||||
// const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
|
||||
|
||||
const rpcSess = useRpcSessionAtPos({uri: uri, line: 0, character: 0})
|
||||
|
||||
/** Delete all proof lines starting from a given line.
|
||||
* Note that the first line (i.e. deleting everything) is `1`!
|
||||
*/
|
||||
function deleteProof(line: number) {
|
||||
return (ev) => {
|
||||
let deletedChat: Array<GameHint> = []
|
||||
proof?.steps.slice(line).map((step, i) => {
|
||||
let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
|
||||
|
||||
// Only add these hidden hints to the deletion stack which were visible
|
||||
deletedChat = [...deletedChat, ...filteredHints.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
|
||||
})
|
||||
setDeletedChat(deletedChat)
|
||||
|
||||
// delete showHelp for deleted steps
|
||||
setShowHelp(new Set(Array.from(showHelp).filter(i => i < line - 1)))
|
||||
|
||||
editor.executeEdits("typewriter", [{
|
||||
range: monaco.Selection.fromPositions(
|
||||
{ lineNumber: line, column: 1 },
|
||||
editor.getModel().getFullModelRange().getEndPosition()
|
||||
),
|
||||
text: '',
|
||||
forceMoveMarkers: false
|
||||
}])
|
||||
setSelectedStep(null)
|
||||
setTypewriterInput(proof?.steps[line].command)
|
||||
// Reload proof on deleting
|
||||
loadGoals(rpcSess, uri, setProof, setCrashed)
|
||||
ev.stopPropagation()
|
||||
}
|
||||
}
|
||||
|
||||
function toggleSelectStep(line: number) {
|
||||
return (ev) => {
|
||||
if (mobile) {return}
|
||||
if (selectedStep == line) {
|
||||
setSelectedStep(null)
|
||||
console.debug(`unselected step`)
|
||||
} else {
|
||||
setSelectedStep(line)
|
||||
console.debug(`step ${line} selected`)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Scroll to the end of the proof if it is updated.
|
||||
React.useEffect(() => {
|
||||
if (proof?.steps.length > 1) {
|
||||
proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
|
||||
} else {
|
||||
proofPanelRef.current?.scrollTo(0,0)
|
||||
}
|
||||
// also reenable the commandline when the proof changes
|
||||
|
||||
// BUG: If selecting 2nd goal on a intermediate proofstep and then delete proof to there,
|
||||
// the commandline is not displaying disabled even though it should.
|
||||
setDisableInput(false)
|
||||
}, [proof])
|
||||
|
||||
// Scroll to element if selection changes
|
||||
React.useEffect(() => {
|
||||
if (typeof selectedStep !== 'undefined') {
|
||||
Array.from(proofPanelRef.current?.getElementsByClassName(`step-${selectedStep}`)).map((elem) => {
|
||||
elem.scrollIntoView({ block: "center" })
|
||||
})
|
||||
}
|
||||
}, [selectedStep])
|
||||
|
||||
// TODO: superfluous, can be replaced with `withErr` from above
|
||||
let lastStepErrors = proof?.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof?.steps.length)) : false
|
||||
|
||||
|
||||
useServerNotificationEffect("$/game/loading", (params : any) => {
|
||||
if (params.kind == "loadConstants") {
|
||||
setLoadingProgress(params.counter/100*50)
|
||||
} else if (params.kind == "finalizeExtensions") {
|
||||
setLoadingProgress(50 + params.counter/150*50)
|
||||
} else {
|
||||
console.error(`Unknown loading kind: ${params.kind}`)
|
||||
}
|
||||
})
|
||||
|
||||
return <div className="typewriter-interface">
|
||||
<RpcContext.Provider value={rpcSess}>
|
||||
<div className="content">
|
||||
{/* <div className='world-image-container empty'>
|
||||
{image &&
|
||||
<img className="contain" src={path.join("data", gameId, image)} alt="" />
|
||||
}
|
||||
|
||||
</div> */}
|
||||
{/* <div className="tmp-pusher">
|
||||
<div className="world-image-container empty">
|
||||
|
||||
</div>
|
||||
</div> */}
|
||||
<div className='proof' ref={proofPanelRef}>
|
||||
{/* <ExerciseStatement /> */}
|
||||
{crashed ? <div>
|
||||
<p className="crashed_message">{t("Crashed! Go to editor mode and fix your proof! Last server response:")}</p>
|
||||
{interimDiags.map(diag => {
|
||||
const severityClass = diag.severity ? {
|
||||
[DiagnosticSeverity.Error]: 'error',
|
||||
[DiagnosticSeverity.Warning]: 'warning',
|
||||
[DiagnosticSeverity.Information]: 'information',
|
||||
[DiagnosticSeverity.Hint]: 'hint',
|
||||
}[diag.severity] : '';
|
||||
|
||||
return <div key={diag.message} >
|
||||
<div className={`${severityClass} ml1 message`}>
|
||||
<p className="mv2">{t("Line")} {diag.range.start.line}, {t("Character")} {diag.range.start.character}</p>
|
||||
<pre className="font-code pre-wrap">
|
||||
{diag.message}as React
|
||||
</pre>
|
||||
</div>
|
||||
</div>
|
||||
})}
|
||||
|
||||
</div> : proof?.steps.length ?
|
||||
<>
|
||||
{proof?.steps.map((step, i) => {
|
||||
let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
|
||||
|
||||
// if (i == proof?.steps.length - 1 && hasInteractiveErrors(step.diags)) {
|
||||
// // if the last command contains an error, we only display the errors but not the
|
||||
// // entered command as it is still present in the command line.
|
||||
// // TODO: Should not use index as key.
|
||||
// return <div key={`proof-step-${i}`} className={`step step-${i}`}>
|
||||
// <Errors errors={step.diags} typewriterMode={true} />
|
||||
// </div>
|
||||
// } else {
|
||||
return <div key={`proof-step-${i}`} className={`step step-${i}` + (selectedStep == i ? ' selected' : '')}>
|
||||
{i > 0 && <>
|
||||
<Command proof={proof} i={i} deleteProof={deleteProof(i)} />
|
||||
<Errors errors={step.diags} typewriterMode={true} />
|
||||
</>}
|
||||
{/* {mobile && i == 0 && props.data?.introduction &&
|
||||
<div className={`message information step-0${selectedStep === 0 ? ' selected' : ''}`} onClick={toggleSelectStep(0)}>
|
||||
<Markdown>{props.data?.introduction}</Markdown>
|
||||
</div>
|
||||
}
|
||||
{mobile &&
|
||||
<Hints key={`hints-${i}`}
|
||||
hints={filteredHints.map(hint => ({hint: hint, step: i}))} />
|
||||
} */}
|
||||
{/* <GoalsTabs proofStep={step} last={i == proof?.steps.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof?.steps.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/> */}
|
||||
{!(isLastStepWithErrors(proof, i)) &&
|
||||
<GoalsTabs goals={step.goals} last={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) ? (n) => setDisableInput(n > 0) : (n) => {}}/>
|
||||
}
|
||||
{mobile && i == proof?.steps.length - 1 &&
|
||||
<MoreHelpButton />
|
||||
}
|
||||
|
||||
{/* Show a message that there are no goals left */}
|
||||
{/* {!step.goals.length && (
|
||||
<div className="message information">
|
||||
{proof?.completed ?
|
||||
<p>Level completed! 🎉</p> :
|
||||
<p>
|
||||
<b>no goals left</b><br />
|
||||
<i>This probably means you solved the level with warnings or Lean encountered a parsing error.</i>
|
||||
</p>
|
||||
}
|
||||
</div>
|
||||
)} */}
|
||||
</div>
|
||||
}
|
||||
//}
|
||||
)}
|
||||
{proof?.diagnostics.length > 0 &&
|
||||
<div key={`proof-step-remaining`} className="step step-remaining">
|
||||
<Errors errors={proof?.diagnostics} typewriterMode={true} />
|
||||
</div>
|
||||
}
|
||||
{mobile && proof?.completed &&
|
||||
<div className="button-row mobile">
|
||||
{/* {props.level >= props.worldSize ?
|
||||
<Button to={`/${gameId}`}>
|
||||
<FontAwesomeIcon icon={faHome} /> {t("Home")}
|
||||
</Button>
|
||||
:
|
||||
<Button to={`/${gameId}/world/${props.world}/level/${props.level + 1}`}>
|
||||
Next <FontAwesomeIcon icon={faArrowRight} />
|
||||
</Button>
|
||||
} */}
|
||||
</div>
|
||||
}
|
||||
</> : <CircularProgress variant="determinate" value={100*(1 - 1.024 ** (- loadingProgress))} />
|
||||
// note: since we don't know the total number of files,
|
||||
// we use a function which strictly monotonely increases towards `100` as `x → ∞`
|
||||
// The base is chosen at random s.t. we get roughly 91% for `x = 100`.
|
||||
}
|
||||
</div>
|
||||
</div>
|
||||
{/* <Typewriter disabled={disableInput || !proof?.steps.length}/> */}
|
||||
<TypewriterInput />
|
||||
</RpcContext.Provider>
|
||||
</div>
|
||||
}
|
||||
@ -1,17 +1,24 @@
|
||||
import * as React from 'react'
|
||||
import { useRouteError } from "react-router-dom";
|
||||
import '../css/error_page.css'
|
||||
|
||||
/** The fallback error page */
|
||||
export default function ErrorPage() {
|
||||
const error: any = useRouteError();
|
||||
console.error(error);
|
||||
const error: any = useRouteError()
|
||||
console.error(error)
|
||||
|
||||
return (
|
||||
<div id="error-page">
|
||||
<div className="error-message">
|
||||
<h1>Oops!</h1>
|
||||
<p>Sorry, an unexpected error has occurred.</p>
|
||||
<p>
|
||||
<i>{error.statusText || error.message}</i>
|
||||
</p>
|
||||
<p>Something unexpected happened:</p>
|
||||
<p><code>({error.status}) {error.statusText || error.message}<br/>{error.data}</code></p>
|
||||
<p>Please create an issue at the <a href="https://github.com/leanprover-community/lean4game/issues" target="_blank">lean4game repo</a>.</p>
|
||||
<div className="thought-bubble" />
|
||||
<div className="thought-bubble" />
|
||||
<div className="thought-bubble" />
|
||||
<div className="thought-bubble" />
|
||||
</div>
|
||||
);
|
||||
</div>
|
||||
)
|
||||
}
|
||||
|
||||
@ -0,0 +1,14 @@
|
||||
import * as React from 'react'
|
||||
import ReactCountryFlag from 'react-country-flag'
|
||||
import lean4gameConfig from '../config.json'
|
||||
|
||||
/** Displays either a flag or the language-code, depending on the settings.
|
||||
* The argument `iso` is an ISO-language code.
|
||||
*/
|
||||
export const Flag : React.FC<{ iso: string, showTitle?: boolean}> = ({iso, showTitle=false}) => {
|
||||
let lang = lean4gameConfig.newLanguages[iso]
|
||||
if (lean4gameConfig.useFlags && lang) {
|
||||
return <ReactCountryFlag countryCode={lang.flag} title={showTitle ? lang.name : null} />
|
||||
}
|
||||
return <span>{iso}</span>
|
||||
}
|
||||
@ -0,0 +1,112 @@
|
||||
import * as React from 'react'
|
||||
import { useContext, useEffect, useRef, useState } from 'react'
|
||||
import Split from 'react-split'
|
||||
|
||||
import { useAppDispatch, useAppSelector } from '../hooks'
|
||||
import { changeTypewriterMode, selectCode, selectSelections, selectTypewriterMode } from '../state/progress'
|
||||
import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api'
|
||||
import { ChatContext, GameIdContext, PageContext, PreferencesContext, ProofContext } from '../state/context'
|
||||
import { InventoryPanel } from './inventory'
|
||||
import { WorldTreePanel } from './world_tree'
|
||||
|
||||
import i18next from 'i18next'
|
||||
import { ChatPanel } from './chat'
|
||||
import { NewLevel } from './level'
|
||||
import { GameHint, ProofState } from './editor/Defs'
|
||||
import { useSelector } from 'react-redux'
|
||||
import { Diagnostic } from 'vscode-languageserver-types'
|
||||
|
||||
import '../css/game.css'
|
||||
import '../css/welcome.css'
|
||||
import '../css/level.css'
|
||||
|
||||
/** main page of the game showing among others the tree of worlds/levels */
|
||||
function Game() {
|
||||
|
||||
const dispatch = useAppDispatch()
|
||||
const { gameId, worldId, levelId } = React.useContext(GameIdContext)
|
||||
|
||||
// Load the namespace of the game
|
||||
i18next.loadNamespaces(gameId)
|
||||
|
||||
const {mobile} = useContext(PreferencesContext)
|
||||
const {isSavePreferences, language, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext)
|
||||
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
|
||||
const inventory = useLoadInventoryOverviewQuery({game: gameId})
|
||||
|
||||
const {page, setPage} = useContext(PageContext)
|
||||
|
||||
const chatRef = useRef<HTMLDivElement>(null)
|
||||
// When deleting the proof, we want to keep to old messages around until
|
||||
// a new proof has been entered. e.g. to consult messages coming from dead ends
|
||||
const [deletedChat, setDeletedChat] = useState<Array<GameHint>>([])
|
||||
// A set of row numbers where help is displayed
|
||||
const [showHelp, setShowHelp] = useState<Set<number>>(new Set())
|
||||
// Select and highlight proof steps and corresponding hints
|
||||
// TODO: with the new design, there is no difference between the introduction and
|
||||
// a hint at the beginning of the proof...
|
||||
const [selectedStep, setSelectedStep] = useState<number>(null)
|
||||
|
||||
// The state variables for the `ProofContext`
|
||||
const [proof, setProof] = useState<ProofState>({steps: [], diagnostics: [], completed: false, completedWithWarnings: false})
|
||||
const [interimDiags, setInterimDiags] = useState<Array<Diagnostic>>([])
|
||||
const [isCrashed, setIsCrashed] = useState<Boolean>(false)
|
||||
|
||||
const typewriterMode = useSelector(selectTypewriterMode(gameId))
|
||||
const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
|
||||
|
||||
const initialCode = useAppSelector(selectCode(gameId, worldId, levelId))
|
||||
const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId))
|
||||
|
||||
// set the window title
|
||||
useEffect(() => {
|
||||
if (gameInfo.data?.title) {
|
||||
window.document.title = gameInfo.data.title
|
||||
}
|
||||
}, [gameInfo.data?.title])
|
||||
|
||||
// Delete the current proof on changing level
|
||||
useEffect(() => {
|
||||
setProof(null)
|
||||
setSelectedStep(null)
|
||||
setDeletedChat([])
|
||||
setShowHelp(new Set())
|
||||
}, [gameId, worldId, levelId])
|
||||
|
||||
return <ChatContext.Provider value={{selectedStep, setSelectedStep, deletedChat, setDeletedChat, showHelp, setShowHelp, chatRef}}>
|
||||
<ProofContext.Provider value={{proof, setProof, interimDiags, setInterimDiags, crashed: isCrashed, setCrashed: setIsCrashed}}>
|
||||
{ mobile ?
|
||||
<div className="app-content mobile">
|
||||
{<>
|
||||
<ChatPanel visible={worldId ? (levelId == 0 && page == 1) :(page == 0)} />
|
||||
{ worldId ?
|
||||
<NewLevel visible={page == 1} /> :
|
||||
<WorldTreePanel visible={page == 1} />
|
||||
}
|
||||
<InventoryPanel visible={page == 2} />
|
||||
</>
|
||||
}
|
||||
</div>
|
||||
:
|
||||
<Split className="app-content" minSize={0} snapOffset={200} sizes={[25, 50, 25]}>
|
||||
<ChatPanel />
|
||||
<div className="column">
|
||||
{/* Note: apparently without this `div` the split panel bugs out. */}
|
||||
{worldId ?
|
||||
<NewLevel />
|
||||
: <WorldTreePanel /> }
|
||||
</div>
|
||||
<InventoryPanel />
|
||||
</Split>
|
||||
}
|
||||
</ProofContext.Provider>
|
||||
</ChatContext.Provider>
|
||||
|
||||
}
|
||||
|
||||
export default Game
|
||||
function useLevelEditor(codeviewRef: React.MutableRefObject<HTMLDivElement>, initialCode: any, initialSelections: any, onDidChangeContent: any, onDidChangeSelection: any): { editor: any; infoProvider: any; editorConnection: any } {
|
||||
throw new Error('Function not implemented.')
|
||||
}
|
||||
@ -1,125 +0,0 @@
|
||||
import { GameHint, InteractiveGoalsWithHints, ProofState } from "./infoview/rpc_api";
|
||||
import * as React from 'react';
|
||||
import Markdown from './markdown';
|
||||
import { DeletedChatContext, ProofContext } from "./infoview/context";
|
||||
import { lastStepHasErrors } from "./infoview/goals";
|
||||
import { Button } from "./button";
|
||||
import { useTranslation } from "react-i18next";
|
||||
import { GameIdContext } from "../app";
|
||||
|
||||
/** Plug-in the variable names in a hint. We do this client-side to prepare
|
||||
* for i18n in the future. i.e. one should be able translate the `rawText`
|
||||
* and have the variables substituted just before displaying.
|
||||
*/
|
||||
function getHintText(hint: GameHint): string {
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
let { t } = useTranslation()
|
||||
if (hint.rawText) {
|
||||
// Replace the variable names used in the hint with the ones used by the player
|
||||
// variable names are marked like `«{g}»` inside the text.
|
||||
return t(hint.rawText, {ns: gameId}).replaceAll(/«\{(.*?)\}»/g, ((_, v) =>
|
||||
// `hint.varNames` contains tuples `[oldName, newName]`
|
||||
(hint.varNames.find(x => x[0] == v))[1]))
|
||||
} else {
|
||||
// hints created in the frontend do not have a `rawText`
|
||||
// TODO: `hint.text` could be removed in theory.
|
||||
return t(hint.text, {ns: gameId})
|
||||
}
|
||||
}
|
||||
|
||||
export function Hint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
|
||||
return <div className={`message information step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
|
||||
<Markdown>{getHintText(hint)}</Markdown>
|
||||
</div>
|
||||
}
|
||||
|
||||
export function HiddenHint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
|
||||
return <div className={`message warning step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
|
||||
<Markdown>{getHintText(hint)}</Markdown>
|
||||
</div>
|
||||
}
|
||||
|
||||
export function Hints({hints, showHidden, step, selected, toggleSelection, lastLevel} : {hints: GameHint[], showHidden: boolean, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
|
||||
if (!hints) {return <></>}
|
||||
const openHints = hints.filter(hint => !hint.hidden)
|
||||
const hiddenHints = hints.filter(hint => hint.hidden)
|
||||
|
||||
// TODO: Should not use index as key.
|
||||
return <>
|
||||
{openHints.map((hint, j) => <Hint key={`hint-${step}-${j}`} hint={hint} step={step} selected={selected} toggleSelection={toggleSelection} lastLevel={lastLevel} />)}
|
||||
{showHidden && hiddenHints.map((hint, j) => <HiddenHint key={`hidden-hint-${step}-${j}`} hint={hint} step={step} selected={selected} toggleSelection={toggleSelection} lastLevel={lastLevel} />)}
|
||||
</>
|
||||
}
|
||||
|
||||
export function DeletedHint({hint} : {hint: GameHint}) {
|
||||
return <div className="message information deleted-hint">
|
||||
<Markdown>{getHintText(hint)}</Markdown>
|
||||
</div>
|
||||
}
|
||||
|
||||
export function DeletedHints({hints} : {hints: GameHint[]}) {
|
||||
|
||||
const openHints = hints.filter(hint => !hint.hidden)
|
||||
const hiddenHints = hints.filter(hint => hint.hidden)
|
||||
|
||||
// TODO: Should not use index as key.
|
||||
return <>
|
||||
{openHints.map((hint, i) => <DeletedHint key={`deleted-hint-${i}`} hint={hint} />)}
|
||||
{hiddenHints.map((hint, i) => <DeletedHint key={`deleted-hidden-hint-${i}`} hint={hint}/>)}
|
||||
</>
|
||||
}
|
||||
|
||||
/** Filter hints to not show consequtive identical hints twice.
|
||||
* Hidden hints are not filtered.
|
||||
*/
|
||||
export function filterHints(hints: GameHint[], prevHints: GameHint[]): GameHint[] {
|
||||
if (!hints) {
|
||||
return []}
|
||||
else if (!prevHints) {
|
||||
return hints }
|
||||
else {
|
||||
return hints.filter((hint) => hint.hidden ||
|
||||
(prevHints.find(x => (x.text == hint.text && x.hidden == hint.hidden)) === undefined)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
function hasHiddenHints(step: InteractiveGoalsWithHints): boolean {
|
||||
return step?.goals[0]?.hints.some((hint) => hint.hidden)
|
||||
}
|
||||
|
||||
|
||||
export function MoreHelpButton({selected=null} : {selected?: number}) {
|
||||
|
||||
const { t } = useTranslation()
|
||||
|
||||
const {proof, setProof} = React.useContext(ProofContext)
|
||||
const {deletedChat, setDeletedChat, showHelp, setShowHelp} = React.useContext(DeletedChatContext)
|
||||
|
||||
let k = proof?.steps.length ?
|
||||
((selected === null) ? (proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected)
|
||||
: 0
|
||||
|
||||
const activateHiddenHints = (ev) => {
|
||||
// If the last step (`k`) has errors, we want the hidden hints from the
|
||||
// second-to-last step to be affected
|
||||
if (!(proof?.steps.length)) {return}
|
||||
|
||||
// state must not be mutated, therefore we need to clone the set
|
||||
let tmp = new Set(showHelp)
|
||||
if (tmp.has(k)) {
|
||||
tmp.delete(k)
|
||||
} else {
|
||||
tmp.add(k)
|
||||
}
|
||||
setShowHelp(tmp)
|
||||
console.debug(`help: ${Array.from(tmp.values())}`)
|
||||
}
|
||||
|
||||
if (hasHiddenHints(proof?.steps[k]) && !showHelp.has(k)) {
|
||||
return <Button to="" onClick={activateHiddenHints}>
|
||||
{t("Show more help!")}
|
||||
</Button>
|
||||
}
|
||||
}
|
||||
@ -1,172 +1,274 @@
|
||||
import * as React from 'react';
|
||||
import { useState, useEffect } from 'react';
|
||||
import * as React from 'react'
|
||||
import { useState, useEffect, createContext, useContext } from 'react';
|
||||
import '../css/inventory.css'
|
||||
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
|
||||
import { faLock, faBan, faCheck } from '@fortawesome/free-solid-svg-icons'
|
||||
import { faLock, faBan, faCheck, faXmark } from '@fortawesome/free-solid-svg-icons'
|
||||
import { faClipboard } from '@fortawesome/free-regular-svg-icons'
|
||||
import { GameIdContext } from '../app';
|
||||
import Markdown from './markdown';
|
||||
import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery } from '../state/api';
|
||||
import { selectDifficulty, selectInventory } from '../state/progress';
|
||||
import { useLoadDocQuery, InventoryTile, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api';
|
||||
import { changedInventory, selectDifficulty, selectInventory } from '../state/progress';
|
||||
import { store } from '../state/store';
|
||||
import { useSelector } from 'react-redux';
|
||||
import { useTranslation } from 'react-i18next';
|
||||
import { t } from 'i18next';
|
||||
import { NavButton } from './navigation';
|
||||
import { LoadingIcon, Markdown } from './utils';
|
||||
import { GameIdContext } from '../state/context';
|
||||
import { useAppDispatch } from '../hooks';
|
||||
|
||||
export function Inventory({levelInfo, openDoc, lemmaTab, setLemmaTab, enableAll=false} :
|
||||
{
|
||||
levelInfo: LevelInfo|InventoryOverview,
|
||||
openDoc: (props: {name: string, type: string}) => void,
|
||||
lemmaTab: any,
|
||||
setLemmaTab: any,
|
||||
enableAll?: boolean,
|
||||
|
||||
/** Context which manages the inventory */
|
||||
const InventoryContext = createContext<{
|
||||
theoremTab: string,
|
||||
setTheoremTab: React.Dispatch<React.SetStateAction<string>>,
|
||||
categoryTab: "tactic"|"theorem"|"definition",
|
||||
setCategoryTab: React.Dispatch<React.SetStateAction<"tactic"|"theorem"|"definition">>,
|
||||
docTile: InventoryTile,
|
||||
setDocTile: React.Dispatch<React.SetStateAction<InventoryTile>>
|
||||
}>({
|
||||
theoremTab: null,
|
||||
setTheoremTab: () => {},
|
||||
categoryTab: "tactic",
|
||||
setCategoryTab: () => {},
|
||||
docTile: null,
|
||||
setDocTile: () => {}
|
||||
})
|
||||
|
||||
|
||||
/**
|
||||
*/
|
||||
function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc } :
|
||||
{ item: InventoryTile,
|
||||
name: any,
|
||||
displayName: any,
|
||||
locked: any,
|
||||
disabled: any,
|
||||
newly: any,
|
||||
showDoc: any
|
||||
}) {
|
||||
const { t } = useTranslation()
|
||||
const icon = locked ? <FontAwesomeIcon icon={faLock} /> :
|
||||
disabled ? <FontAwesomeIcon icon={faBan} /> : <></>
|
||||
const className = locked ? "locked" : disabled ? "disabled" : newly ? "new" : ""
|
||||
// Note: This is somewhat a hack as the statement of theorems comes currently in the form
|
||||
// `Namespace.statement_name (x y : Nat) : some type`
|
||||
const title = locked ? t("Not unlocked yet") :
|
||||
disabled ? t("Not available in this level") : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '')
|
||||
|
||||
return (
|
||||
<div className="inventory">
|
||||
{/* TODO: Click on Tactic: show info
|
||||
TODO: click on paste icon -> paste into command line */}
|
||||
<h2>{t("Tactics")}</h2>
|
||||
{levelInfo?.tactics &&
|
||||
<InventoryList items={levelInfo?.tactics} docType="Tactic" openDoc={openDoc} enableAll={enableAll}/>
|
||||
}
|
||||
<h2>{t("Definitions")}</h2>
|
||||
{levelInfo?.definitions &&
|
||||
<InventoryList items={levelInfo?.definitions} docType="Definition" openDoc={openDoc} enableAll={enableAll}/>
|
||||
const { gameId, worldId, levelId } = React.useContext(GameIdContext)
|
||||
const difficulty = useSelector(selectDifficulty(gameId))
|
||||
|
||||
// local state to show checkmark after pressing the copy button
|
||||
const [copied, setCopied] = useState(false)
|
||||
|
||||
const handleClick = () => {
|
||||
// if ((difficulty == 0) || !locked) {
|
||||
showDoc()
|
||||
// }
|
||||
}
|
||||
<h2>{t("Theorems")}</h2>
|
||||
{levelInfo?.lemmas &&
|
||||
<InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} level={levelInfo} enableAll={enableAll} tab={lemmaTab} setTab={setLemmaTab}/>
|
||||
|
||||
const copyItemName = (ev) => {
|
||||
navigator.clipboard.writeText(displayName)
|
||||
setCopied(true)
|
||||
setInterval(() => {
|
||||
setCopied(false)
|
||||
}, 3000);
|
||||
ev.stopPropagation()
|
||||
}
|
||||
|
||||
return <div className={`item ${className}` +
|
||||
`${(difficulty == 0) ? ' enabled' : ''}` +
|
||||
`${item.world == worldId && item.level == levelId - 1 ? ' recent' : ''}` +
|
||||
`${item.world == worldId && item.level < levelId ? ' current-world' : ''}` } onClick={handleClick} title={title}>
|
||||
{icon} {displayName}
|
||||
<div className="copy-button" onClick={copyItemName}>
|
||||
{copied ? <FontAwesomeIcon icon={faCheck} /> : <FontAwesomeIcon icon={faClipboard} />}
|
||||
</div>
|
||||
</div>
|
||||
)
|
||||
}
|
||||
|
||||
function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, level=undefined, enableAll=false} :
|
||||
|
||||
function InventoryList({ items, tab=null, setTab=()=>{} } :
|
||||
{
|
||||
items: InventoryTile[],
|
||||
docType: string,
|
||||
openDoc(props: {name: string, type: string}): void,
|
||||
tab?: any,
|
||||
setTab?: any,
|
||||
level?: LevelInfo|InventoryOverview,
|
||||
enableAll?: boolean,
|
||||
tab?: string,
|
||||
setTab?: React.Dispatch<React.SetStateAction<string>>
|
||||
}) {
|
||||
// TODO: `level` is only used in the `useEffect` below to check if a new level has
|
||||
// been loaded. Is there a better way to observe this?
|
||||
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
const { gameId, worldId, levelId } = React.useContext(GameIdContext)
|
||||
const { setDocTile, categoryTab, setCategoryTab } = useContext(InventoryContext)
|
||||
|
||||
const difficulty = useSelector(selectDifficulty(gameId))
|
||||
|
||||
const inventory: string[] = selectInventory(gameId)(store.getState())
|
||||
|
||||
const [categories, setCategories] = useState<Array<string>>([])
|
||||
const [modifiedItems, setModifiedItems] = useState<Array<InventoryTile>>([])
|
||||
const [currentWorldItems, setCurrentWorldItems] = useState<Array<InventoryTile>>([])
|
||||
|
||||
|
||||
useEffect(() => {
|
||||
const categorySet = new Set<string>()
|
||||
|
||||
if (!items) {return}
|
||||
for (let item of items) {
|
||||
categorySet.add(item.category)
|
||||
}
|
||||
const categories = Array.from(categorySet).sort()
|
||||
setCategories(Array.from(categorySet).sort())
|
||||
|
||||
// Add inventory items from local store as unlocked.
|
||||
// Items are unlocked if they are in the local store, or if the server says they should be
|
||||
// given the dependency graph. (OR-connection) (TODO: maybe add different logic for different
|
||||
// modi)
|
||||
let inv: string[] = selectInventory(gameId)(store.getState())
|
||||
let modifiedItems : InventoryTile[] = items.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile)
|
||||
let _modifiedItems : InventoryTile[] = items?.map(tile => inventory.includes(tile.name) ? {...tile, locked: false} : tile)
|
||||
setModifiedItems(_modifiedItems)
|
||||
// Item(s) proved in the preceeding level
|
||||
setCurrentWorldItems(_modifiedItems.filter(x => x.world == worldId && x.level < levelId))
|
||||
// setRecentItems(_modifiedItems.filter(x => x.world == worldId && x.level == levelId - 1))
|
||||
|
||||
}, []) // TODO: had `items, inventory`
|
||||
|
||||
return <>
|
||||
{ categories.length > 1 &&
|
||||
<div className="tab-bar">
|
||||
{categories.map((cat) =>
|
||||
<div key={`category-${cat}`} className={`tab ${cat == (tab ?? categories[0]) ? "active": ""}`}
|
||||
onClick={() => { setTab(cat) }}>{cat}</div>)}
|
||||
{categories.map((cat) => {
|
||||
let hasNew = modifiedItems.filter(item => item.new && (cat == item.category)).length > 0
|
||||
return <div key={`category-${cat}`} className={`tab${cat == (tab ?? categories[0]) ? " active": ""}${hasNew ? ' new': ''}${currentWorldItems.map(x => x.category).includes(cat) ? ' recent': ''}`}
|
||||
onClick={() => { setTab(cat) }}>{cat}</div>})}
|
||||
</div>}
|
||||
<div className="inventory-list">
|
||||
{[...modifiedItems].sort(
|
||||
// For lemas, sort entries `available > disabled > locked`
|
||||
// otherwise alphabetically
|
||||
(x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled) || x.displayName.localeCompare(y.displayName)
|
||||
// alternative approach:
|
||||
// // For theorems, sort entries `available > disabled > locked`
|
||||
// // otherwise alphabetically
|
||||
// (x, y) => +(categoryTab == "theorem") * (+x.locked - +y.locked || +x.disabled - +y.disabled) || x.displayName.localeCompare(y.displayName)
|
||||
|
||||
// sort alphabetically
|
||||
(x, y) => x.displayName.localeCompare(y.displayName)
|
||||
).filter(item => !item.hidden && ((tab ?? categories[0]) == item.category)).map((item, i) => {
|
||||
return <InventoryItem key={`${item.category}-${item.name}`}
|
||||
item={item}
|
||||
showDoc={() => {openDoc({name: item.name, type: docType})}}
|
||||
showDoc={() => {setDocTile(item)}}
|
||||
name={item.name} displayName={item.displayName} locked={difficulty > 0 ? item.locked : false}
|
||||
disabled={item.disabled} newly={item.new} enableAll={enableAll} />
|
||||
disabled={item.disabled}
|
||||
newly={item.new} />
|
||||
})
|
||||
}
|
||||
</div>
|
||||
</>
|
||||
}
|
||||
|
||||
function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc, enableAll=false}) {
|
||||
const icon = locked ? <FontAwesomeIcon icon={faLock} /> :
|
||||
disabled ? <FontAwesomeIcon icon={faBan} /> : item.st
|
||||
const className = locked ? "locked" : disabled ? "disabled" : newly ? "new" : ""
|
||||
// Note: This is somewhat a hack as the statement of lemmas comes currently in the form
|
||||
// `Namespace.statement_name (x y : Nat) : some type`
|
||||
const title = locked ? t("Not unlocked yet") :
|
||||
disabled ? t("Not available in this level") : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '')
|
||||
|
||||
const [copied, setCopied] = useState(false)
|
||||
|
||||
const handleClick = () => {
|
||||
if (enableAll || !locked) {
|
||||
showDoc()
|
||||
}
|
||||
}
|
||||
/** The `Inventory` shows all items present in the game sorted by item type. */
|
||||
export function Inventory () {
|
||||
const { t } = useTranslation()
|
||||
|
||||
const copyItemName = (ev) => {
|
||||
navigator.clipboard.writeText(displayName)
|
||||
setCopied(true)
|
||||
setInterval(() => {
|
||||
setCopied(false)
|
||||
}, 3000);
|
||||
ev.stopPropagation()
|
||||
const { gameId, worldId, levelId } = React.useContext(GameIdContext)
|
||||
const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
|
||||
|
||||
let { theoremTab, setTheoremTab, categoryTab, setCategoryTab } = useContext(InventoryContext)
|
||||
|
||||
/** Helper function to find if a list of tiles comprises any new elements. */
|
||||
function containsNew(tiles: InventoryTile[]) {
|
||||
return tiles?.filter(item => item.new).length > 0
|
||||
}
|
||||
|
||||
return <div className={`item ${className}${enableAll ? ' enabled' : ''}`} onClick={handleClick} title={title}>
|
||||
{icon} {displayName}
|
||||
<div className="copy-button" onClick={copyItemName}>
|
||||
{copied ? <FontAwesomeIcon icon={faCheck} /> : <FontAwesomeIcon icon={faClipboard} />}
|
||||
return (
|
||||
<div className="inventory">
|
||||
{ levelInfo.data ? <>
|
||||
<div className="tab-bar major">
|
||||
<div className={`tab${(categoryTab == "theorem") ? " active": ""}${containsNew(levelInfo.data?.theorems) ? " new" : ""}`} onClick={() => { setCategoryTab("theorem") }}>{t("Theorems")}</div>
|
||||
<div className={`tab${(categoryTab == "tactic") ? " active": ""}${containsNew(levelInfo.data?.tactics) ? " new" : ""}`} onClick={() => { setCategoryTab("tactic") }}>{t("Tactics")}</div>
|
||||
<div className={`tab${(categoryTab == "definition") ? " active": ""}${containsNew(levelInfo.data?.definitions) ? " new" : ""}`} onClick={() => { setCategoryTab("definition") }}>{t("Definitions")}</div>
|
||||
</div>
|
||||
{ (categoryTab == "theorem") &&
|
||||
<InventoryList items={levelInfo.data?.theorems} tab={theoremTab} setTab={setTheoremTab} />
|
||||
}
|
||||
{ (categoryTab == "tactic") &&
|
||||
<InventoryList items={levelInfo.data?.tactics} />
|
||||
}
|
||||
{ (categoryTab == "definition") &&
|
||||
<InventoryList items={levelInfo.data?.definitions} />
|
||||
}
|
||||
</> : <LoadingIcon /> }
|
||||
</div>
|
||||
)
|
||||
}
|
||||
|
||||
export function Documentation({name, type, handleClose}) {
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
const doc = useLoadDocQuery({game: gameId, type: type, name: name})
|
||||
/** The `documentation` */
|
||||
export function Documentation() {
|
||||
const dispatch = useAppDispatch()
|
||||
const { gameId } = useContext(GameIdContext)
|
||||
const difficulty = useSelector(selectDifficulty(gameId))
|
||||
|
||||
// const docEntry = useLoadDocQuery({game: gameId, type: type, name: name})
|
||||
let { docTile, setDocTile } = useContext(InventoryContext)
|
||||
|
||||
const docEntry = useLoadDocQuery({game: gameId, name: docTile.name})
|
||||
let inv: string[] = selectInventory(gameId)(store.getState())
|
||||
|
||||
// Set `inventoryDoc` to `null` to close the doc
|
||||
function closeInventoryDoc() { setDocTile(null) }
|
||||
|
||||
return <div className="documentation">
|
||||
<div className="codicon codicon-close modal-close" onClick={handleClose}></div>
|
||||
<h1 className="doc">{doc.data?.displayName}</h1>
|
||||
<p><code>{doc.data?.statement}</code></p>
|
||||
{/* <code>docstring: {doc.data?.docstring}</code> */}
|
||||
<Markdown>{t(doc.data?.content, {ns: gameId})}</Markdown>
|
||||
</div>
|
||||
<NavButton
|
||||
icon={faXmark}
|
||||
onClick={closeInventoryDoc}
|
||||
inverted={true} />
|
||||
{ difficulty == 1 && docTile.locked &&
|
||||
<NavButton
|
||||
icon={faLock}
|
||||
title={t("Unlock this item!")}
|
||||
onClick={() => {
|
||||
console.log(`Adding '${docTile.name}' to the inventory.`)
|
||||
dispatch(changedInventory({ game: gameId, inventory: [...inv, docTile.name] }))
|
||||
closeInventoryDoc() // note: closing seems better than keeping it open without the lock disappearing
|
||||
}}
|
||||
className="lock"
|
||||
inverted={true} />
|
||||
}
|
||||
<h1 className="doc">{docTile.displayName}</h1>
|
||||
<p><code>{docEntry.data?.statement}</code></p>
|
||||
<Markdown>{t(docEntry.data?.content, {ns: gameId})}</Markdown>
|
||||
{/* TODO: The condition below should be updated so that the section
|
||||
is displayed whenever it's non-empty. */}
|
||||
{docTile.proven && <>
|
||||
<h2>Further details</h2>
|
||||
<ul>
|
||||
{docTile.proven && <li>Proven in: <a href={`#/${gameId}/world/${docTile.world}/level/${docTile.level}`}>{docTile.world} level {docTile.level}</a></li>}
|
||||
</ul>
|
||||
</>
|
||||
}
|
||||
|
||||
/** The panel (on the welcome page) showing the user's inventory with tactics, definitions, and lemmas */
|
||||
export function InventoryPanel({levelInfo, visible = true}) {
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
</div>
|
||||
}
|
||||
|
||||
const [lemmaTab, setLemmaTab] = useState(levelInfo?.lemmaTab)
|
||||
/** The panel showing the user's inventory with tactics, definitions, and theorems */
|
||||
export function InventoryPanel({visible = true}) {
|
||||
const {gameId, worldId, levelId} = React.useContext(GameIdContext)
|
||||
const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
|
||||
const inventory = useLoadInventoryOverviewQuery({game: gameId})
|
||||
|
||||
const [theoremTab, setTheoremTab] = useState<string>(null)
|
||||
const [categoryTab, setCategoryTab] = useState<"tactic"|"theorem"|"definition">('tactic')
|
||||
// The inventory is overlayed by the doc entry of a clicked item
|
||||
const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null)
|
||||
// Set `inventoryDoc` to `null` to close the doc
|
||||
function closeInventoryDoc() {setInventoryDoc(null)}
|
||||
const [docTile, setDocTile] = useState<InventoryTile>(null)
|
||||
|
||||
useEffect(() => {
|
||||
// If the level specifies `LemmaTab "Nat"`, we switch to this tab on loading.
|
||||
// If the level specifies `TheoremTab "Nat"`, we switch to this tab on loading.
|
||||
// `defaultTab` is `null` or `undefined` otherwise, in which case we don't want to switch.
|
||||
if (levelInfo?.lemmaTab) {
|
||||
setLemmaTab(levelInfo?.lemmaTab)
|
||||
if (levelInfo?.data?.theoremTab) {
|
||||
setTheoremTab(levelInfo?.data?.theoremTab)
|
||||
}}, [levelInfo])
|
||||
|
||||
return <div className={`column inventory-panel ${visible ? '' : 'hidden'}`}>
|
||||
{inventoryDoc ?
|
||||
<Documentation name={inventoryDoc.name} type={inventoryDoc.type} handleClose={closeInventoryDoc}/>
|
||||
<InventoryContext.Provider value={{theoremTab, setTheoremTab, categoryTab, setCategoryTab, docTile, setDocTile }}>
|
||||
{docTile ?
|
||||
<Documentation />
|
||||
:
|
||||
<Inventory levelInfo={levelInfo} openDoc={setInventoryDoc} enableAll={true} lemmaTab={lemmaTab} setLemmaTab={setLemmaTab}/>
|
||||
<Inventory />
|
||||
}
|
||||
</InventoryContext.Provider>
|
||||
</div>
|
||||
}
|
||||
|
||||
// HERE: next up: locked items should not be disabled!
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
@ -1,19 +0,0 @@
|
||||
import * as React from 'react';
|
||||
import ReactMarkdown from 'react-markdown';
|
||||
import remarkMath from 'remark-math'
|
||||
import rehypeKatex from 'rehype-katex'
|
||||
import 'katex/dist/katex.min.css' // `rehype-katex` does not import the CSS for you
|
||||
import gfm from "remark-gfm";
|
||||
|
||||
function Markdown(props) {
|
||||
const newProps = {
|
||||
...props,
|
||||
remarkPlugins: [...props.remarkPlugins ?? [], remarkMath, gfm],
|
||||
rehypePlugins: [...props.remarkPlugins ?? [], rehypeKatex],
|
||||
};
|
||||
return (
|
||||
<ReactMarkdown {...newProps} className="markdown" />
|
||||
);
|
||||
}
|
||||
|
||||
export default Markdown
|
||||
@ -0,0 +1,363 @@
|
||||
import * as React from 'react'
|
||||
import { createContext, useContext, useState } from 'react'
|
||||
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
|
||||
import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome,
|
||||
faArrowRight, faArrowLeft, faXmark, faBars, faCode,
|
||||
faCircleInfo, faTerminal, faGear, IconDefinition, faShield } from '@fortawesome/free-solid-svg-icons'
|
||||
import { GameIdContext, PageContext, PreferencesContext } from "../state/context"
|
||||
import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api'
|
||||
import { downloadProgress } from './popup/erase'
|
||||
import { useTranslation } from 'react-i18next'
|
||||
import '../css/navigation.css'
|
||||
import { PopupContext } from './popup/popup'
|
||||
import { useSelector } from 'react-redux'
|
||||
import { selectCompleted, selectDifficulty, selectProgress, selectReadIntro } from '../state/progress'
|
||||
import lean4gameConfig from '../config.json'
|
||||
import { Flag } from './flag'
|
||||
import { useAppSelector } from '../hooks'
|
||||
|
||||
/** SVG github icon */
|
||||
function GithubIcon () {
|
||||
return <svg className="svg-inline--fa" height="24" aria-hidden="true" viewBox="0 0 16 16" version="1.1" width="24" >
|
||||
<path fill="#fff" d="M8 0c4.42 0 8 3.58 8 8a8.013 8.013 0 0 1-5.45 7.59c-.4.08-.55-.17-.55-.38 0-.27.01-1.13.01-2.2 0-.75-.25-1.23-.54-1.48 1.78-.2 3.65-.88 3.65-3.95 0-.88-.31-1.59-.82-2.15.08-.2.36-1.02-.08-2.12 0 0-.67-.22-2.2.82-.64-.18-1.32-.27-2-.27-.68 0-1.36.09-2 .27-1.53-1.03-2.2-.82-2.2-.82-.44 1.1-.16 1.92-.08 2.12-.51.56-.82 1.28-.82 2.15 0 3.06 1.86 3.75 3.64 3.95-.23.2-.44.55-.51 1.07-.46.21-1.61.55-2.33-.66-.15-.24-.6-.83-1.23-.82-.67.01-.27.38.01.53.34.19.73.9.82 1.13.16.45.68 1.31 2.69.94 0 .67.01 1.3.01 1.49 0 .21-.15.45-.55.38A7.995 7.995 0 0 1 0 8c0-4.42 3.58-8 8-8Z"></path>
|
||||
</svg>
|
||||
}
|
||||
|
||||
/** A button to appear in the navigation (both, top bar or dropdown). */
|
||||
export const NavButton: React.FC<{
|
||||
icon?: IconDefinition
|
||||
iconElement?: JSX.Element
|
||||
text?: string
|
||||
onClick?: React.MouseEventHandler<HTMLAnchorElement>
|
||||
title?: string
|
||||
href?: string
|
||||
inverted?: boolean
|
||||
disabled?: boolean
|
||||
className?: string
|
||||
}> = ({icon, iconElement, text, onClick=()=>{}, title, href=null, inverted=false, disabled=false, className=''}) => {
|
||||
return <a className={`${className} nav-button btn${inverted?' btn-inverted':''}${disabled?' btn-disabled':''}`} onClick={disabled?null:onClick} href={disabled?null:href} title={title}>
|
||||
{iconElement ?? (icon && <FontAwesomeIcon icon={icon} />)}{text && <> {text}</>}
|
||||
</a>
|
||||
}
|
||||
|
||||
/** Context which manages the dropdown navigation */
|
||||
const NavigationContext = createContext<{
|
||||
navOpen: boolean,
|
||||
setNavOpen: React.Dispatch<React.SetStateAction<boolean>>
|
||||
}>({navOpen: false, setNavOpen: () => {}})
|
||||
|
||||
/** Content of the navigation during game selection. */
|
||||
function NavigationLandingPage () {
|
||||
return <div className="nav-content">
|
||||
<div className="nav-title-left"></div>
|
||||
<div className="nav-title-middle"></div>
|
||||
<div className="nav-title-right"></div>
|
||||
</div>
|
||||
}
|
||||
|
||||
/** Content of the navigation on Desktop during world selection. */
|
||||
function DesktopNavigationOverview () {
|
||||
const { t } = useTranslation()
|
||||
const { gameId } = useContext(GameIdContext)
|
||||
const { setPopupContent } = useContext(PopupContext)
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
|
||||
return <div className="nav-content">
|
||||
<div className="nav-title-left">
|
||||
<NavButton
|
||||
text={t("Rules")}
|
||||
onClick={() => {setPopupContent("rules")}}
|
||||
inverted={true} />
|
||||
</div>
|
||||
<div className="nav-title-middle">
|
||||
<span className="nav-title">{t(gameInfo.data?.title, {ns: gameId})}</span>
|
||||
</div>
|
||||
<div className="nav-title-right"></div>
|
||||
</div>
|
||||
}
|
||||
|
||||
/** Content of the navigation on Mobile during world selection. */
|
||||
function MobileNavigationOverview () {
|
||||
const { t } = useTranslation()
|
||||
const {page, setPage} = useContext(PageContext)
|
||||
const { setPopupContent } = useContext(PopupContext)
|
||||
|
||||
const { gameId, worldId } = useContext(GameIdContext)
|
||||
const readIntro = useSelector(selectReadIntro(gameId, worldId))
|
||||
|
||||
return <div className="nav-content">
|
||||
<div className="nav-title-left">
|
||||
<NavButton
|
||||
text={t("Rules")}
|
||||
onClick={() => {setPopupContent("rules")}}
|
||||
inverted={true} />
|
||||
</div>
|
||||
<div className="nav-title-middle">
|
||||
<span className="nav-title">
|
||||
</span>
|
||||
</div>
|
||||
<div className="nav-title-right">
|
||||
{page > 0 &&
|
||||
<NavButton
|
||||
text={page == 1 ? t("Intro") : null}
|
||||
icon={page == 1 ? null : faBookOpen}
|
||||
onClick={() => setPage(page - 1)}
|
||||
inverted={true} />
|
||||
}
|
||||
{ page < 2 &&
|
||||
<NavButton
|
||||
text={(page==0) ? t("Start") : null}
|
||||
icon={(page==0) ? null : faBook}
|
||||
onClick={() => setPage(page+1)}
|
||||
disabled={!readIntro}
|
||||
inverted={true} />
|
||||
}
|
||||
</div>
|
||||
|
||||
</div>
|
||||
}
|
||||
|
||||
/** Content of the navigation on Desktop in a level. */
|
||||
function DesktopNavigationLevel () {
|
||||
const { t } = useTranslation()
|
||||
const { gameId, worldId, levelId } = useContext(GameIdContext)
|
||||
const { typewriterMode, setTypewriterMode, lockEditorMode } = useContext(PageContext)
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
|
||||
const difficulty = useSelector(selectDifficulty(gameId))
|
||||
const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
|
||||
|
||||
const readIntro = useSelector(selectReadIntro(gameId, worldId))
|
||||
|
||||
const worldTitle = gameInfo.data?.worlds.nodes[worldId]?.title
|
||||
const levelTitle = ((levelId == 0) ?
|
||||
t("Introduction") :
|
||||
(
|
||||
t("Level") +
|
||||
` ${levelId}` +
|
||||
(gameInfo.data?.worldSize[worldId] ? ` / ${gameInfo.data?.worldSize[worldId]}` : '') +
|
||||
(levelInfo.data?.title ? ` : ${t(levelInfo?.data?.title, {ns: gameId})}` : '')
|
||||
)
|
||||
)
|
||||
|
||||
return <div className="nav-content">
|
||||
<div className="nav-title-left">
|
||||
<span className="nav-title">{worldTitle ? `${t(worldTitle, {ns: gameId})}` : '' /* ${t("World")}: */ }
|
||||
</span>
|
||||
</div>
|
||||
<div className="nav-title-middle">
|
||||
<span className="nav-title">
|
||||
{ levelTitle
|
||||
}
|
||||
</span>
|
||||
</div>
|
||||
<div className="nav-title-right" >
|
||||
{ levelId > 0 &&
|
||||
<NavButton
|
||||
icon={faArrowLeft}
|
||||
text={t("Previous")}
|
||||
inverted={true}
|
||||
href={`#/${gameId}/world/${worldId}/level/${levelId - 1}`} />
|
||||
}
|
||||
{ levelId == gameInfo.data?.worldSize[worldId] ?
|
||||
<NavButton
|
||||
icon={faHome}
|
||||
text={t("Home")}
|
||||
inverted={true}
|
||||
disabled={levelId > 0 && difficulty == 2 && !completed}
|
||||
href={`#/${gameId}`} /> :
|
||||
<NavButton
|
||||
icon={faArrowRight}
|
||||
text={levelId == 0 ? t("Start") : t("Next")} inverted={true}
|
||||
disabled={levelId == 0 ? !readIntro : (difficulty == 2 && !completed)}
|
||||
href={`#/${gameId}/world/${worldId}/level/${levelId + 1}`} />
|
||||
}
|
||||
</div>
|
||||
</div>
|
||||
}
|
||||
|
||||
/** Content of the navigation on Mobile in a level. */
|
||||
function MobileNavigationLevel () {
|
||||
const { t } = useTranslation()
|
||||
const {gameId, worldId, levelId} = useContext(GameIdContext)
|
||||
const {page, setPage} = useContext(PageContext)
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
|
||||
|
||||
let title = worldId ?
|
||||
` ${levelId} / ${gameInfo.data?.worldSize[worldId]}`+ (levelInfo?.data?.title && ` : ${t(levelInfo?.data?.title, {ns: gameId})}`)
|
||||
:
|
||||
''
|
||||
|
||||
return <div className="nav-content">
|
||||
<div className="nav-title-left"></div>
|
||||
<div className="nav-title-middle">
|
||||
<span className="nav-title">
|
||||
{title}
|
||||
</span>
|
||||
</div>
|
||||
<div className="nav-title-right">
|
||||
<NavButton
|
||||
icon={(page == 1) ? faBook : faBookOpen}
|
||||
onClick={() => setPage((page == 1) ? 2 : 1)}
|
||||
inverted={true} />
|
||||
</div>
|
||||
</div>
|
||||
}
|
||||
|
||||
/** The skeleton of the navigation which is the same across all layouts. */
|
||||
export function Navigation () {
|
||||
const { t, i18n } = useTranslation()
|
||||
const { gameId, worldId, levelId } = useContext(GameIdContext)
|
||||
const { mobile, language, setLanguage } = useContext(PreferencesContext)
|
||||
const { setPopupContent } = useContext(PopupContext)
|
||||
const { typewriterMode, setTypewriterMode, lockEditorMode } = useContext(PageContext)
|
||||
const gameProgress = useSelector(selectProgress(gameId))
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
const levelInfo = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
|
||||
const difficulty = useSelector(selectDifficulty(gameId))
|
||||
const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
|
||||
|
||||
const readIntro = useSelector(selectReadIntro(gameId, worldId))
|
||||
|
||||
const [navOpen, setNavOpen] = useState(false)
|
||||
const [langNavOpen, setLangNavOpen] = useState(false)
|
||||
function toggleNav () {setNavOpen(!navOpen); setLangNavOpen(false)}
|
||||
function toggleLangNav () {setLangNavOpen(!langNavOpen); setNavOpen(false)}
|
||||
|
||||
/** toggle input mode if allowed */
|
||||
function toggleInputMode(ev: React.MouseEvent) {
|
||||
if (!lockEditorMode) {
|
||||
setTypewriterMode(!typewriterMode)
|
||||
console.log('test')
|
||||
}
|
||||
}
|
||||
|
||||
return <nav>
|
||||
<NavigationContext.Provider value={{navOpen, setNavOpen}}>
|
||||
{ gameId && <>
|
||||
<NavButton
|
||||
icon={worldId ? faHome : faGlobe}
|
||||
title={worldId ? t("home") : t("back to games selection")}
|
||||
href={worldId ? `#/${gameId}` : `#`} />
|
||||
</>}
|
||||
{ gameId ?
|
||||
worldId ?
|
||||
(mobile ? <MobileNavigationLevel /> : <DesktopNavigationLevel />) :
|
||||
(mobile ? <MobileNavigationOverview /> : <DesktopNavigationOverview />) :
|
||||
<NavigationLandingPage />
|
||||
}
|
||||
{ !gameId &&
|
||||
<NavButton
|
||||
iconElement={<GithubIcon />}
|
||||
title={t("view the Lean game server on Github")}
|
||||
href='https://github.com/leanprover-community/lean4game' />
|
||||
}
|
||||
{(!gameId || gameInfo.data?.tile?.languages.length > 1) &&
|
||||
// Language button only visible if the game exists in `>1` languages
|
||||
<NavButton
|
||||
iconElement={langNavOpen ? null : <Flag iso={i18n.language} />}
|
||||
icon={langNavOpen ? faXmark : null}
|
||||
title={langNavOpen ? t('close language menu') : t('open language menu')}
|
||||
onClick={toggleLangNav}
|
||||
/>
|
||||
}
|
||||
<NavButton
|
||||
icon={navOpen ? faXmark : faBars}
|
||||
title={navOpen ? t('close menu') : t('open menu')}
|
||||
onClick={toggleNav} />
|
||||
{ langNavOpen &&
|
||||
<div className='dropdown' onClick={toggleLangNav} >
|
||||
{gameId && gameInfo.data?.tile?.languages ?
|
||||
// Show all languages the game is available in
|
||||
gameInfo.data?.tile?.languages.map(iso =>
|
||||
<NavButton
|
||||
key={`lang-selection-${iso}`}
|
||||
iconElement={<Flag iso={iso} />}
|
||||
text={lean4gameConfig.newLanguages[iso]?.name}
|
||||
onClick={() => {setLanguage(iso)}}
|
||||
inverted={true} />) :
|
||||
// Show all languages the interface is available in (e.g. landing page)
|
||||
Object.entries(lean4gameConfig.newLanguages).map(([iso, val]) =>
|
||||
<NavButton
|
||||
key={`lang-selection-${iso}`}
|
||||
iconElement={<Flag iso={iso} />}
|
||||
text={lean4gameConfig.newLanguages[iso]?.name}
|
||||
onClick={() => {setLanguage(iso)}}
|
||||
inverted={true} />)
|
||||
}
|
||||
</div>
|
||||
}
|
||||
{ navOpen &&
|
||||
<div className='dropdown' onClick={toggleNav} >
|
||||
{ gameId && <>
|
||||
{ mobile && (levelId == gameInfo.data?.worldSize[worldId] ?
|
||||
<NavButton
|
||||
icon={faHome}
|
||||
text={t("Home")}
|
||||
inverted={true}
|
||||
disabled={levelId > 0 && difficulty == 2 && !completed}
|
||||
href={`#/${gameId}`} /> :
|
||||
<NavButton
|
||||
icon={faArrowRight}
|
||||
text={levelId == 0 ? t("Start") : t("Next")} inverted={true}
|
||||
disabled={levelId == 0 ? !readIntro : (difficulty == 2 && !completed)}
|
||||
href={`#/${gameId}/world/${worldId}/level/${levelId + 1}`} />
|
||||
)}
|
||||
{mobile && levelId > 0 &&
|
||||
<NavButton
|
||||
icon={faArrowLeft}
|
||||
text={t("Previous")}
|
||||
inverted={true}
|
||||
href={`#/${gameId}/world/${worldId}/level/${levelId - 1}`} />
|
||||
}
|
||||
{ mobile && levelId > 0 &&
|
||||
<NavButton
|
||||
icon={(typewriterMode && !lockEditorMode) ? faCode : faTerminal}
|
||||
inverted={true}
|
||||
text={typewriterMode ? t("Editor Mode") : t("Typewriter Mode")}
|
||||
disabled={levelId == 0 || lockEditorMode}
|
||||
onClick={(ev) => toggleInputMode(ev)}
|
||||
title={lockEditorMode ? t("Editor mode is enforced!") : typewriterMode ? t("Editor mode") : t("Typewriter mode")} />
|
||||
}
|
||||
<NavButton
|
||||
icon={faCircleInfo}
|
||||
text={t("Game Info")}
|
||||
onClick={() => {setPopupContent("info")}}
|
||||
inverted={true} />
|
||||
<NavButton
|
||||
icon={faEraser}
|
||||
text={t("Erase")}
|
||||
onClick={() => {setPopupContent("erase")}}
|
||||
inverted={true} />
|
||||
<NavButton
|
||||
icon={faDownload}
|
||||
text={t("Download")}
|
||||
onClick={() => {downloadProgress(gameId, gameProgress)}}
|
||||
inverted={true} />
|
||||
<NavButton
|
||||
icon={faUpload}
|
||||
text={t("Upload")}
|
||||
onClick={() => {setPopupContent("upload")}}
|
||||
inverted={true} />
|
||||
</>}
|
||||
<NavButton
|
||||
icon={faCircleInfo}
|
||||
text={t("Impressum")}
|
||||
onClick={() => {setPopupContent("impressum")}}
|
||||
inverted={true} />
|
||||
<NavButton
|
||||
icon={faShield}
|
||||
text={t("Privacy Policy")}
|
||||
onClick={() => {setPopupContent("privacy")}}
|
||||
inverted={true} />
|
||||
<NavButton
|
||||
icon={faGear}
|
||||
text={t("Preferences")}
|
||||
onClick={() => {setPopupContent("preferences")}}
|
||||
inverted={true} />
|
||||
</div>
|
||||
}
|
||||
</NavigationContext.Provider>
|
||||
</nav>
|
||||
}
|
||||
@ -1,28 +0,0 @@
|
||||
/**
|
||||
* @fileOverview
|
||||
*/
|
||||
import * as React from 'react'
|
||||
import { Typography } from '@mui/material'
|
||||
import Markdown from '../markdown'
|
||||
import { useTranslation } from 'react-i18next'
|
||||
import { GameIdContext } from '../../app'
|
||||
|
||||
/** 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}) {
|
||||
let { t } = useTranslation()
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
|
||||
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>{t(info, {ns: gameId})}</Markdown>
|
||||
</Typography>
|
||||
</div>
|
||||
</div>
|
||||
}
|
||||
@ -0,0 +1,43 @@
|
||||
import * as React from 'react'
|
||||
import { Trans, useTranslation } from 'react-i18next';
|
||||
|
||||
/** Pop-up that is displayed when opening the privacy policy. */
|
||||
export function ImpressumPopup () {
|
||||
let {t, i18n} = useTranslation()
|
||||
|
||||
function content (lng = i18n.language) {
|
||||
const tt = i18n.getFixedT(lng);
|
||||
return <Trans t={tt} >
|
||||
<h2>Impressum</h2>
|
||||
<p>
|
||||
<strong>Contact:</strong><br />
|
||||
Marcus Zibrowius, Jon Eugster<br />
|
||||
Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br />
|
||||
Universitätsstr. 1<br />
|
||||
40225 Düsseldorf<br />
|
||||
Germany<br />
|
||||
+49 211 81-14690<br />
|
||||
<a href="https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team">Contact Details</a>
|
||||
</p>
|
||||
<p>
|
||||
<strong>Legal form:</strong><br />
|
||||
The Heinrich Heine University Düsseldorf is a corporation under public law. It is legally represented by the Rector Prof. Dr. Anja Steinbeck. The responsible supervisory authority is the Ministry of Culture and Science of North Rhine-Westphalia, Völklinger Straße 49, 40221 Düsseldorf.
|
||||
</p>
|
||||
<p>
|
||||
<strong>VAT identification number:</strong><br />
|
||||
according to §27a Sales Tax Act<br />
|
||||
DE 811222416
|
||||
</p>
|
||||
<p><a href="https://www.hhu.de/impressum" target="_blank">Impressum HHU</a></p>
|
||||
</Trans>
|
||||
}
|
||||
|
||||
return <>
|
||||
{i18n.language != 'en' && <>
|
||||
<p><i>(English version below)</i></p>
|
||||
{content()}
|
||||
<hr />
|
||||
</>}
|
||||
{content('en')}
|
||||
</>
|
||||
}
|
||||
@ -0,0 +1,56 @@
|
||||
import * as React from 'react'
|
||||
import { Typography } from '@mui/material'
|
||||
import { Markdown } from '../utils'
|
||||
import { Trans, useTranslation } from 'react-i18next'
|
||||
import { useGetGameInfoQuery } from '../../state/api'
|
||||
import { GameIdContext } from '../../state/context'
|
||||
|
||||
/** 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 () {
|
||||
let { t } = useTranslation()
|
||||
const {gameId} = React.useContext(GameIdContext)
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
|
||||
return <>
|
||||
<Typography variant="body1" component="div" className="welcome-text">
|
||||
<Markdown>{t(gameInfo.data?.info, {ns: gameId})}</Markdown>
|
||||
<hr />
|
||||
<Trans>
|
||||
<h2>Progress saving</h2>
|
||||
<p>
|
||||
The game stores your progress in your local browser storage. If you delete it, your progress will be lost!<br />
|
||||
Warning: In most browsers, deleting cookies will also clear the local storage (or "local site data").
|
||||
Make sure to download your game progress first!
|
||||
</p>
|
||||
<h2>Accessibility</h2>
|
||||
<p>
|
||||
If you experience any accessibilty barriers, please get in contact with us!
|
||||
We are dedicated to address such barriers to the best of our abilities.
|
||||
</p>
|
||||
<h2>Development</h2>
|
||||
<p>The game engine has been created by <strong>Alexander Bentkamp</strong>, <strong>Jon Eugster</strong>.
|
||||
On a prototype by <strong>Patrick Massot</strong>.
|
||||
</p>
|
||||
<p>
|
||||
The source code of this Lean game engine
|
||||
is <a href="https://github.com/leanprover-community/lean4game" target="_blank">available on Github</a>.
|
||||
If you experience any problems, please
|
||||
file an <a href="https://github.com/leanprover-community/lean4game/issues" target="_blank">Issue on Github</a> or
|
||||
get directly in contact.
|
||||
</p>
|
||||
<h2>Funding</h2>
|
||||
<p>
|
||||
The game engine has been developed as part of the
|
||||
project <a href="https://hhu-adam.github.io/" target="_blank">ADAM: Anticipating the Digital
|
||||
Age of Mathematics</a> at
|
||||
Heinrich-Heine-Universität Düsseldorf. It is funded by
|
||||
the <i>Stiftung Innovation in der Hochschullehre</i> as part of project <i>Freiraum 2022</i>.
|
||||
</p>
|
||||
</Trans>
|
||||
</Typography>
|
||||
</>
|
||||
}
|
||||
@ -0,0 +1,58 @@
|
||||
import * as React from 'react'
|
||||
import { useContext } from 'react'
|
||||
import { PrivacyPolicyPopup } from './privacy'
|
||||
import { ImpressumPopup } from './impressum'
|
||||
import { InfoPopup } from './info'
|
||||
import { ErasePopup } from './erase'
|
||||
import { PreferencesPopup } from './preferences'
|
||||
import { UploadPopup } from './upload'
|
||||
import { RulesPopup } from './rules'
|
||||
import '../../css/popup.css'
|
||||
import { NavButton } from '../navigation'
|
||||
import { faXmark } from '@fortawesome/free-solid-svg-icons'
|
||||
|
||||
/** The context which manages if a popup is shown.
|
||||
* If `popupContent` is `null`, the popup is closed.
|
||||
*/
|
||||
export const PopupContext = React.createContext<{
|
||||
popupContent: string,
|
||||
setPopupContent: React.Dispatch<React.SetStateAction<string>>
|
||||
}>({
|
||||
popupContent: null,
|
||||
setPopupContent: () => {}
|
||||
})
|
||||
|
||||
/** To create a new Popup, one needs to add its content as `React.JSX.Element` here
|
||||
* and then call `setPopupConent(key)` at the place where to popup should be opened.
|
||||
*
|
||||
* TODO: The drawback of this design is that there is no check for key missmatches.
|
||||
* How could that be achieved?
|
||||
*/
|
||||
export const Popups = {
|
||||
"erase": <ErasePopup />,
|
||||
"impressum": <ImpressumPopup />,
|
||||
"info": <InfoPopup />,
|
||||
"preferences": <PreferencesPopup />,
|
||||
"privacy": <PrivacyPolicyPopup />,
|
||||
"rules": <RulesPopup />,
|
||||
"upload": <UploadPopup />,
|
||||
}
|
||||
|
||||
/** The skeleton for the popups. */
|
||||
export function Popup () {
|
||||
const {popupContent, setPopupContent} = useContext(PopupContext)
|
||||
function closePopup() {
|
||||
setPopupContent(null)
|
||||
}
|
||||
|
||||
return <div className="modal-wrapper">
|
||||
<div className="modal-backdrop" onClick={closePopup} />
|
||||
<div className="modal">
|
||||
{/* <NavButton icon={faXmark}
|
||||
onClick={closePopup}
|
||||
inverted={true} /> */}
|
||||
<div className="codicon codicon-close modal-close" onClick={closePopup}></div>
|
||||
{Popups[popupContent]}
|
||||
</div>
|
||||
</div>
|
||||
}
|
||||
@ -0,0 +1,48 @@
|
||||
import * as React from 'react'
|
||||
import { Trans, useTranslation } from 'react-i18next';
|
||||
|
||||
/** Pop-up that is displayed when opening the privacy policy.
|
||||
*
|
||||
* Note: Do not translate the Impressum!
|
||||
*/
|
||||
export function PrivacyPolicyPopup () {
|
||||
let {t, i18n} = useTranslation()
|
||||
function content (lng = i18n.language) {
|
||||
const tt = i18n.getFixedT(lng);
|
||||
return <Trans t={tt} >
|
||||
<h2>Privacy Policy</h2>
|
||||
<p>
|
||||
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.
|
||||
</p>
|
||||
<p>
|
||||
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.
|
||||
</p>
|
||||
<p>Our server is located in Germany.</p>
|
||||
<p>
|
||||
<strong>Contact:</strong><br />
|
||||
Marcus Zibrowius, Jon Eugster<br />
|
||||
Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br />
|
||||
Universitätsstr. 1<br />
|
||||
40225 Düsseldorf<br />
|
||||
Germany<br />
|
||||
+49 211 81-14690<br />
|
||||
<a href="https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team">Contact Details</a>
|
||||
</p>
|
||||
</Trans>
|
||||
}
|
||||
|
||||
return <>
|
||||
{i18n.language != 'en' && <>
|
||||
<p><i>(English version below)</i></p>
|
||||
{content()}
|
||||
<hr />
|
||||
</>}
|
||||
{content('en')}
|
||||
</>
|
||||
}
|
||||
@ -1,61 +0,0 @@
|
||||
/**
|
||||
* @fileOverview The impressum/privacy policy
|
||||
*/
|
||||
import { faShield } from '@fortawesome/free-solid-svg-icons';
|
||||
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome';
|
||||
import * as React from 'react'
|
||||
|
||||
/** 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.
|
||||
*
|
||||
* Note: Do not translate the Impressum!
|
||||
*/
|
||||
export function PrivacyPolicyPopup ({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>Privacy Policy & Impressum</h2>
|
||||
<p>
|
||||
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.
|
||||
</p>
|
||||
<p>
|
||||
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.
|
||||
</p>
|
||||
<p>Our server is located in Germany.</p>
|
||||
<p>
|
||||
<strong>Contact information:</strong><br />
|
||||
Alexander Bentkamp, Jon Eugster<br />
|
||||
Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br />
|
||||
Universitätsstr. 1<br />
|
||||
40225 Düsseldorf<br />
|
||||
Germany<br />
|
||||
+49 211 81-12173<br />
|
||||
<a href="https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster">Contact Details</a>
|
||||
</p>
|
||||
<h2>Development & Funding</h2>
|
||||
<p>
|
||||
The source code of this Lean game engine
|
||||
is <a href="https://github.com/leanprover-community/lean4game" target="_blank">available on Github</a>.
|
||||
If you experience any problems, please
|
||||
file an <a href="https://github.com/leanprover-community/lean4game/issues" target="_blank">Issue on Github</a> or
|
||||
get directly in contact.
|
||||
</p>
|
||||
<p>
|
||||
The game engine has been developed as part of the
|
||||
project <a href="https://hhu-adam.github.io/" target="_blank">ADAM: Anticipating the Digital
|
||||
Age of Mathematics</a> at
|
||||
Heinrich-Heine-Universität Düsseldorf. It is funded by
|
||||
the <i>Stiftung Innovation in der Hochschullehre</i> as part of project <i>Freiraum 2022</i>.
|
||||
</p>
|
||||
</div>
|
||||
</div>
|
||||
}
|
||||
@ -0,0 +1,88 @@
|
||||
import { Box, Slider } from '@mui/material'
|
||||
import * as React from 'react'
|
||||
import { Trans, useTranslation } from 'react-i18next'
|
||||
import { changedDifficulty, selectDifficulty } from '../../state/progress'
|
||||
import { useSelector } from 'react-redux'
|
||||
import { useContext } from 'react'
|
||||
import { useAppDispatch } from '../../hooks'
|
||||
import { GameIdContext } from '../../state/context'
|
||||
|
||||
/** Pop-up that is displayed when opening the help explaining the game rules.
|
||||
*
|
||||
*/
|
||||
export function RulesPopup () {
|
||||
const { t } = useTranslation()
|
||||
const { gameId } = useContext(GameIdContext)
|
||||
const difficulty = useSelector(selectDifficulty(gameId))
|
||||
const dispatch = useAppDispatch()
|
||||
|
||||
function label(x : number) {
|
||||
return x == 0 ? t("none") : x == 1 ? t("relaxed") : t("regular")
|
||||
}
|
||||
|
||||
return <>
|
||||
<h2>{t("Game Rules")}</h2>
|
||||
|
||||
{/* <span className="difficulty-label">{t("Rules")}
|
||||
<FontAwesomeIcon icon={rulesHelp ? faXmark : faCircleQuestion} className='helpButton' onClick={() => (setRulesHelp(!rulesHelp))}/>
|
||||
</span> */}
|
||||
<Box className="slider-wrapper">
|
||||
<Slider
|
||||
orientation="horizontal"
|
||||
title={t("Game Rules")}
|
||||
min={0} max={2}
|
||||
aria-label={t("Game Rules")}
|
||||
value={difficulty}
|
||||
marks={[
|
||||
{value: 0, label: label(0)},
|
||||
{value: 1, label: label(1)},
|
||||
{value: 2, label: label(2)}
|
||||
]}
|
||||
valueLabelFormat={label}
|
||||
getAriaValueText={label}
|
||||
valueLabelDisplay="off"
|
||||
onChange={(ev, val: number) => {
|
||||
dispatch(changedDifficulty({game: gameId, difficulty: val}))
|
||||
}}
|
||||
/>
|
||||
</Box>
|
||||
<Trans>
|
||||
<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>
|
||||
</Trans>
|
||||
<table>
|
||||
<thead>
|
||||
<tr>
|
||||
<th scope="col"></th>
|
||||
<th scope="col">{t("levels")}</th>
|
||||
<th scope="col">{t("tactics")}</th>
|
||||
</tr>
|
||||
</thead>
|
||||
<tbody>
|
||||
<tr>
|
||||
<th scope="row">{t("regular")}</th>
|
||||
<td>🔐</td>
|
||||
<td>🔐</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<th scope="row">{t("relaxed")}</th>
|
||||
<td>🔓</td>
|
||||
<td>🔐</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<th scope="row">{t("none")}</th>
|
||||
<td>🔓</td>
|
||||
<td>🔓</td>
|
||||
</tr>
|
||||
</tbody>
|
||||
</table>
|
||||
</>
|
||||
}
|
||||
@ -1,60 +0,0 @@
|
||||
/**
|
||||
* @fileOverview
|
||||
*/
|
||||
import * as React from 'react'
|
||||
import { Trans, useTranslation } from 'react-i18next'
|
||||
|
||||
/** 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}) {
|
||||
const { t } = useTranslation()
|
||||
|
||||
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>{t("Game Rules")}</h2>
|
||||
<Trans>
|
||||
<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>
|
||||
</Trans>
|
||||
<table>
|
||||
<thead>
|
||||
<tr>
|
||||
<th scope="col"></th>
|
||||
<th scope="col">{t("levels")}</th>
|
||||
<th scope="col">{t("tactics")}</th>
|
||||
</tr>
|
||||
</thead>
|
||||
<tbody>
|
||||
<tr>
|
||||
<th scope="row">{t("regular")}</th>
|
||||
<td>🔐</td>
|
||||
<td>🔐</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<th scope="row">{t("relaxed")}</th>
|
||||
<td>🔓</td>
|
||||
<td>🔐</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<th scope="row">{t("none")}</th>
|
||||
<td>🔓</td>
|
||||
<td>🔓</td>
|
||||
</tr>
|
||||
</tbody>
|
||||
</table>
|
||||
</div>
|
||||
</div>
|
||||
}
|
||||
@ -0,0 +1,43 @@
|
||||
import * as React from 'react'
|
||||
import { Link, LinkProps } from "react-router-dom"
|
||||
import { Box, CircularProgress } from "@mui/material"
|
||||
import ReactMarkdown from 'react-markdown'
|
||||
import remarkMath from 'remark-math'
|
||||
import rehypeKatex from 'rehype-katex'
|
||||
import rehypeRaw from 'rehype-raw'
|
||||
import 'katex/dist/katex.min.css' // `rehype-katex` does not import the CSS for you
|
||||
import gfm from "remark-gfm"
|
||||
|
||||
/** Simple loading icon */
|
||||
export function LoadingIcon () {
|
||||
return <Box display="flex" alignItems="center" justifyContent="center" sx={{ flex: 1, height: "calc(100vh - 64px)" }}>
|
||||
<CircularProgress />
|
||||
</Box>
|
||||
}
|
||||
|
||||
export interface ButtonProps extends LinkProps {
|
||||
disabled?: boolean
|
||||
inverted?: string // Apparently "inverted" in DOM cannot be `boolean` but must be `inverted`
|
||||
}
|
||||
|
||||
|
||||
/** Our own button class */
|
||||
export function Button(props: ButtonProps) {
|
||||
if (props.disabled) {
|
||||
return <span className={`btn btn-disabled ${props.inverted === "true" ? 'btn-inverted' : ''}`} {...props}>{props.children}</span>
|
||||
} else {
|
||||
return <Link className={`btn ${props.inverted === "true" ? 'btn-inverted' : ''}`} {...props}>{props.children}</Link>
|
||||
}
|
||||
}
|
||||
|
||||
/** Spiced-up markdown */
|
||||
export function Markdown(props) {
|
||||
const newProps = {
|
||||
...props,
|
||||
remarkPlugins: [...props.remarkPlugins ?? [], remarkMath, gfm],
|
||||
rehypePlugins: [...props.remarkPlugins ?? [], rehypeKatex, rehypeRaw],
|
||||
};
|
||||
return (
|
||||
<ReactMarkdown {...newProps} className="markdown" />
|
||||
);
|
||||
}
|
||||
@ -1,151 +0,0 @@
|
||||
import * as React from 'react'
|
||||
import { useEffect } from 'react'
|
||||
import Split from 'react-split'
|
||||
import { Box, CircularProgress } from '@mui/material'
|
||||
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
|
||||
import { faArrowRight } from '@fortawesome/free-solid-svg-icons'
|
||||
|
||||
import { GameIdContext } from '../app'
|
||||
import { useAppDispatch, useAppSelector } from '../hooks'
|
||||
import { changedOpenedIntro, selectOpenedIntro } from '../state/progress'
|
||||
import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api'
|
||||
import { Button } from './button'
|
||||
import { PreferencesContext } from './infoview/context'
|
||||
import { InventoryPanel } from './inventory'
|
||||
import { ErasePopup } from './popup/erase'
|
||||
import { InfoPopup } from './popup/game_info'
|
||||
import { PrivacyPolicyPopup } from './popup/privacy_policy'
|
||||
import { RulesHelpPopup } from './popup/rules_help'
|
||||
import { UploadPopup } from './popup/upload'
|
||||
import { PreferencesPopup} from "./popup/preferences"
|
||||
import { WorldTreePanel } from './world_tree'
|
||||
|
||||
import '../css/welcome.css'
|
||||
import { WelcomeAppBar } from './app_bar'
|
||||
import { Hint } from './hints'
|
||||
import i18next from 'i18next'
|
||||
import { useTranslation } from 'react-i18next'
|
||||
|
||||
|
||||
/** the panel showing the game's introduction text */
|
||||
function IntroductionPanel({introduction, setPageNumber}: {introduction: string, setPageNumber}) {
|
||||
const {mobile} = React.useContext(PreferencesContext)
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
|
||||
let { t } = useTranslation()
|
||||
|
||||
const dispatch = useAppDispatch()
|
||||
|
||||
// TODO: I left the setup for splitting up the introduction in place, but if it's not needed
|
||||
// then this can be simplified.
|
||||
|
||||
// let text: Array<string> = introduction.split(/\n(\s*\n)+/)
|
||||
let text: Array<string> = introduction ? [t(introduction, {ns : gameId})] : []
|
||||
|
||||
return <div className="column chat-panel">
|
||||
<div className="chat">
|
||||
{text?.map(((t, i) =>
|
||||
t.trim() ?
|
||||
<Hint key={`intro-p-${i}`}
|
||||
hint={{text: t, hidden: false, rawText: t, varNames: []}}
|
||||
step={0} selected={null} toggleSelection={undefined} />
|
||||
: <></>
|
||||
))}
|
||||
</div>
|
||||
{mobile &&
|
||||
<div className="button-row">
|
||||
<Button className="btn" to=""
|
||||
title="" onClick={() => {
|
||||
setPageNumber(1);
|
||||
dispatch(changedOpenedIntro({game: gameId, openedIntro: true}))
|
||||
}}>
|
||||
Start <FontAwesomeIcon icon={faArrowRight}/>
|
||||
</Button>
|
||||
</div>
|
||||
}
|
||||
</div>
|
||||
}
|
||||
|
||||
/** main page of the game showing among others the tree of worlds/levels */
|
||||
function Welcome() {
|
||||
const gameId = React.useContext(GameIdContext)
|
||||
|
||||
// Load the namespace of the game
|
||||
i18next.loadNamespaces(gameId)
|
||||
|
||||
const {mobile} = React.useContext(PreferencesContext)
|
||||
const {layout, isSavePreferences, language, setLayout, setIsSavePreferences, setLanguage} = React.useContext(PreferencesContext)
|
||||
|
||||
const gameInfo = useGetGameInfoQuery({game: gameId})
|
||||
const inventory = useLoadInventoryOverviewQuery({game: gameId})
|
||||
|
||||
// For mobile only
|
||||
const openedIntro = useAppSelector(selectOpenedIntro(gameId))
|
||||
const [pageNumber, setPageNumber] = React.useState(openedIntro ? 1 : 0)
|
||||
|
||||
// pop-ups
|
||||
const [eraseMenu, setEraseMenu] = React.useState(false)
|
||||
const [impressum, setImpressum] = React.useState(false)
|
||||
const [info, setInfo] = React.useState(false)
|
||||
const [rulesHelp, setRulesHelp] = React.useState(false)
|
||||
const [uploadMenu, setUploadMenu] = React.useState(false)
|
||||
const [preferencesPopup, setPreferencesPopup] = React.useState(false)
|
||||
|
||||
function closeEraseMenu() {setEraseMenu(false)}
|
||||
function closeImpressum() {setImpressum(false)}
|
||||
function closeInfo() {setInfo(false)}
|
||||
function closeRulesHelp() {setRulesHelp(false)}
|
||||
function closeUploadMenu() {setUploadMenu(false)}
|
||||
function closePreferencesPopup() {setPreferencesPopup(false)}
|
||||
function toggleEraseMenu() {setEraseMenu(!eraseMenu)}
|
||||
function toggleImpressum() {setImpressum(!impressum)}
|
||||
function toggleInfo() {setInfo(!info)}
|
||||
function toggleUploadMenu() {setUploadMenu(!uploadMenu)}
|
||||
function togglePreferencesPopup() {setPreferencesPopup(!preferencesPopup)}
|
||||
|
||||
// set the window title
|
||||
useEffect(() => {
|
||||
if (gameInfo.data?.title) {
|
||||
window.document.title = gameInfo.data.title
|
||||
}
|
||||
}, [gameInfo.data?.title])
|
||||
|
||||
return gameInfo.isLoading ?
|
||||
<Box display="flex" alignItems="center" justifyContent="center" sx={{ height: "calc(100vh - 64px)" }}>
|
||||
<CircularProgress />
|
||||
</Box>
|
||||
: <>
|
||||
<WelcomeAppBar pageNumber={pageNumber} setPageNumber={setPageNumber} gameInfo={gameInfo.data} toggleImpressum={toggleImpressum}
|
||||
toggleEraseMenu={toggleEraseMenu} toggleUploadMenu={toggleUploadMenu}
|
||||
toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>
|
||||
<div className="app-content">
|
||||
{ mobile ?
|
||||
<div className="welcome mobile">
|
||||
{(pageNumber == 0 ?
|
||||
<IntroductionPanel introduction={gameInfo.data?.introduction} setPageNumber={setPageNumber} />
|
||||
: pageNumber == 1 ?
|
||||
<WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
|
||||
rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
|
||||
:
|
||||
<InventoryPanel levelInfo={inventory?.data} />
|
||||
)}
|
||||
</div>
|
||||
:
|
||||
<Split className="welcome" minSize={0} snapOffset={200} sizes={[25, 50, 25]}>
|
||||
<IntroductionPanel introduction={gameInfo.data?.introduction} setPageNumber={setPageNumber} />
|
||||
<WorldTreePanel worlds={gameInfo.data?.worlds} worldSize={gameInfo.data?.worldSize}
|
||||
rulesHelp={rulesHelp} setRulesHelp={setRulesHelp} />
|
||||
<InventoryPanel levelInfo={inventory?.data} />
|
||||
</Split>
|
||||
}
|
||||
</div>
|
||||
{impressum ? <PrivacyPolicyPopup handleClose={closeImpressum} /> : null}
|
||||
{rulesHelp ? <RulesHelpPopup handleClose={closeRulesHelp} /> : null}
|
||||
{eraseMenu? <ErasePopup handleClose={closeEraseMenu}/> : null}
|
||||
{uploadMenu? <UploadPopup handleClose={closeUploadMenu}/> : null}
|
||||
{info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}
|
||||
{preferencesPopup ? <PreferencesPopup handleClose={closePreferencesPopup} /> : null}
|
||||
</>
|
||||
}
|
||||
|
||||
export default Welcome
|
||||
@ -0,0 +1,99 @@
|
||||
.chat {
|
||||
flex: 1;
|
||||
overflow-y: scroll;
|
||||
margin-left: .5em;
|
||||
margin-right: .5em;
|
||||
}
|
||||
|
||||
.chat-panel {
|
||||
padding-top: 0;
|
||||
padding-bottom: 0;
|
||||
overflow: hidden;
|
||||
display: flex;
|
||||
flex-direction: column;
|
||||
|
||||
}
|
||||
|
||||
.button-row {
|
||||
/* width:100%; */
|
||||
/* margin-left: .5em;
|
||||
margin-right: .5em; */
|
||||
min-height: 2.5em;
|
||||
border-top: 0.1em solid #aaa;
|
||||
display: flex;
|
||||
padding-top: .2rem;
|
||||
margin: .5rem;
|
||||
|
||||
}
|
||||
|
||||
.button-row > .btn:not(:last-child), .button-row > .btn-placeholder:not(:last-child) {
|
||||
/* display: block; */
|
||||
margin-right: .2rem;
|
||||
}
|
||||
|
||||
.button-row .btn-placeholder {
|
||||
display: inline-block;
|
||||
flex: 1;
|
||||
margin: 0;
|
||||
}
|
||||
|
||||
.button-row .btn {
|
||||
flex: 1;
|
||||
/* margin-top: 1rem;
|
||||
margin-bottom: 1rem;
|
||||
margin-left: .5rem;
|
||||
margin-right: .5rem; */
|
||||
text-align: center;
|
||||
margin: 0;
|
||||
padding: .5em;
|
||||
}
|
||||
|
||||
|
||||
.message {
|
||||
margin: 10px 0;
|
||||
padding: 5px 10px;
|
||||
border-radius: 3px 3px 3px 3px;
|
||||
}
|
||||
|
||||
.message.information, .message.info, .message.kind-5, .message.kind-3, .message.kind-4 {
|
||||
/* color: #059; */
|
||||
color: #000;
|
||||
background-color: #DDF6FF;
|
||||
}
|
||||
|
||||
.message.warning, .message.kind-2 {
|
||||
color: #9F6000;
|
||||
background-color: #FEEFB3;
|
||||
}
|
||||
|
||||
.message.error, .message.kind-1 {
|
||||
color: #D8000C;
|
||||
background-color: #FFBABA;
|
||||
}
|
||||
|
||||
.message.deleted-hint {
|
||||
background-color: #EEE;
|
||||
color: #777;
|
||||
box-shadow: .0em .0em .5em .2em #EEE;
|
||||
}
|
||||
|
||||
.message.success, , .message.kind-6 {
|
||||
color: #000;
|
||||
background-color: #E5FFDD;
|
||||
}
|
||||
|
||||
.chat .message {
|
||||
margin-left: .5em;
|
||||
margin-right: .5em;
|
||||
overflow-x: auto;
|
||||
}
|
||||
|
||||
.chat .recent {
|
||||
box-shadow: .0em .0em .4em .1em #8cbbe9;
|
||||
}
|
||||
|
||||
.chat .selected {
|
||||
/* border: 3px solid #5191d1; */
|
||||
|
||||
box-shadow: .0em .0em .4em .1em var(--clr-primary);
|
||||
}
|
||||
@ -0,0 +1,27 @@
|
||||
.editor-wrapper {
|
||||
flex: 1;
|
||||
position: relative;
|
||||
}
|
||||
|
||||
.editor-wrapper .editor-split {
|
||||
height: 100%;
|
||||
}
|
||||
|
||||
#editor {
|
||||
height: 400px;
|
||||
}
|
||||
|
||||
#infoview {
|
||||
height: 400px;
|
||||
}
|
||||
|
||||
#infoview iframe {
|
||||
width: 100%;
|
||||
height: 95%; /* TODO: setting this to 100% makes it a few pixels too high... */
|
||||
border: unset;
|
||||
}
|
||||
|
||||
/* .typewriter {
|
||||
background-color: lightpink;
|
||||
min-height: 400px;
|
||||
} */
|
||||
@ -0,0 +1,60 @@
|
||||
#error-page {
|
||||
height: 100vh;
|
||||
background-image: url("/RoboSurprised.png");
|
||||
background-repeat: no-repeat;
|
||||
background-size: contain;
|
||||
background-position: right bottom;
|
||||
}
|
||||
|
||||
/* these colours are matching the ones of `.messages.error` */
|
||||
.error-message{
|
||||
border: 2px solid #D8000C;
|
||||
background-color: #FFBABA;
|
||||
border-radius: 1rem;
|
||||
display: inline-block;
|
||||
margin: 3rem;
|
||||
padding-left: 1rem;
|
||||
padding-right: 1rem;
|
||||
/* color: #D8000C; */
|
||||
position: relative;
|
||||
}
|
||||
|
||||
|
||||
.thought-bubble {
|
||||
border: 2px solid #D8000C;
|
||||
background-color: #FFBABA;
|
||||
position: absolute;
|
||||
display: block;
|
||||
}
|
||||
|
||||
.thought-bubble:nth-of-type(1) {
|
||||
bottom: -3.5rem;
|
||||
left: 1rem;
|
||||
border-radius: 1.2rem;
|
||||
width: 2.4rem;
|
||||
height: 2.4rem;
|
||||
}
|
||||
|
||||
.thought-bubble:nth-of-type(2) {
|
||||
bottom: -6rem;
|
||||
left: 2.5rem;
|
||||
border-radius: 1rem;
|
||||
width: 2rem;
|
||||
height: 2rem;
|
||||
}
|
||||
|
||||
.thought-bubble:nth-of-type(3) {
|
||||
bottom: -7.5rem;
|
||||
left: 4.5rem;
|
||||
border-radius: 0.8rem;
|
||||
width: 1.6rem;
|
||||
height: 1.6rem;
|
||||
}
|
||||
|
||||
.thought-bubble:nth-of-type(4) {
|
||||
bottom: -8.2rem;
|
||||
left: 6.8rem;
|
||||
border-radius: 0.6rem;
|
||||
width: 1.4rem;
|
||||
height: 1.4rem;
|
||||
}
|
||||
@ -0,0 +1,37 @@
|
||||
.app-content {
|
||||
height: 100%;
|
||||
flex: 1;
|
||||
min-height: 0;
|
||||
display: flex;
|
||||
}
|
||||
|
||||
.gutter {
|
||||
background-color: #eee;
|
||||
|
||||
background-repeat: no-repeat;
|
||||
background-position: 50%;
|
||||
}
|
||||
|
||||
.gutter.gutter-vertical {
|
||||
background-image: url('data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAB4AAAAFAQMAAABo7865AAAABlBMVEVHcEzMzMzyAv2sAAAAAXRSTlMAQObYZgAAABBJREFUeF5jOAMEEAIEEFwAn3kMwcB6I2AAAAAASUVORK5CYII=');
|
||||
}
|
||||
|
||||
.gutter.gutter-horizontal {
|
||||
background-image: url('data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAUAAAAeCAYAAADkftS9AAAAIklEQVQoU2M4c+bMfxAGAgYYmwGrIIiDjrELjpo5aiZeMwF+yNnOs5KSvgAAAABJRU5ErkJggg==');
|
||||
}
|
||||
|
||||
|
||||
.column {
|
||||
width: 100%;
|
||||
height: 100%;
|
||||
overflow: auto;
|
||||
position: relative;
|
||||
scroll-behavior: smooth;
|
||||
}
|
||||
|
||||
.slider .column {
|
||||
height: 100%;
|
||||
overflow: auto;
|
||||
position: relative;
|
||||
scroll-behavior: smooth;
|
||||
}
|
||||
@ -0,0 +1,97 @@
|
||||
|
||||
nav {
|
||||
flex: 0;
|
||||
background: var(--clr-primary);
|
||||
display: flex;
|
||||
position: relative;
|
||||
flex-direction: row;
|
||||
justify-content: space-between;
|
||||
align-items: center;
|
||||
padding: 1.1em;
|
||||
filter: drop-shadow(0 0 5px rgba(0,0,0,0.5));
|
||||
z-index: 2;
|
||||
}
|
||||
|
||||
.nav-content {
|
||||
flex: 1;
|
||||
display: flex;
|
||||
}
|
||||
|
||||
.nav-content > div {
|
||||
/* border: 1px solid red; */
|
||||
text-align: center;
|
||||
}
|
||||
|
||||
.nav-title-left, .nav-title-right {
|
||||
flex-grow: 0;
|
||||
flex-shrink: 0;
|
||||
display: flex;
|
||||
align-items: center;
|
||||
}
|
||||
|
||||
.nav-title-middle {
|
||||
flex-grow: 1;
|
||||
flex-shrink: 1;
|
||||
margin-left: .5rem;
|
||||
margin-right: .5rem;
|
||||
}
|
||||
|
||||
.nav-title {
|
||||
color: white;
|
||||
font-weight: 500;
|
||||
font-size: 1.3rem;
|
||||
display: inline-block;
|
||||
margin: 0;
|
||||
/* margin: 0 1em; */
|
||||
}
|
||||
|
||||
/* fix to make toggle buttons work */
|
||||
.svg-inline--fa {
|
||||
width: 1em;
|
||||
}
|
||||
|
||||
/* TODO */
|
||||
.nav-button:not(.btn-inverted) {
|
||||
font-size: 1.3rem;
|
||||
}
|
||||
|
||||
.dropdown {
|
||||
z-index: 10;
|
||||
}
|
||||
|
||||
.dropdown {
|
||||
position: absolute;
|
||||
display: flex;
|
||||
flex-direction: column;
|
||||
right: 0;
|
||||
top: 100%;
|
||||
background-color: #fff;
|
||||
z-index: 5;
|
||||
border-top: 1px solid rgba(0, 0, 0, 0.1);
|
||||
border-bottom: 1px solid rgba(0, 0, 0, 0.1);
|
||||
box-shadow: -.1rem .3rem .3rem 0 rgba(0, 0, 0, 0.1);
|
||||
}
|
||||
|
||||
.dropdown .svg-inline--fa {
|
||||
width: 1.8rem;
|
||||
}
|
||||
|
||||
.btn-right {
|
||||
float: right;
|
||||
margin: 0.2rem;
|
||||
}
|
||||
|
||||
.btn-input-mode {
|
||||
position: absolute;
|
||||
right: 0.4rem;
|
||||
z-index: 5;
|
||||
top: 0.4rem;
|
||||
margin: 0;
|
||||
border: 1px solid var(--clr-primary);
|
||||
background-color: #eee;
|
||||
font-size: .7rem;
|
||||
/* box-shadow: .0em .0em .4em .1em var(--clr-primary); */
|
||||
/* box-shadow: -.1rem .3rem .3rem 0 var(--clr-primary); */
|
||||
/* border-top-right-radius: 0;
|
||||
border-bottom-right-radius: 0; */
|
||||
}
|
||||
@ -0,0 +1,30 @@
|
||||
|
||||
/* For the "Rules" popup. */
|
||||
.slider-wrapper {
|
||||
padding-left: 2rem;
|
||||
padding-right: 2rem;
|
||||
padding-top: 1rem;
|
||||
}
|
||||
|
||||
.modal-close {
|
||||
float: right;
|
||||
scale: 2;
|
||||
color: var(--vscode-breadcrumb-foreground);
|
||||
cursor: pointer;
|
||||
}
|
||||
|
||||
.modal-close:hover {
|
||||
float: right;
|
||||
scale: 2;
|
||||
color: var(--vscode-breadcrumb-focusForeground);
|
||||
}
|
||||
|
||||
.modal .nav-button {
|
||||
float: right;
|
||||
font-size: 1.5rem;
|
||||
}
|
||||
|
||||
.settings-buttons .btn {
|
||||
margin-top: 0.2rem;
|
||||
margin-bottom: 0.2rem;
|
||||
}
|
||||
@ -0,0 +1,9 @@
|
||||
# Client
|
||||
|
||||
This document describes features of the frontent/client side.
|
||||
|
||||
|
||||
## URL
|
||||
|
||||
You can add `?lang=de` at the end of the URL to specify the language that should be set. This
|
||||
will change the user's preferred language to the one specified.
|
||||
File diff suppressed because it is too large
Load Diff
@ -1,20 +1,43 @@
|
||||
{
|
||||
"compilerOptions": {
|
||||
"outDir": "./client/dist/",
|
||||
"module": "esnext",
|
||||
"target": "es5",
|
||||
"allowJs": true,
|
||||
"resolveJsonModule": true,
|
||||
"esModuleInterop": true,
|
||||
"moduleResolution": "node",
|
||||
"jsx": "react",
|
||||
"downlevelIteration": true,
|
||||
"experimentalDecorators": true,
|
||||
"allowSyntheticDefaultImports": true,
|
||||
"composite": true,
|
||||
"tsBuildInfoFile": "./node_modules/.tmp/tsconfig.app.tsbuildinfo",
|
||||
"target": "ES2020",
|
||||
|
||||
"useDefineForClassFields": true,
|
||||
"lib": [
|
||||
"ES2021.String",
|
||||
"DOM"
|
||||
]
|
||||
"ES2020.String",
|
||||
"DOM",
|
||||
"DOM.Iterable"
|
||||
],
|
||||
"module": "ESNext",
|
||||
"skipLibCheck": true,
|
||||
|
||||
/* Bundler mode */
|
||||
"moduleResolution": "bundler",
|
||||
"allowImportingTsExtensions": true,
|
||||
"resolveJsonModule": true,
|
||||
"isolatedModules": true,
|
||||
"moduleDetection": "force",
|
||||
"noEmit": true,
|
||||
"jsx": "react-jsx",
|
||||
|
||||
/* Linting */
|
||||
// "strict": true,
|
||||
// "noUnusedLocals": true,
|
||||
// "noUnusedParameters": true,
|
||||
// "noFallthroughCasesInSwitch": true
|
||||
|
||||
// "allowJs": true,
|
||||
// "esModuleInterop": true,
|
||||
// "downlevelIteration": true,
|
||||
// "experimentalDecorators": true,
|
||||
// "allowSyntheticDefaultImports": true,
|
||||
},
|
||||
"exclude": ["server", "relay"]
|
||||
"exclude": [
|
||||
"server",
|
||||
"relay",
|
||||
"node_modules"
|
||||
]
|
||||
}
|
||||
|
||||
Loading…
Reference in New Issue