Jon Eugster
f0171797f3
typo
2023-02-02 14:59:23 +01:00
Jon Eugster
72d65824b1
Merge branch 'main' of github.com:leanprover-community/lean4game
2023-02-02 14:45:48 +01:00
Jon Eugster
404f346920
set theory levels
2023-02-02 14:44:58 +01:00
Alexander Bentkamp
41cc23543b
fix command line bug
2023-02-02 09:35:03 +01:00
Alexander Bentkamp
73a44bd057
disable undo button
2023-01-30 15:30:48 +01:00
Alexander Bentkamp
5025fa939b
show line numbers only in editor mode
2023-01-30 15:18:06 +01:00
Alexander Bentkamp
45f88cf5a8
undo button
2023-01-30 15:15:39 +01:00
Alexander Bentkamp
fbdc1afe34
hide command line properly
2023-01-30 13:18:02 +01:00
Alexander Bentkamp
f73dac8353
prettier command line
2023-01-30 12:28:25 +01:00
Alexander Bentkamp
48de58416d
editor mode
2023-01-30 12:00:33 +01:00
Alexander Bentkamp
e2ea6fa85e
resizable panels
2023-01-30 11:19:33 +01:00
Alexander Bentkamp
2774fab98c
replace mui buttons, move them into bar
2023-01-27 17:28:32 +01:00
Alexander Bentkamp
8c83e802e9
center loading icon
2023-01-27 16:39:00 +01:00
Alexander Bentkamp
6d567a696f
add command line #26
2023-01-27 12:14:08 +01:00
Alexander Bentkamp
450f32a56b
disable quickSuggestions
...
Fixes #10
2023-01-26 16:28:08 +01:00
Alexander Bentkamp
221927942f
fix semantic highlighting
...
Fixes #29
2023-01-26 16:19:56 +01:00
Alexander Bentkamp
fdbd962742
set_option tactic.hygienic false
...
Fixes #28
2023-01-26 12:17:26 +01:00
Alexander Bentkamp
f82c310557
check when level is completed
...
fixes #27
2023-01-26 12:06:13 +01:00
Alexander Bentkamp
5578359742
remove old files
2023-01-26 11:33:36 +01:00
Alexander Bentkamp
fda1a0ef08
use our custom unfoldSnaps instead of unfoldCmdSnaps
2023-01-26 11:10:57 +01:00
Alexander Bentkamp
e930bbb8af
show unsolved goals message, but without the goals
2023-01-25 17:25:12 +01:00
Alexander Bentkamp
cda4e5b859
Hide "unsolved goals" messages
2023-01-25 16:36:21 +01:00
Alexander Bentkamp
5bfae3a1c2
show other goals only for more than 1 goal
2023-01-25 16:22:45 +01:00
Alexander Bentkamp
e3c67a06b8
fix error
2023-01-25 16:19:41 +01:00
Alexander Bentkamp
a2c9645144
prettier goal display
2023-01-25 14:57:34 +01:00
Alexander Bentkamp
313e44a16d
split into main goal and other goals
2023-01-25 14:45:07 +01:00
Alexander Bentkamp
3e4a687bd1
prettier goal view
2023-01-25 13:51:00 +01:00
Alexander Bentkamp
ba3b65b7db
use css for svg styling
2023-01-25 13:47:44 +01:00
Alexander Bentkamp
026679e541
fix: kill docker when socket gets closed
2023-01-25 13:20:49 +01:00
Alexander Bentkamp
ab3a0df9af
update lean4web
2023-01-25 11:54:57 +01:00
Alexander Bentkamp
1d2b12eb5f
fix error
2023-01-25 11:32:00 +01:00
Alexander Bentkamp
3d349f9a6b
reintroduce infoProvider.dispose();
...
We need to find another solution to avoid the unsubscribe error
2023-01-25 11:30:26 +01:00
Alexander Bentkamp
6c9ba14fd2
Split assumptions and objects
...
Fixes #9
Fixes #24
2023-01-25 11:29:40 +01:00
Alexander Bentkamp
ca366d4bde
custom interactive goal data types
2023-01-25 11:00:36 +01:00
Alexander Bentkamp
09aae16693
Add loading indicators in infoview
2023-01-25 10:22:03 +01:00
Alexander Bentkamp
59c33d2423
remove custom getDiagnostics
2023-01-25 10:15:29 +01:00
Alexander Bentkamp
126bfa051a
prettier hints
2023-01-25 10:07:22 +01:00
Alexander Bentkamp
f4ac6ef7fb
remove infoprovider.dispose()
...
The issue is that this removes the server notification subscriptions and then we get an error because react executes the cleanup of child components only after cleanup of parent components
2023-01-24 17:17:25 +01:00
Jon Eugster
f2dc99ff35
levels.
2023-01-24 16:54:28 +01:00
Alexander Bentkamp
8c4b995a32
rename message to hint
2023-01-24 16:37:18 +01:00
Jon Eugster
ecc9a488a2
typo
2023-01-24 16:00:15 +01:00
Jon Eugster
d4c3d90e9b
level names
2023-01-24 15:46:14 +01:00
Jon Eugster
6576aa0231
levels.
2023-01-24 15:11:24 +01:00
Jon Eugster
eff64d9713
Merge branch 'main' of github.com:leanprover-community/lean4game
2023-01-24 14:54:39 +01:00
Jon Eugster
96ec872f49
levels.
2023-01-24 14:54:36 +01:00
Alexander Bentkamp
b7cc5aaf57
show hints
2023-01-24 14:09:34 +01:00
Alexander Bentkamp
8175d32a3c
custom getInteractiveGoals RPC
2023-01-24 12:15:47 +01:00
Alexander Bentkamp
1aba4162e4
integrate infoview into react component tree
2023-01-24 11:22:43 +01:00
Alexander Bentkamp
32bacf8b7c
move renderInfoview function
2023-01-24 11:03:02 +01:00
Alexander Bentkamp
45bdc22600
show all messages, independent of cursor position
2023-01-24 10:50:51 +01:00