Commit Graph
100 Commits
Author SHA1 Message Date
joneugster 6f92d61381 fix redirect from landing page in dev container #145 2023-11-09 15:26:53 +01:00
joneugster 506677ee02 bump to v4.2.0 2023-11-08 10:36:13 +01:00
joneugster 3d97cff0f4 change to vite 2023-11-08 09:30:59 +01:00
joneugster 918151ade5 npm audit 2023-10-27 14:07:24 +02:00
joneugster c2b5754371 Merge branch 'refactor' 2023-10-27 14:05:25 +02:00
joneugster d1cd0f80fd refactor app_bar 2023-10-27 14:03:25 +02:00
joneugster d52d63020c fix dropdown on safari 2023-10-27 14:00:54 +02:00
joneugster 5c41d5c83c Merge branch 'main' into refactor 2023-10-24 11:39:50 +02:00
joneugster 8e4c993bd7 fix Exercise statement 2023-10-24 09:39:32 +02:00
joneugster 787d010b6c cleanup app_bar.tsx 2023-10-23 21:07:33 +02:00
joneugster e740027144 move css files 2023-10-23 18:07:55 +02:00
joneugster 53e015a2fe cleanup app.tsx 2023-10-23 18:00:42 +02:00
joneugster b70ac78cf7 split Typewriterinterface and catch promise file close error #127 2023-10-22 01:00:47 +02:00
joneugster 853f797157 add comment for rpc bug 2023-10-21 04:20:19 +02:00
joneugster 84ad619537 Improve input and deletion of typewriter #122 2023-10-21 03:16:57 +02:00
joneugster b6bc77828d remove 'Exercise' word #123 2023-10-21 02:21:05 +02:00
joneugster ceee1b38e1 move circular loading 2023-10-21 02:13:44 +02:00
joneugster b5927a1024 Fix assumption display in inventory and editor mode #84 2023-10-20 21:59:47 +02:00
joneugster 2b159f508f move test 2023-10-20 17:59:46 +02:00
joneugster 30f9d46489 check for structural recursion #117 2023-10-19 13:46:44 +02:00
joneugster 5de8ce8be7 fixes of lean bump 2023-10-19 12:10:58 +02:00
joneugster 2de82a1106 fix from lean bump 2023-10-18 14:57:14 +02:00
joneugster ca58cb0e78 typo 2023-10-18 14:56:53 +02:00
joneugster ec96f2c80e bump lean-toolchain 2023-10-18 14:53:42 +02:00
joneugster cafe74a22b add file 2023-10-18 14:49:30 +02:00
joneugster cc4321ff3f Turn some logInfo into trace[debug] to toggle the off for building 2023-10-17 16:01:39 +02:00
joneugster 19592668ae documentation 2023-10-17 02:06:32 +02:00
joneugster 556c072cef NewLemma checks if specified theorem exists and searches for docstrings 2023-10-17 02:05:17 +02:00
joneugster bb0ba83f18 load arbitrary games with tags g/local/FolderName 2023-10-16 21:24:50 +02:00
joneugster 0c65a2e4f1 reorganise popups 2023-10-16 15:20:00 +02:00
joneugster 06aa5d5339 help button explaining Game Rules 2023-10-16 14:59:55 +02:00
joneugster 63a0d8d5f0 typo 2023-10-16 04:30:44 +02:00
joneugster d66546a7f1 fix empty typewriter containing two lines 2023-10-15 03:16:27 +02:00
joneugster caee7195db lean4game.verbose option 2023-10-15 03:15:02 +02:00
joneugster 2b5c42a3c5 insert template when editor empty 2023-10-14 14:53:19 +02:00
joneugster 4ca570e232 landing page html 2023-10-14 14:24:39 +02:00
joneugster ae5413f82e improve world tree 2023-10-13 22:58:08 +02:00
joneugster 60069191dd update doc 2023-10-13 22:57:42 +02:00
joneugster 9cd44911a4 strip newlines when switching to typewriter 2023-10-13 15:51:00 +02:00
joneugster 047c5ae268 force editor mode if template present 2023-10-13 15:51:00 +02:00
joneugster 04038a32c8 fix inventory local storage 2023-10-13 15:51:00 +02:00
Jon Eugster 6970f10e30 Merge pull request #116 from leanprover-community/eugster/level-error-msg
fix: show error on duplicated level number
2023-10-10 10:07:26 +02:00
joneugster 165c0e176a typo 2023-10-09 14:29:49 +02:00
joneugster 7563963c34 npm update and landing page update 2023-10-09 12:29:16 +02:00
Jon Eugster 7016173f53 tweak world tree 2023-10-09 11:23:54 +02:00
Jon Eugster 6ce5131c63 open-book icon for closing inventory button on mobile #89 2023-10-09 11:23:50 +02:00
Jon Eugster 0b1fe3baf1 Update DOCUMENTATION.md #111 2023-10-09 11:23:47 +02:00
Jon Eugster b2936e0200 show typewriter input as disabled if non-primary goal is selected 2023-10-09 11:23:43 +02:00
Jon Eugster 24eed37f89 split intro text consistently into bubbles #100 2023-10-09 11:23:40 +02:00
Jon Eugster 3a3471c615 throw error in regular difficulty if tactic not unlocked 2023-10-09 11:23:37 +02:00
Jon Eugster 8730c2067c uniform impressum everywhere #96 2023-10-09 11:23:34 +02:00
Jon Eugster 5257865b47 highlight only goals without command #115 2023-10-09 11:23:32 +02:00
Jon Eugster 9689b8ca53 rename filename to typewriter 2023-10-09 11:23:29 +02:00
Jon Eugster 7b26280ae9 rename commandline to typewriter #107 2023-10-09 11:23:26 +02:00
Jon Eugster c3a36e2cf3 change name from lemma to theorem #108 2023-10-09 11:23:12 +02:00
Jon Eugster c50517b5e6 clicking on level 1 opens the introduction 2023-09-21 17:39:09 +02:00
Jon Eugster ade2074598 remove unecessary stuff 2023-09-10 21:06:31 +02:00
Jon Eugster b01dd1de6e stuff 2023-09-10 16:15:41 +02:00
Jon Eugster 87cb299b1f bump lean 2023-09-10 14:39:55 +02:00
Jon Eugster 37f2d50e77 add LEAN4GAME_SINGLE_GAME env variable 2023-09-10 14:39:30 +02:00
Jon Eugster 98ea870a43 small fixes 2023-09-01 20:09:49 +02:00
Jon Eugster 22f0bac569 fix 2023-09-01 13:44:58 +02:00
Jon Eugster 9c6ed17113 coulour introduction texts #100 2023-09-01 13:04:22 +02:00
Jon Eugster 4d4d2a59e7 uniform layout for world introduction #94 2023-09-01 12:35:09 +02:00
Jon Eugster 6371f77379 satisfy unused variable linter 2023-09-01 12:11:49 +02:00
Jon Eugster 73b80e714d improve welcome page 2023-09-01 11:52:11 +02:00
Jon Eugster db5cfbc433 new design for welcome page #96 2023-08-31 18:15:15 +02:00
Jon Eugster 42eaedda70 css for loading circle 2023-08-31 14:48:57 +02:00
Jon Eugster 6437013479 bump lean-toolchain
bump toolchain
2023-08-31 13:38:11 +02:00
Jon Eugster 2bc0bb22f3 world size varies with number of levels #95 2023-08-30 17:34:05 +02:00
Jon Eugster 714634fe5a bug where commandline would be hidden 2023-08-30 17:31:49 +02:00
Jon Eugster d7fdd95cab uniform design of toggle buttons #89 2023-08-29 10:15:00 +02:00
Jon Eugster c738695e81 spacing around proof step #92 2023-08-28 12:37:11 +02:00
Jon Eugster eb8fa91319 style old goal states #93 2023-08-28 12:24:05 +02:00
Jon Eugster 88860d277d rename game modes #97 2023-08-28 11:40:01 +02:00
Jon Eugster 50ec616b8e automate lemmaTab #88 2023-08-28 11:33:01 +02:00
Jon Eugster 764ed558e7 move exercise statement #91 2023-08-28 11:16:55 +02:00
Jon Eugster 8be7f2f17b modify client api to include template 2023-08-25 18:06:26 +02:00
Jon Eugster b6ea453084 add Template server-side 2023-08-25 18:04:10 +02:00
Jon Eugster 25f2f08309 fix inventory overview 2023-08-12 12:50:26 +02:00
Jon Eugster 70d30d1212 fix panics due to HashMap.find! 2023-08-12 12:17:22 +02:00
Jon Eugster 735f58be95 small improvements to the client 2023-08-11 18:25:52 +02:00
Jon Eugster adb93e30bd update documentation 2023-08-07 12:54:22 +02:00
Jon Eugster 0b14489911 use docComment for statement description 2023-08-07 01:16:02 +02:00
Jon Eugster 9ef4122e94 add allowed keywords 'by' and 'to' 2023-08-06 23:59:04 +02:00
Jon Eugster cd0417dc36 bump toolchain 2023-08-06 23:59:04 +02:00
Jon Eugster de1bdc1d20 Merge pull request #83 from alexjbest/attr
add attributes and docstring to `Statement`
2023-08-06 23:58:22 +02:00
Jon Eugster a00edfa884 Update DOCUMENTATION.md 2023-08-06 19:33:28 +02:00
Jon Eugster 5072dacf94 fix new items in inventory 2023-08-04 18:37:47 +02:00
Jon Eugster f5eb185eb2 Merge branch 'dev' 2023-08-04 10:30:06 +02:00
Jon Eugster 8cbe9f0ba8 documentation 2023-08-04 10:29:46 +02:00
Jon Eugster 593ca10720 cleanup 2023-08-04 10:29:40 +02:00
Jon Eugster bd8c857539 cleanup level.tsx 2023-08-02 16:58:30 +02:00
Jon Eugster 25055b017b cleanup world_tree 2023-08-02 15:35:32 +02:00
Jon Eugster cd6974b687 rename file 2023-08-02 15:32:07 +02:00
Jon Eugster 61cba63b81 cleanup welcome.tsx 2023-08-02 15:30:27 +02:00
Jon Eugster e429946046 change nav-bar on desktop 2023-08-02 11:02:13 +02:00
Jon Eugster 5e4a959c8a move next-level-buttons on mobile 2023-07-29 16:41:59 +02:00
Jon Eugster 1ce68fe7fe fix end-of-level-buttons for mobile 2023-07-29 15:01:46 +02:00
Jon Eugster e23a4bec64 mobile store if game intro has been read 2023-07-29 14:39:36 +02:00