move everything

This commit is contained in:
Joeri Exelmans 2025-05-23 22:35:47 +02:00
parent 3ff7e76694
commit 9050581a10
25 changed files with 37 additions and 42 deletions

View file

@ -1,56 +0,0 @@
.editor {
padding: 2px;;
}
.editor.error {
border: 1px solid red;
display: inline-block;
}
.editor.unknown {
border: 1px dashed dodgerblue;
display: inline-block;
}
*:hover:not(:has(> *:hover)) {
/* useful for debugging: */
/* border-width: 2px !important; */
}
.offending .error {
background-color: transparent;
}
.typeSignature {
display: inline-block;
/* z-index: 1; */
position: relative;
}
.typeSignature.gotDebug {
background-color: gold;
padding: 2px;
}
.typeDebug {
display: none;
}
.typeSignature:hover > .typeDebug {
display: inline-block;
position: absolute;
white-space-collapse: preserve;
width: max-content;
background-color: #d2ebf1e0;
color: black;
font-family: var(--my-monospace-font);
padding: 4px;
z-index: 1000;
}
.editor:hover > .typeSignature {
display: inline-block;
}
.keyword {
color: blue;
font-weight: bold;
}