Jon Eugster
|
19d2ea363a
|
refactor i18next-scanner config
|
2 years ago |
|
Jon Eugster
|
3ac8fdace7
|
mark translations in app-bar
|
2 years ago |
|
Jon Eugster
|
8d0493acb5
|
make preferences work #179
|
2 years ago |
|
Jon Eugster
|
27c661f08f
|
modify generated statement in inventory
|
2 years ago |
|
Jon Eugster
|
b37f050da5
|
Merge pull request #204 from noamraph/patch-1
Update level.css - hide .katex-mathml, to fix scrolling issue
|
2 years ago |
Noam Yorav-Raphael
|
09c81ea43f
|
Update level.css - hide .katex-mathml, to fix scrolling issue
Fixes https://github.com/leanprover-community/lean4game/issues/202
|
2 years ago |
|
Jon Eugster
|
ff12b34295
|
add suspense to wait for loading #179
|
2 years ago |
|
Jon Eugster
|
45bc0468df
|
implement i18next and i18next-scanner
|
2 years ago |
|
Jon Eugster
|
c24efb1377
|
Merge pull request #203 from JiechengZhao/main
add next_i18n
|
2 years ago |
Hydrogenbear
|
830bffaf11
|
Remove gitignore introduced by accidently lake init
|
2 years ago |
|
Jon Eugster
|
a9447a70d4
|
add interface buttons for i18n #179
|
2 years ago |
|
Jon Eugster
|
eaa4eecad2
|
add doc
|
2 years ago |
|
Jon Eugster
|
1828e73b30
|
add preample tactic sequence to Statement
|
2 years ago |
|
Jon Eugster
|
ce9f5c7840
|
fix locked editor mode
|
2 years ago |
|
Hydrogenbear
|
64d7879c32
|
delete accidently lake init
|
2 years ago |
|
Hydrogenbear
|
cb711205a2
|
Add react_i18n
|
2 years ago |
|
Jon Eugster
|
f42829422d
|
delete hidden hints in chat on Retry
|
2 years ago |
|
Jon Eugster
|
ee6741232f
|
add doc
|
2 years ago |
|
Jon Eugster
|
fa4ae5672d
|
bump to v4.6.1
|
2 years ago |
|
Jon Eugster
|
9bc0a3de46
|
add let_intros for better experience with levels about functions
|
2 years ago |
|
Jon Eugster
|
6cdbfbd9cb
|
Revert "DisableTheorem and co. should not warn if doc does not exist"
This reverts commit 381930e547.
|
2 years ago |
|
Jon Eugster
|
f55581a5f2
|
doc
|
2 years ago |
|
Jon Eugster
|
381930e547
|
DisableTheorem and co. should not warn if doc does not exist
|
2 years ago |
|
Jon Eugster
|
e07570181c
|
typo
|
2 years ago |
|
Jon Eugster
|
87689e1c3a
|
dont show 'intermediate goal solved' on error
|
2 years ago |
|
Jon Eugster
|
47297e4194
|
temporary fix to improve message on server crash
|
2 years ago |
|
Jon Eugster
|
f3f077741d
|
fix client breaking if server timed out.
|
2 years ago |
|
Jon Eugster
|
edf1085310
|
fix ts warnings
|
2 years ago |
|
Jon Eugster
|
68f84a3426
|
fix replacement for 2+ variables
|
2 years ago |
|
Jon Eugster
|
217f86ce5e
|
fix allowed keywords that are not tactics
|
2 years ago |
|
Jon Eugster
|
dd60093dfc
|
bump i18n again
|
2 years ago |
|
Jon Eugster
|
85347a54d9
|
bump i18n
|
2 years ago |
|
Jon Eugster
|
3b4afd6e0e
|
update i18n dependency
|
2 years ago |
|
Jon Eugster
|
2c12872a6e
|
npm audit
|
2 years ago |
|
Jon Eugster
|
ad819bf7ff
|
npm package
|
2 years ago |
|
Jon Eugster
|
c0f366abba
|
Merge branch 'dev'
|
2 years ago |
|
Jon Eugster
|
f72ebdf050
|
bump to v4.6.0
|
2 years ago |
|
Jon Eugster
|
af8463ca5d
|
fixes for v4.6.0-rc1
|
2 years ago |
|
Jon Eugster
|
d0a444205a
|
bump to v4.6.0-rc1
|
2 years ago |
|
Jon Eugster
|
1796c76a84
|
remove debugging css
|
2 years ago |
|
Jon Eugster
|
a75a4a81ac
|
add i18n dependency (#179)
|
2 years ago |
|
Jon Eugster
|
45d84103c1
|
bump npm packages
|
2 years ago |
|
Jon Eugster
|
92e9ed38b2
|
add manual trigger to github action
|
2 years ago |
|
Jon Eugster
|
d689c7ec86
|
update npm deps
|
2 years ago |
|
Jon Eugster
|
16c979a6c2
|
bump npm dependencies
|
2 years ago |
|
Jon Eugster
|
2b85386373
|
move Hint tactic back
|
2 years ago |
|
Jon Eugster
|
8008b68fd6
|
cleanup code surrounding hints
|
2 years ago |
|
Jon Eugster
|
2649f985fa
|
plug-in variables in hints client-side
|
2 years ago |
|
Jon Eugster
|
698a88c545
|
Update troubleshoot.md
|
2 years ago |
|
Jon Eugster
|
3775ad98c8
|
level completed message in editor
|
2 years ago |