Commit Graph

749 Commits (a2726ae287ad6e4c0c32f93ceb1208dc7587de04)
 

Author SHA1 Message Date
joneugster 9cd44911a4 strip newlines when switching to typewriter 3 years ago
joneugster 047c5ae268 force editor mode if template present 3 years ago
joneugster 04038a32c8 fix inventory local storage 3 years ago
Jon Eugster 6970f10e30
Merge pull request #116 from leanprover-community/eugster/level-error-msg
fix: show error on duplicated level number
3 years ago
joneugster 165c0e176a typo 3 years ago
joneugster 7563963c34 npm update and landing page update 3 years ago
Jon Eugster 7016173f53 tweak world tree 3 years ago
Jon Eugster 6ce5131c63 open-book icon for closing inventory button on mobile #89 3 years ago
Jon Eugster 0b1fe3baf1 Update DOCUMENTATION.md #111 3 years ago
Jon Eugster b2936e0200 show typewriter input as disabled if non-primary goal is selected 3 years ago
Jon Eugster 24eed37f89 split intro text consistently into bubbles #100 3 years ago
Jon Eugster 3a3471c615 throw error in regular difficulty if tactic not unlocked 3 years ago
Jon Eugster 8730c2067c uniform impressum everywhere #96 3 years ago
Jon Eugster 5257865b47 highlight only goals without command #115 3 years ago
Jon Eugster 9689b8ca53 rename filename to typewriter 3 years ago
Jon Eugster 7b26280ae9 rename commandline to typewriter #107 3 years ago
Jon Eugster c3a36e2cf3 change name from lemma to theorem #108 3 years ago
Jon 6e046d72b6 show error on duplicated level number 3 years ago
Alexander Bentkamp 923a6cfb4f delete outdated local storage 3 years ago
Alexander Bentkamp 2254f594fa repair tooltips 3 years ago
Alexander Bentkamp 972213ec69 hide hidden items everywhere 3 years ago
Alexander Bentkamp c59444aab5 add notes 3 years ago
Alexander Bentkamp 8db364748b fix data undefined issue 3 years ago
Alexander Bentkamp a423681150 fix hidden items 3 years ago
Alexander Bentkamp a445635a99 remove some vulnerable dependencies 3 years ago
Alexander Bentkamp 5c919fb983 Add NewHiddenTactic command
Fixes #109
3 years ago
Alexander Bentkamp 1d49535fcf remove docstring warning if TacticDoc is provided
Fixes https://github.com/hhu-adam/NNG4/issues/21
3 years ago
Jon Eugster c50517b5e6
clicking on level 1 opens the introduction 3 years ago
Alexander Bentkamp f70aab29ed close level immediately when leaving it 3 years ago
Alexander Bentkamp a7dab88747 remove old debug code 3 years ago
Jon Eugster ade2074598 remove unecessary stuff 3 years ago
Jon Eugster b01dd1de6e stuff 3 years ago
Jon Eugster 87cb299b1f bump lean 3 years ago
Jon Eugster 37f2d50e77 add LEAN4GAME_SINGLE_GAME env variable 3 years ago
Jon Eugster 98ea870a43 small fixes 3 years ago
Jon Eugster 22f0bac569 fix 3 years ago
Jon Eugster 9c6ed17113 coulour introduction texts #100 3 years ago
Jon Eugster 4d4d2a59e7 uniform layout for world introduction #94 3 years ago
Jon Eugster 6371f77379 satisfy unused variable linter 3 years ago
Jon Eugster 73b80e714d improve welcome page 3 years ago
Jon Eugster db5cfbc433 new design for welcome page #96 3 years ago
Jon Eugster 42eaedda70 css for loading circle 3 years ago
Jon Eugster 6437013479
bump lean-toolchain
bump toolchain
3 years ago
Scott Morrison a26736aff8 bump toolchain 3 years ago
Jon Eugster 2bc0bb22f3 world size varies with number of levels #95 3 years ago
Jon Eugster 714634fe5a bug where commandline would be hidden 3 years ago
Jon Eugster d7fdd95cab uniform design of toggle buttons #89 3 years ago
Jon Eugster c738695e81 spacing around proof step #92 3 years ago
Jon Eugster eb8fa91319 style old goal states #93 3 years ago
Jon Eugster 88860d277d rename game modes #97 3 years ago