-
+ return
+ {/*
{svgElements}
-
+ :
}
diff --git a/client/src/config.json b/client/src/config.json
index 70075a68..2067bd5b 100644
--- a/client/src/config.json
+++ b/client/src/config.json
@@ -6,7 +6,6 @@
"trequetrum/lean4game-logic",
"jadabouhawili/knightsandknaves-lean4game"
],
-
"languages": [
{
"iso": "en",
@@ -18,16 +17,16 @@
"flag": "DE",
"name": "Deutsch"
},
- {
- "iso": "zh",
- "flag": "CN",
- "name": "中文"
- },
{
"iso": "es",
"flag": "ES",
"name": "Español"
},
+ {
+ "iso": "zh",
+ "flag": "CN",
+ "name": "中文"
+ },
{
"iso": "ko",
"flag": "KR",
@@ -43,5 +42,6 @@
"flag": "IT",
"name": "Italiano"
}
- ]
+ ],
+ "useFlags": false
}
diff --git a/client/src/css/app.css b/client/src/css/app.css
index 206638df..d1b5ceb3 100644
--- a/client/src/css/app.css
+++ b/client/src/css/app.css
@@ -6,18 +6,25 @@
--clr-light-gray: #ddd;
--clr-dark-gray: #aaa;
--clr-darker-gray: #555;
- --ff-primary: Roboto;
}
/* General styling */
+html, body, #root, .app {
+ height: 100%;
+}
+
body {
- font-family: var(--ff-primary);
+ font-family: "Roboto", sans-serif;
-webkit-font-smoothing: antialiased;
-moz-osx-font-smoothing: grayscale;
}
+.hidden {
+ display: none !important;
+}
+
.markdown code {
color: rgba(0, 32, 90, 0.87);
background-color: rgba(223, 227, 234);
@@ -75,6 +82,7 @@ body {
.btn-disabled, .btn[disabled] {
color: var(--clr-dark-gray);
background: var(--clr-light-gray);
+ cursor: not-allowed;
}
.btn-inverted.btn-disabled, .btn-inverted.btn[disabled] {
@@ -88,16 +96,12 @@ em {
/* App Bar */
-#root {
- height: 100%;
-}
-
.app {
- height: 100%;
display: flex;
flex-direction: column;
}
+/* TODO: remove */
.app-bar {
flex: 0;
background: var(--clr-primary);
@@ -126,14 +130,6 @@ em {
/* margin: 0 1em; */
}
-.app-content {
- height: 100%;
- flex: 1;
- min-height: 0;
- display: flex;
-}
-
-
.markdown li ul, .markdown li ol {
margin:0 1.5em;
}
@@ -142,6 +138,40 @@ em {
margin:0 1.5em 1.5em 1.5em;
}
-.privacy-policy {
- z-index: 10;
+/* TODO: should not be #root */
+#root code {
+ font-family: "JuliaMono", monospace;
+}
+
+@font-face {
+ font-family: 'JuliaMono';
+ src: local('JuliaMono'), url('/fonts/JuliaMono-Regular.ttf') format('truetype');
+}
+
+@font-face {
+ font-family: 'Roboto';
+ src: local('Roboto'), url('/fonts/Roboto-Regular.ttf') format('truetype');
+}
+
+h1 {
+ font-size: 2em;
+ margin: .67em 0;
+}
+
+h2 {
+ font-size: 1.5em;
+}
+
+h3 {
+ font-size: 1.3em;
+}
+
+h4 {
+ font-size: 1.1em;
+ font-style: italic;
+}
+
+h5, h6 {
+ font-size: 1em;
+ font-style: italic;
}
diff --git a/client/src/css/chat.css b/client/src/css/chat.css
new file mode 100644
index 00000000..1d370f4a
--- /dev/null
+++ b/client/src/css/chat.css
@@ -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);
+}
diff --git a/client/src/css/editor.css b/client/src/css/editor.css
new file mode 100644
index 00000000..7c6edc16
--- /dev/null
+++ b/client/src/css/editor.css
@@ -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;
+} */
diff --git a/client/src/css/error_page.css b/client/src/css/error_page.css
new file mode 100644
index 00000000..6650e9ee
--- /dev/null
+++ b/client/src/css/error_page.css
@@ -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;
+}
diff --git a/client/src/css/game.css b/client/src/css/game.css
new file mode 100644
index 00000000..79998649
--- /dev/null
+++ b/client/src/css/game.css
@@ -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;
+}
diff --git a/client/src/css/infoview.css b/client/src/css/infoview.css
index 987a175c..0d9baff6 100644
--- a/client/src/css/infoview.css
+++ b/client/src/css/infoview.css
@@ -1,28 +1,4 @@
-.message {
- margin: 10px 0;
- padding: 5px 10px;
- border-radius: 3px 3px 3px 3px;
-}
-.message.information, .message.info {
- /* color: #059; */
- color: #000;
- background-color: #DDF6FF;
-}
-.message.warning {
- color: #9F6000;
- background-color: #FEEFB3;
-}
-.message.error {
- color: #D8000C;
- background-color: #FFBABA;
-}
-
-.message.deleted-hint {
- background-color: #eee;
- color: #777;
- box-shadow: .0em .0em .5em .2em #eee;
- }
.hyp-group {
margin-bottom: 0.3em;
@@ -50,69 +26,6 @@
}
-.typewriter {
- background: var(--clr-primary);
- padding: 0.5em;
- font-family: var(--ff-primary);
- border-radius: 0.2em;
- /* margin: 0.2em 0 0; */
-}
-
-.typewriter.disabled{
- background: #bbb;
-}
-
-.typewriter.disabled .btn-inverted,
-.typewriter.disabled .mtk1 {
- color: #777;
-}
-
-.typewriter.disabled .typewriter-input-wrapper,
-.typewriter.disabled .monaco-editor,
-.typewriter.disabled .monaco-editor-background,
-.typewriter.disabled .btn-inverted {
- background-color: #eee;
-}
-
-.typewriter form {
- display: flex;
-}
-
-.typewriter button, .undo-button {
- display: block;
- white-space: nowrap;
- flex: 0;
-}
-
-.typewriter .typewriter-input-wrapper{
- min-width: 0;
- flex: 1;
- padding: 0.4em .6em 0;
- font-size: 1rem;
- background: white;
- display: flex;
- flex-direction: column;
-}
-
-.typewriter-interface .proof .MuiCircularProgress-root {
- left: 50%;
- position: relative;
- margin-left: -20px;
- margin-bottom: 0.6em;
-}
-
-.typewriter .typewriter-input {
- flex: 1;
-}
-
-/* Turn off some monaco decorations: */
-.typewriter-input .monaco-editor .view-overlays .current-line {
- border: 0;
-}
-.typewriter-input .monaco-editor .scroll-decoration {
- box-shadow: none;
-}
-
.other-goals .goals-section-title, .other-goals summary, .other-goals summary .font-code {
color: #5191d1;
}
@@ -122,8 +35,8 @@
flex-direction: row;
}
-.goals-section div {
- flex-grow: 1;
+.goal-tabs {
+ width: 100%;
}
#current-proof, #main-assumptions {
@@ -167,22 +80,12 @@
}
-/* Push the goals to the bottom for now, until we insert the proof history above. */
-.typewriter-interface .content {
- display: flex;
- flex-direction: column;
- scroll-behavior: smooth;
-}
/* TODO this is in the wrong file */
.chat {
scroll-behavior: smooth;
}
-.typewriter-interface .content .tmp-pusher {
- flex: 1;
-}
-
.exercise .command {
background-color: #bbb;
padding: .5em;
@@ -210,8 +113,8 @@
.exercise .command-text {
flex: 1;
background-color: #fff;
- font-family: "Droid Sans Mono", "monospace", monospace;
font-size: 14px;
+ font-family: "JuliaMono", monospace;
padding: 0.4em .6em 0;
}
@@ -225,3 +128,43 @@
padding-left: .5em;
padding-right: .5em;
}
+
+/* Apparently this prevents the layout from jumping around when hovering over expressions. */
+.tooltip-arrow {
+ display: none;
+}
+
+
+.goal-tab {
+ /* border: 2px dotted darkgreen; */
+ padding: .2rem;
+ display: flex;
+ flex-direction: row;
+ font-family: "JuliaMono", monospace;
+}
+
+.goal-tab .hyp-group-title {
+ font-family: "Roboto", sans-serif;
+}
+
+.goal-tab .goal, .goal-tab .hypotheses {
+ /* border: 1px solid lightblue; */
+ display: inline-block;
+ flex: 1;
+ display: flex;
+ flex-direction: column;
+ justify-content: center;
+}
+
+.goal-sign {
+ /* border: 1px solid lightblue; */
+ width: 1rem;
+ margin-left: .5rem;
+ margin-right: .5rem;
+ display: inline-block;
+}
+
+.goal-sign line {
+ stroke: var(--clr-dark-gray);
+ stroke-width: 2;
+}
diff --git a/client/src/css/inventory.css b/client/src/css/inventory.css
index fb6fb0f0..f515b135 100644
--- a/client/src/css/inventory.css
+++ b/client/src/css/inventory.css
@@ -10,6 +10,7 @@
.documentation h1 {
font-weight: 900;
+ font-family: "JuliaMono", monospace;
}
.documentation.hidden {
@@ -33,9 +34,15 @@
position: relative;
}
+.inventory .item, .inventory .tab-bar:not(.major) .tab {
+ font-family: "JuliaMono", monospace;
+ font-size: .9rem;
+}
+
.inventory .item.locked {
border: solid 1px #ccc;
color: #ccc;
+ background-color: #f2f2f2;
}
.inventory .item.disabled {
@@ -46,13 +53,21 @@
background-color: rgb(255, 242, 190);
}
-.inventory .item:not(.locked), .inventory .item.enabled {
+.inventory .item.current-world {
+ background-color: rgb(250, 231, 255);
+}
+
+.inventory .item.recent {
+ background-color: rgb(242, 190, 255);
+}
+
+.inventory .item, .inventory .item.enabled {
cursor: pointer;
}
.tab-bar {
border-bottom: 0.1em solid var(--clr-dark-gray);
- margin-bottom: 0.5em;
+ margin-bottom: 1em;
}
.tab {
@@ -67,11 +82,43 @@
display: inline-block;
}
+.tab-bar.major {
+ display: flex;
+ flex-direction: row;
+ flex-wrap: wrap;
+ padding-top: .5em;
+ font-weight: bold;
+}
+
+.tab-bar.major .tab {
+ flex: 1;
+ text-align: center;
+ font-size: 1.2em;
+ padding-left: 0;
+ padding-right: 0;
+}
+
.tab-bar.current .tab.active {
color: black;
border-bottom: 0.3em solid var(--clr-primary);
}
+.inventory .tab.recent {
+ background-image: linear-gradient(to bottom, rgba(255,0,0,0), rgb(242, 190, 255));
+}
+
+.inventory .tab.recent:not(.active) {
+ border-bottom: 0.3em solid rgb(242, 190, 255);
+}
+
+.inventory .tab.new {
+ background-image: linear-gradient(to bottom, rgba(255,0,0,0), rgb(255, 242, 190));
+}
+
+.inventory .tab.new:not(.active) {
+ border-bottom: 0.3em solid rgb(255, 242, 190);
+}
+
.tab.active {
color: black;
border-bottom: 0.3em solid #999;
@@ -94,3 +141,13 @@
align-items: end;
text-align: end;
}
+
+.documentation .nav-button {
+ float: right;
+ font-size: 1.5rem;
+}
+
+.documentation .nav-button.lock {
+ float: left;
+ font-size: .7rem;
+}
diff --git a/client/src/css/landing_page.css b/client/src/css/landing_page.css
index 4831c9f2..f1a8b6b8 100644
--- a/client/src/css/landing_page.css
+++ b/client/src/css/landing_page.css
@@ -9,10 +9,6 @@ html {
font-size: 16px;
}
-body {
- font-family: system-ui, -apple-system, "Segoe UI", Roboto, "Helvetica Neue", Arial, "Noto Sans", "Liberation Sans", sans-serif, "Apple Color Emoji", "Segoe UI Emoji", "Segoe UI Symbol", "Noto Color Emoji";
-}
-
a {
text-decoration: none;
}
@@ -165,12 +161,12 @@ header {
font-style: italic;
}
-header nav {
+/* header nav {
display: flex;
justify-content: flex-end;
padding: 8px;
background-color: rgba(0, 133, 162, .7);
-}
+} */
footer {
background-color: rgba(0, 133, 162, 1);
@@ -231,3 +227,7 @@ footer .link {
margin-right: calc(50% - 650px);
}
}
+
+.info .languages span + span {
+ margin-left: .5em;
+}
diff --git a/client/src/css/level.css b/client/src/css/level.css
index d6fbb7ec..3ae80273 100644
--- a/client/src/css/level.css
+++ b/client/src/css/level.css
@@ -5,31 +5,12 @@
/* display: flex; */
}
-.hidden {
- display: none;
-}
-
-.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==');
-}
-
-.inventory-panel, .exercise-panel, .doc-panel, .introduction-panel {
+/* .inventory-panel, .exercise-panel, .doc-panel, .introduction-panel {
height: 100%;
width: 100%;
overflow: auto;
position: relative;
-}
+} */
.infoview {
padding-top: 1em;
@@ -63,11 +44,11 @@
padding-top: 0em;
}
-.exercise {
+/* .exercise {
flex: 1 1 auto;
display: flex;
flex-flow: column;
-}
+} */
.codeview {
flex: 1 1 auto;
@@ -193,70 +174,21 @@ td code {
.exercise {
height: 100%;
-}
-
-.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;
-
-}
-
-.chat-panel .button-row {
- /* width:100%; */
- margin-left: .5em;
- margin-right: .5em;
- min-height: 2.5em;
- border-top: 0.1em solid #aaa;
-}
-
-.chat-panel .btn {
- margin-top: 1rem;
- margin-bottom: 1rem;
- margin-left: .5rem;
- margin-right: .5rem;
-}
-
-/* .exercise-panel {
- display: flex;
- flex-flow: column;
- height: 100%;
-} */
-
-.button-row.mobile {
- margin: .5rem;
- padding-top: .2rem;
-}
-
-.button-row.mobile .btn {
- padding: .5em;
- border-radius: .2em;
width: 100%;
- margin: 0;
- text-align: center;
}
-
-.typewriter-interface {
+.exercise-content {
display: flex;
flex-flow: column;
height: 100%;
+ z-index: 1;
}
.typewriter {
flex: 0 1 auto;
}
-.typewriter-interface .content {
+.exercise-content {
flex: 1 1 auto;
overflow-y: scroll;
padding: 0;
@@ -276,16 +208,7 @@ td code {
margin-top: 10px;
}
-.chat .message {
- margin-left: .5em;
- margin-right: .5em;
-}
-
-.chat .recent {
- box-shadow: .0em .0em .4em .1em #8cbbe9;
-}
-
-.exercise .step.selected .goal-tabs, .chat .selected {
+.exercise .step.selected .goal-tab {
/* border: 3px solid #5191d1; */
box-shadow: .0em .0em .4em .1em var(--clr-primary);
}
@@ -314,7 +237,7 @@ td code {
right: 0;
top: 100%;
background-color: #fff;
- z-index: 1;
+ z-index: 10;
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);
@@ -341,22 +264,31 @@ td code {
justify-content: center;
}
-.typewriter-interface .content, .world-image-container.empty {
+.exercise {
background-color: #eee;
+ position: relative;
}
-.world-image-container {
+.world-image {
+ height: 100%;
+ width: 100%;
+ overflow: hidden;
display: flex;
flex-direction: column;
- min-height: 0px; /* somehow this has a desired affect, but why? */
- overflow: hidden;
+ position: absolute;
+ z-index: 0;
+ /* min-height: 0px;*/ /* somehow this has a desired affect, but why? */
}
-.world-image-container img.contain {
+.world-image img.contain {
+ height: 100%;
+ width: 100%;
object-fit: contain;
+ object-position: top center;
+ pointer-events: none;
}
-.world-image-container.center {
+.world-image.center {
justify-content: center;
}
@@ -366,10 +298,43 @@ td code {
object-fit: cover;
}
-.typewriter-interface .proof {
+.proof {
+ z-index: 2;
background-color: #fff;
}
+.exercise-content .tmp-pusher {
+ flex: 1;
+}
+
+.exercise-content {
+ background: none;
+}
+
+.editor-mode .proof {
+ height: 100%;
+ display: flex;
+ flex-direction: column;
+}
+
+.editor-mode .tmp-pusher {
+ height: 0;
+}
+
+/* Push the goals to the bottom for now, until we insert the proof history above. */
+.exercise-content {
+ display: flex;
+ flex-direction: column;
+ scroll-behavior: smooth;
+}
+
+.exercise-content .proof .MuiCircularProgress-root {
+ left: 50%;
+ position: relative;
+ margin-left: -20px;
+ margin-bottom: 0.6em;
+}
+
.toggle-width {
min-width: 40px;
text-align: center;
@@ -393,3 +358,16 @@ td code {
background: #DDF6FF;
text-align: center;
}
+
+#unicode-input, .lean-abbrev-input {
+ min-width: 0;
+ white-space: pre;
+ flex: 1;
+ /* padding: 0.4em .6em 0; */
+ font-size: var(--vscode-editor-font-size);
+ background-color: white;
+ border: 2px solid orange;
+ display: flex;
+ flex-direction: column;
+ font-family: JuliaMono, monospace;
+}
diff --git a/client/src/css/navigation.css b/client/src/css/navigation.css
new file mode 100644
index 00000000..00b570e4
--- /dev/null
+++ b/client/src/css/navigation.css
@@ -0,0 +1,213 @@
+
+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: 10;
+}
+
+.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: 10;
+ 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: 3;
+ 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; */
+}
+
+.mobile-nav .svg-inline--fa {
+ margin-left: 0.3rem;
+ margin-right: 0.3rem;
+}
+
+.modal-wrapper {
+ z-index: 10;
+}
+
+.modal hr {
+ margin-top: 3rem;
+ margin-bottom: 3rem;
+ border-color: var(--vscode-breadcrumb-foreground);
+}
+
+/* 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;
+}
+
+.modal-wrapper {
+ position: fixed;
+ top: 0;
+ right: 0;
+ bottom: 0;
+ left: 0;
+ padding: 0;
+}
+
+.modal-backdrop {
+ position: fixed;
+ top: 0;
+ right: 0;
+ bottom: 0;
+ left: 0;
+ background: rgba(0, 0, 0, 0.25);
+ z-index: 6;
+}
+
+.modal h2 {
+ text-align: center;
+}
+
+.modal {
+ position: absolute;
+ top: 50%;
+ left: 50%;
+ transform: translate(-50%, -50%);
+ min-width: max(50%, 300px);
+ max-width: 60ch;
+ max-height: 80%;
+ overflow: scroll;
+ background: #fff;
+ z-index: 7;
+ padding: 2em;
+ border-radius: 1em;
+ text-align: left;
+ color: var(--vscode-breadcrumb-foreground);
+}
+
+.modal input[type="text"] {
+ width: 100%;
+}
+
+.modal .form-error {
+ color: #a00;
+ font-weight: bold;
+}
+
+.modal input[type="submit"] {
+ border: none;
+ color: var(--vscode-button-foreground);
+ background: var(--vscode-button-background);
+ cursor: pointer;
+ padding: .5em 1em;
+ border-radius: .2em;
+ display: block;
+ margin: 1em auto;
+}
+
+.modal table {
+ width: 100%;
+}
+
+.modal a.download-link {
+ cursor: pointer;
+ font-style: italic;
+ text-decoration: underline dotted;
+
+}
diff --git a/client/src/css/popup.css b/client/src/css/popup.css
new file mode 100644
index 00000000..e69de29b
diff --git a/client/src/css/typewriter.css b/client/src/css/typewriter.css
new file mode 100644
index 00000000..eed840d7
--- /dev/null
+++ b/client/src/css/typewriter.css
@@ -0,0 +1,55 @@
+.typewriter {
+ background: var(--clr-primary);
+ padding: 0.5em;
+ font-family: var(--ff-primary);
+ border-radius: 0.2em;
+ /* margin: 0.2em 0 0; */
+}
+
+.typewriter.disabled{
+ background: #bbb;
+}
+
+.typewriter.disabled .btn-inverted,
+.typewriter.disabled .mtk1 {
+ color: #777;
+}
+
+.typewriter.disabled .typewriter-input-wrapper,
+.typewriter.disabled .monaco-editor,
+.typewriter.disabled .monaco-editor-background,
+.typewriter.disabled .btn-inverted {
+ background-color: #eee;
+}
+
+.typewriter form {
+ display: flex;
+}
+
+.typewriter button, .undo-button {
+ display: block;
+ white-space: nowrap;
+ flex: 0;
+}
+
+.typewriter .typewriter-input-wrapper{
+ min-width: 0;
+ flex: 1;
+ padding: 0.4em .6em 0;
+ font-size: 1rem;
+ background: white;
+ display: flex;
+ flex-direction: column;
+}
+
+.typewriter .typewriter-input {
+ flex: 1;
+}
+
+/* Turn off some monaco decorations: */
+.typewriter-input .monaco-editor .view-overlays .current-line {
+ border: 0;
+}
+.typewriter-input .monaco-editor .scroll-decoration {
+ box-shadow: none;
+}
diff --git a/client/src/css/welcome.css b/client/src/css/welcome.css
index e48f7d08..e448d7e7 100644
--- a/client/src/css/welcome.css
+++ b/client/src/css/welcome.css
@@ -14,9 +14,6 @@
width: 100%;
}
-.app-content {
- height: 100%
-}
.welcome .column {
height: 100%;
@@ -35,28 +32,6 @@ i {
font-style: italic;
}
-h1 {
- font-size: 2em;
- margin: .67em 0;
-}
-
-h2 {
- font-size: 1.5em;
-}
-
-h3 {
- font-size: 1.3em;
-}
-
-h4 {
- font-size: 1.1em;
- font-style: italic;
-}
-
-h5, h6 {
- font-size: 1em;
- font-style: italic;
-}
/******************/
/* Privacy Button */
@@ -95,99 +70,6 @@ h5, h6 {
right: 1.5px;
}
-/*****************/
-/* Privacy Popup */
-/*****************/
-
-.modal-wrapper {
- position: fixed;
- top: 0;
- right: 0;
- bottom: 0;
- left: 0;
- padding: 0;
-}
-
-.modal-backdrop {
- position: fixed;
- top: 0;
- right: 0;
- bottom: 0;
- left: 0;
- background: rgba(0, 0, 0, 0.25);
- z-index: 2;
-}
-
-.modal h2 {
- text-align: center;
-}
-
-.modal {
- position: absolute;
- top: 50%;
- left: 50%;
- transform: translate(-50%, -50%);
- min-width: max(50%, 300px);
- max-width: 60ch;
- max-height: 80%;
- overflow: scroll;
- background: #fff;
- z-index: 3;
- padding: 2em;
- border-radius: 1em;
- text-align: left;
- color: var(--vscode-breadcrumb-foreground);
-}
-
-.modal input[type="text"] {
- width: 100%;
-}
-
-.modal .form-error {
- color: #a00;
- font-weight: bold;
-}
-
-.modal input[type="submit"] {
- border: none;
- color: var(--vscode-button-foreground);
- background: var(--vscode-button-background);
- cursor: pointer;
- padding: .5em 1em;
- border-radius: .2em;
- display: block;
- margin: 1em auto;
-}
-
-.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 table {
- width: 100%;
-}
-
-.modal a.download-link {
- cursor: pointer;
- font-style: italic;
- text-decoration: underline dotted;
-
-}
-
-.mobile-nav .svg-inline--fa {
- margin-left: 0.3rem;
- margin-right: 0.3rem;
-}
-
.preferences-category.tail-category{
margin-top: 2em;
}
@@ -198,4 +80,4 @@ h5, h6 {
.preferences-item.leave-left-gap{
margin-left: 3em;
-}
\ No newline at end of file
+}
diff --git a/client/src/i18n.ts b/client/src/i18n.ts
index a2db8a82..faf8d0a3 100644
--- a/client/src/i18n.ts
+++ b/client/src/i18n.ts
@@ -11,7 +11,8 @@ i18n
// > see https://github.com/i18next/i18next-http-backend
loadPath: function(lngs, namespaces: Array
) {
if (namespaces[0].startsWith("g/")) {
- return '/i18n/{{ns}}/{{lng}}/Game.json';
+ // return '/i18n/{{ns}}/{{lng}}/Game.json';
+ return '/i18n/{{ns}}/{{lng}}/Game.po';
} else {
return '/locales/{{lng}}/{{ns}}.json';
}
diff --git a/client/src/index.tsx b/client/src/index.tsx
index f91f3776..016ae7ac 100644
--- a/client/src/index.tsx
+++ b/client/src/index.tsx
@@ -6,33 +6,30 @@ import { Provider } from 'react-redux'
import type { RouteObject } from "react-router"
import { createHashRouter, RouterProvider, Route, redirect } from "react-router-dom"
import ErrorPage from './components/error_page'
-import Welcome from './components/welcome'
import LandingPage from './components/landing_page'
-import Level from './components/level'
-import './i18n';
+import './i18n'
+import Game from './components/game'
// If `VITE_LEAN4GAME_SINGLE` is set to true, then `/` should be redirected to
// `/g/local/game`. This is used for the devcontainer setup
let single_game = (import.meta.env.VITE_LEAN4GAME_SINGLE == "true")
-let root_object: RouteObject = single_game ? {
- path: "/",
- loader: () => redirect("/g/local/game")
-} : {
- path: "/",
- element:
-);
+)
diff --git a/client/src/state/api.ts b/client/src/state/api.ts
index 1a645978..8b9ef4b5 100644
--- a/client/src/state/api.ts
+++ b/client/src/state/api.ts
@@ -36,6 +36,9 @@ export interface InventoryTile {
new: boolean,
hidden: boolean
altTitle: string,
+ world : string|null,
+ level : number|null,
+ proven : boolean
}
export interface LevelInfo {
@@ -44,11 +47,11 @@ export interface LevelInfo {
conclusion: null|string,
index: number,
tactics: InventoryTile[],
- lemmas: InventoryTile[],
+ theorems: InventoryTile[],
definitions: InventoryTile[],
descrText: null|string,
descrFormat: null|string,
- lemmaTab: null|string,
+ theoremTab: null|string,
statementName: null|string,
displayName: null|string,
template: null|string,
@@ -58,9 +61,9 @@ export interface LevelInfo {
/** Used to display the inventory on the welcome page */
export interface InventoryOverview {
tactics: InventoryTile[],
- lemmas: InventoryTile[],
+ theorems: InventoryTile[],
definitions: InventoryTile[],
- lemmaTab: null,
+ theoremTab: null,
}
interface Doc {
@@ -81,13 +84,19 @@ export const apiSlice = createApi({
query: ({game}) => `${game}/game.json`,
}),
loadLevel: builder.query({
- query: ({game, world, level}) => `${game}/level__${world}__${level}.json`,
+ query: ({game, world, level}) => {
+ if (world && level > 0) {
+ return `${game}/level__${world}__${level}.json`
+ } else {
+ return `${game}/inventory.json`
+ }
+ },
}),
loadInventoryOverview: builder.query({
query: ({game}) => `${game}/inventory.json`,
}),
- loadDoc: builder.query({
- query: ({game, type, name}) => `${game}/doc__${type}__${name}.json`,
+ loadDoc: builder.query({
+ query: ({game, name}) => `${game}/doc__${name}.json`,
}),
}),
})
diff --git a/client/src/components/infoview/context.ts b/client/src/state/context.ts
similarity index 72%
rename from client/src/components/infoview/context.ts
rename to client/src/state/context.ts
index e6dd6ee7..47307374 100644
--- a/client/src/components/infoview/context.ts
+++ b/client/src/state/context.ts
@@ -5,14 +5,25 @@ import * as React from 'react';
import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
import { InteractiveDiagnostic } from '@leanprover/infoview-api';
import { Diagnostic } from 'vscode-languageserver-types'
-import { GameHint, InteractiveGoal, InteractiveTermGoal,InteractiveGoalsWithHints, ProofState } from './rpc_api';
-import { PreferencesState } from '../../state/preferences';
+import { GameHint, InteractiveGoal, InteractiveTermGoal, InteractiveGoalsWithHints, ProofState } from '../components/editor/Defs';
+import { PreferencesState } from './preferences';
+import { LeanMonaco, LeanMonacoEditor } from 'lean4monaco';
+import { RpcSessionAtPos } from 'lean4monaco/dist/vscode-lean4/vscode-lean4/src/infoview';
-export const MonacoEditorContext = React.createContext(
- null as any)
+export const MonacoEditorContext = React.createContext<{
+ leanMonacoEditor: LeanMonacoEditor
+ leanMonaco: LeanMonaco
+ rpcSess: RpcSessionAtPos
+}>(null)
export type InfoStatus = 'updating' | 'error' | 'ready';
+
+export const GameIdContext = React.createContext<{
+ gameId: string,
+ worldId: string|null,
+ levelId: number|null}>({gameId: null, worldId: null, levelId: null});
+
// /** One step of the proof */
// export type ProofStep = {
// /** The command in this step */
@@ -93,36 +104,45 @@ export const PreferencesContext = React.createContext({
setLanguage: () => {},
})
-export const WorldLevelIdContext = React.createContext<{
- worldId : string,
- levelId: number
-}>({
- worldId : null,
- levelId: 0,
-})
-/** Context to keep highlight selected proof step and corresponding chat messages. */
-export const SelectionContext = React.createContext<{
- selectedStep : number,
+export const ChatContext = React.createContext<{
+ selectedStep : number
setSelectedStep: React.Dispatch>
-}>({
- selectedStep : undefined,
- setSelectedStep: () => {}
-})
-
-/** Context for deleted Hints that are visible just a bit after they've been deleted */
-export const DeletedChatContext = React.createContext<{
- deletedChat : GameHint[],
+ deletedChat : GameHint[]
setDeletedChat: React.Dispatch>>
- showHelp : Set,
+ showHelp : Set
setShowHelp: React.Dispatch>>
+ chatRef: React.MutableRefObject
}>({
+ selectedStep : undefined,
+ setSelectedStep: () => {},
deletedChat: undefined,
setDeletedChat: () => {},
showHelp: undefined,
- setShowHelp: () => {}
+ setShowHelp: () => {},
+ chatRef: null
})
+export const PageContext = React.createContext<{
+ typewriterMode: boolean,
+ setTypewriterMode: React.Dispatch>,
+ typewriterInput: string,
+ setTypewriterInput: React.Dispatch>,
+ lockEditorMode: boolean,
+ setLockEditorMode: React.Dispatch>,
+ page: number, /* only for mobile */
+ setPage: React.Dispatch>,
+}>({
+ typewriterMode: true,
+ setTypewriterMode: () => {},
+ typewriterInput: "",
+ setTypewriterInput: () => {},
+ lockEditorMode: false,
+ setLockEditorMode: () => {},
+ page: 0,
+ setPage: () => {}
+});
+
export const InputModeContext = React.createContext<{
typewriterMode: boolean,
setTypewriterMode: React.Dispatch>,
diff --git a/client/src/state/progress.ts b/client/src/state/progress.ts
index c01eca00..617cf250 100644
--- a/client/src/state/progress.ts
+++ b/client/src/state/progress.ts
@@ -19,13 +19,13 @@ interface LevelProgressState {
help: number[], // A set of rows where hidden hints have been displayed
}
interface WorldProgressState {
- [world: string] : {[level: number]: LevelProgressState},
+ [world: string] : {[level: number]: LevelProgressState, readIntro: boolean},
}
export interface GameProgressState {
inventory: string[],
difficulty: number,
- openedIntro: boolean,
+ readIntro: boolean,
data: WorldProgressState,
typewriterMode?: boolean
}
@@ -54,19 +54,24 @@ const initalLevelProgressState: LevelProgressState = {code: "", completed: false
/** Add an empty skeleton with progress for the current game */
function addGameProgress (state: ProgressState, action: PayloadAction<{game: string}>) {
if (!state.games[action.payload.game.toLowerCase()]) {
- state.games[action.payload.game.toLowerCase()] = {inventory: [], openedIntro: true, data: {}, difficulty: DEFAULT_DIFFICULTY}
+ state.games[action.payload.game.toLowerCase()] = {inventory: [], readIntro: false, data: {}, difficulty: DEFAULT_DIFFICULTY}
}
if (!state.games[action.payload.game.toLowerCase()].data) {
state.games[action.payload.game.toLowerCase()].data = {}
}
}
-/** Add an empty skeleton with progress for the current level */
-function addLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
+function addWorldProgress(state: ProgressState, action: PayloadAction<{game: string, world: string}>) {
addGameProgress(state, action)
if (!state.games[action.payload.game.toLowerCase()].data[action.payload.world]) {
- state.games[action.payload.game.toLowerCase()].data[action.payload.world] = {}
+ state.games[action.payload.game.toLowerCase()].data[action.payload.world] = {readIntro: false}
}
+}
+
+/** Add an empty skeleton with progress for the current level */
+function addLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
+ addGameProgress(state, action)
+ addWorldProgress(state, action)
if (!state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level]) {
state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level] = {...initalLevelProgressState}
}
@@ -80,7 +85,7 @@ export const progressSlice = createSlice({
codeEdited(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, code: string}>) {
addLevelProgress(state, action)
state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].code = action.payload.code
- state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].completed = false
+ // state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].completed = false
},
/** TODO: docstring */
changedSelection(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, selections: Selection[]}>) {
@@ -100,11 +105,16 @@ export const progressSlice = createSlice({
},
/** delete all progress for this game */
deleteProgress(state: ProgressState, action: PayloadAction<{game: string}>) {
- state.games[action.payload.game.toLowerCase()] = {inventory: [], data: {}, openedIntro: true, difficulty: DEFAULT_DIFFICULTY}
+ state.games[action.payload.game.toLowerCase()] = {inventory: [], data: {}, readIntro: false, difficulty: DEFAULT_DIFFICULTY}
+ },
+ /** delete progress for this world */
+ deleteWorldProgress(state: ProgressState, action: PayloadAction<{game: string, world: string}>) {
+ // addWorldProgress(state, action)
+ state.games[action.payload.game.toLowerCase()].data[action.payload.world] = {readIntro: false}
},
/** delete progress for this level */
deleteLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
- addLevelProgress(state, action)
+ // addLevelProgress(state, action)
state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level] = initalLevelProgressState
},
/** load progress, e.g. from external import */
@@ -123,9 +133,13 @@ export const progressSlice = createSlice({
state.games[action.payload.game.toLowerCase()].difficulty = action.payload.difficulty
},
/** set the difficulty */
- changedOpenedIntro(state: ProgressState, action: PayloadAction<{game: string, openedIntro: boolean}>) {
- addGameProgress(state, action)
- state.games[action.payload.game.toLowerCase()].openedIntro = action.payload.openedIntro
+ changedReadIntro(state: ProgressState, action: PayloadAction<{game: string, world: string, readIntro: boolean}>) {
+ addWorldProgress(state, action)
+ if (action.payload.world) {
+ state.games[action.payload.game.toLowerCase()].data[action.payload.world].readIntro = action.payload.readIntro
+ } else {
+ state.games[action.payload.game.toLowerCase()].readIntro = action.payload.readIntro
+ }
},
/** set the typewriter mode */
changeTypewriterMode(state: ProgressState, action: PayloadAction<{game: string, typewriterMode: boolean}>) {
@@ -137,79 +151,82 @@ export const progressSlice = createSlice({
/** if the level does not exist, return default values */
export function selectLevel(game: string, world: string, level: number) {
- return (state) =>{
- if (!state.progress.games[game.toLowerCase()]) { return initalLevelProgressState }
- if (!state.progress.games[game.toLowerCase()].data[world]) { return initalLevelProgressState }
- if (!state.progress.games[game.toLowerCase()].data[world][level]) { return initalLevelProgressState }
- return state.progress.games[game.toLowerCase()].data[world][level]
+ return (state) => {
+ if (!state.progress.games[game?.toLowerCase()]) { return initalLevelProgressState }
+ if (!state.progress.games[game?.toLowerCase()]?.data[world]) { return initalLevelProgressState }
+ if (!state.progress.games[game?.toLowerCase()]?.data[world][level]) { return initalLevelProgressState }
+ return state.progress.games[game?.toLowerCase()]?.data[world][level]
}
}
/** return the code of the current level */
export function selectCode(game: string, world: string, level: number) {
return (state) => {
- return selectLevel(game.toLowerCase(), world, level)(state).code
+ return selectLevel(game?.toLowerCase(), world, level)(state).code
}
}
/** return the current inventory */
export function selectInventory(game: string) {
return (state) => {
- if (!state.progress.games[game.toLowerCase()]) { return [] }
- return state.progress.games[game.toLowerCase()].inventory
+ if (!state.progress.games[game?.toLowerCase()]) { return [] }
+ return state.progress.games[game?.toLowerCase()]?.inventory
}
}
/** return the code of the current level */
export function selectHelp(game: string, world: string, level: number) {
return (state) => {
- return selectLevel(game.toLowerCase(), world, level)(state).help
+ return selectLevel(game?.toLowerCase(), world, level)(state).help
}
}
/** return the selections made in the current level */
export function selectSelections(game: string, world: string, level: number) {
return (state) => {
- return selectLevel(game.toLowerCase(), world, level)(state).selections
+ return selectLevel(game?.toLowerCase(), world, level)(state).selections
}
}
/** return whether the current level is clompleted */
export function selectCompleted(game: string, world: string, level: number) {
return (state) => {
- return selectLevel(game.toLowerCase(), world, level)(state).completed
+ return selectLevel(game?.toLowerCase(), world, level)(state).completed
}
}
/** return progress for the current game if it exists */
export function selectProgress(game: string) {
return (state) => {
- return state.progress.games[game.toLowerCase()] ?? null
+ return state.progress.games[game?.toLowerCase()] ?? null
}
}
/** return difficulty for the current game if it exists */
export function selectDifficulty(game: string) {
return (state) => {
- return state.progress.games[game.toLowerCase()]?.difficulty ?? DEFAULT_DIFFICULTY
+ return state.progress.games[game?.toLowerCase()]?.difficulty ?? DEFAULT_DIFFICULTY
}
}
/** return whether the intro has been read */
-export function selectOpenedIntro(game: string) {
+export function selectReadIntro(game: string, worldId: string) {
return (state) => {
- return state.progress.games[game.toLowerCase()]?.openedIntro
+ if (worldId) {
+ return state.progress.games[game?.toLowerCase()]?.data[worldId]?.readIntro
+ }
+ return state.progress.games[game?.toLowerCase()]?.readIntro
}
}
/** return typewriter mode for the current game if it exists */
export function selectTypewriterMode(game: string) {
return (state) => {
- return state.progress.games[game.toLowerCase()]?.typewriterMode ?? true
+ return state.progress.games[game?.toLowerCase()]?.typewriterMode ?? true
}
}
/** Export actions to modify the progress */
export const { changedSelection, codeEdited, levelCompleted, deleteProgress,
- deleteLevelProgress, loadProgress, helpEdited, changedInventory, changedOpenedIntro,
+ deleteLevelProgress, deleteWorldProgress, loadProgress, helpEdited, changedInventory, changedReadIntro,
changedDifficulty, changeTypewriterMode} = progressSlice.actions
diff --git a/cypress.config.ts b/cypress.config.ts
new file mode 100644
index 00000000..e385f84d
--- /dev/null
+++ b/cypress.config.ts
@@ -0,0 +1,13 @@
+import { defineConfig } from "cypress";
+
+// default timeout was 4000.
+// Infoview loading is slow on Windows…
+
+export default defineConfig({
+ defaultCommandTimeout: 40000,
+ e2e: {
+ setupNodeEvents(on, config) {
+ // implement node event listeners here
+ },
+ },
+});
diff --git a/cypress/e2e/spec.cy.ts b/cypress/e2e/spec.cy.ts
new file mode 100644
index 00000000..64ed031c
--- /dev/null
+++ b/cypress/e2e/spec.cy.ts
@@ -0,0 +1,85 @@
+describe('The world selection', () => {
+ it('displays the game title', () => {
+ cy.visit('http://localhost:3000/#/g/test/Test')
+ cy.contains('span.nav-title', 'Test Game').should('exist')
+ })
+
+ it('displays the rules popup', () => {
+ cy.visit('http://localhost:3000/#/g/test/Test')
+ cy.contains('a.nav-button', 'Rules').click()
+ cy.contains('div.modal', 'Game Rules').should('exist')
+ })
+
+ it('displays the world titles', () => {
+ cy.visit('http://localhost:3000/#/g/test/Test')
+ cy.get('p.world-title')
+ .map('textContent')
+ .should('have.members', ['Demo World 1', 'Demo World 2']);
+ })
+
+ it('displays the first world and its first level as selectable', () => {
+ cy.visit('http://localhost:3000/#/g/test/Test')
+ cy.contains('svg.world-selection>a:not(.disabled)', 'Demo World 1').as('world').next('a.level').as('level')
+ cy.get('@world')
+ .should('have.attr', 'href', '#/g/test/Test/world/DemoWorld1/level/0')
+ .and('have.css', 'cursor', 'pointer')
+ cy.get('@level')
+ .should('have.attr', 'href', '#/g/test/Test/world/DemoWorld1/level/0')
+ .and('have.css', 'cursor', 'pointer')
+ })
+
+ it('displays the second world and its first level as disabled', () => {
+ cy.visit('http://localhost:3000/#/g/test/Test')
+ cy.contains('svg.world-selection>a.disabled', 'Demo World 2').as('world').next('a.level.disabled').as('level')
+ cy.get('@world')
+ .should('have.attr', 'href', '#/g/test/Test')
+ .and('have.css', 'cursor', 'default')
+ cy.get('@level')
+ .should('have.attr', 'href', '#/g/test/Test')
+ .and('have.css', 'cursor', 'default')
+ })
+})
+
+describe('The first level', () => {
+ it('can be navigated to from the world selection', () => {
+ cy.visit('http://localhost:3000/#/g/test/Test')
+ cy.contains('p.world-title', 'Demo World 1').click()
+ cy.location().its("hash").should('eq', '#/g/test/Test/world/DemoWorld1/level/0')
+ })
+
+ it('displays world and level title', () => {
+ cy.visit('http://localhost:3000/#/g/test/Test/world/DemoWorld1/level/0')
+ cy.contains('div.nav-content', 'Demo World 1')
+ .children()
+ .map((v) => v.textContent.trim())
+ .should('have.members', ['Demo World 1', 'Introduction', 'Start'])
+ })
+
+ it('displays the inventory tabs', () => {
+ cy.visit('http://localhost:3000/#/g/test/Test/world/DemoWorld1/level/0')
+ cy.get('div.tab')
+ .map((v) => v.textContent.trim())
+ .should('have.members', ['Theorems', 'Tactics', 'Definitions'])
+ })
+
+ it('displays the theorems inventory', () => {
+ cy.visit('http://localhost:3000/#/g/test/Test/world/DemoWorld1/level/0')
+ cy.contains('div.tab', 'Theorems').click()
+ cy.contains('div.inventory-list>div.item', 'demo_statement').click()
+ cy.contains('div.documentation>h1', 'demo_statement').should('exist')
+ cy.get('div.documentation>*>svg.fa-xmark').click()
+ })
+
+ it('displays the tactics inventory', () => {
+ cy.visit('http://localhost:3000/#/g/test/Test/world/DemoWorld1/level/0')
+ cy.contains('div.tab', 'Tactics').click()
+ cy.get('div.inventory-list>div.item')
+ .map((v) => v.textContent.trim())
+ .should('have.members', ['exact', 'rfl', 'rw'])
+ cy.contains('div.inventory-list>div.item', 'exact').click()
+ cy.contains('div.documentation>h1', 'exact').should('exist')
+ cy.get('div.documentation>div.markdown')
+ .contains('exact e closes the main goal if its target type matches that of e.')
+ .should('exist')
+ })
+})
\ No newline at end of file
diff --git a/cypress/support/commands.ts b/cypress/support/commands.ts
new file mode 100644
index 00000000..87c1ab6f
--- /dev/null
+++ b/cypress/support/commands.ts
@@ -0,0 +1,65 @@
+///
+// drag(subject: string, options?: Partial): Chainable
+// dismiss(subject: string, options?: Partial): Chainable
+// visit(originalFn: CommandOriginalFn, url: string, options: Partial): Chainable
+// }
+// }
+// }
+
+type Flatten = T extends Iterable ? Item : never;
+type ArrayIterator = (value: T, index: number, collection: T[]) => TResult;
+
+declare global {
+ namespace Cypress {
+ interface Chainable {
+ map- , K extends keyof Item>(iteratee: K): Chainable
;
+ map- , TResult>(iteratee: ArrayIterator
): Chainable;
+ }
+ }
+}
+
+Cypress.Commands.add('map', { prevSubject: true }, (subject: unknown[], iteratee) => {
+ return cy.wrap(
+ Cypress._.map(subject, iteratee),
+ { log: false }
+ );
+});
+
+Cypress.on('uncaught:exception', (err, runnable) => {
+ // returning false here prevents Cypress from
+ // failing the test
+ return false;
+});
diff --git a/cypress/support/e2e.ts b/cypress/support/e2e.ts
new file mode 100644
index 00000000..f80f74f8
--- /dev/null
+++ b/cypress/support/e2e.ts
@@ -0,0 +1,20 @@
+// ***********************************************************
+// This example support/e2e.ts is processed and
+// loaded automatically before your test files.
+//
+// This is a great place to put global configuration and
+// behavior that modifies Cypress.
+//
+// You can change the location of this file or turn off
+// automatically serving support files with the
+// 'supportFile' configuration option.
+//
+// You can read more here:
+// https://on.cypress.io/configuration
+// ***********************************************************
+
+// Import commands.js using ES2015 syntax:
+import './commands'
+
+// Alternatively you can use CommonJS syntax:
+// require('./commands')
\ No newline at end of file
diff --git a/cypress/tsconfig.json b/cypress/tsconfig.json
new file mode 100644
index 00000000..a9bfdb97
--- /dev/null
+++ b/cypress/tsconfig.json
@@ -0,0 +1,8 @@
+{
+ "compilerOptions": {
+ "target": "es5",
+ "lib": ["es5", "dom"],
+ "types": ["cypress", "node"]
+ },
+ "include": ["**/*.ts"]
+}
\ No newline at end of file
diff --git a/doc/DOCUMENTATION.md b/doc/DOCUMENTATION.md
index ca4a5c20..55244e47 100644
--- a/doc/DOCUMENTATION.md
+++ b/doc/DOCUMENTATION.md
@@ -5,7 +5,7 @@ The server is made out of two parts, named "relay" and "server".
The former, "relay", is the server which
sets up a socket connection to the client, starts the lean servers to work on files and
relays messages between the lean server and the client. `index.mjs` is the file that needs to
-be run, which is done for example using `pm2` or by calling `npm run start_server` or
+be run, which is done for example using `pm2` or by calling `npm run start:server` or
`npm run production`, see more later.
The latter, "server", is the lean server which has two jobs. For one, it produces the "gameserver"
@@ -46,7 +46,7 @@ This way any changes to files in `client/` or `relay/` will cause the server to
Alternative, you can run `npm run build` followed by the commands
```
-npm run start_client
+npm run start:client
npm run production
```
diff --git a/doc/client.md b/doc/client.md
new file mode 100644
index 00000000..bcf1e3d3
--- /dev/null
+++ b/doc/client.md
@@ -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.
diff --git a/doc/create_game.md b/doc/create_game.md
index 857989d0..18556842 100644
--- a/doc/create_game.md
+++ b/doc/create_game.md
@@ -46,6 +46,22 @@ This game has been developed by me.
MakeGame
```
+### Local notations
+
+**Important**: If you use any local notations in your game, you need to open these
+namespaces manually before `MakeGame` in order to see the notation in the inventory.
+
+For example (using mathlib), write
+
+```
+open BigOperators
+
+MakeGame
+```
+
+in order to see `∑ x in s, f x` instead of `Finset.sum s fun x => f x`.
+
+
## 3. Creating a Level
In this tutorial we first learn about Levels. A game consists of a tree of worlds, each world has
diff --git a/doc/hints.md b/doc/hints.md
index 75e95c09..718a51e0 100644
--- a/doc/hints.md
+++ b/doc/hints.md
@@ -100,6 +100,18 @@ For remote images, simply add:
Lean Game Server
-
@@ -23,13 +18,19 @@ Lean Game Server
Impressum: Contact Details
+ +49 211 81-14690Contact Details
+
+
+ Datenschutzerklärung:
![]({path.join("data",)
+ }
+
+