bring back colors

imldresden · Oct 30, 2024 · 34ef07d · 34ef07d
1 parent a16e123
commit 34ef07d
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/frontend/public/js/main/main.js b/frontend/public/js/main/main.js
@@ -96,8 +96,10 @@ function createConceptDropdowns(concepts) {
       concept.value = k;
       concept.innerHTML = concepts[k].short;
       if (concepts[k].rhs && concepts[k].rhs.length > 0) {
+        concept.classList.add('option-rhs-true');
         toProof.appendChild(concept);
       } else {
+        concept.classList.add('option-rhs-false');
         toCE.appendChild(concept);
       }
     }
@@ -127,9 +129,11 @@ function createConceptDropdowns(concepts) {
       rhsC.innerHTML = concepts[rhsKey].short;
       if (ccs.has(rhsKey)) {
         rhsC.type = "pr";
+        rhsC.classList.add('option-rhs-true');
         toProof.appendChild(rhsC);
       } else {
         rhsC.type = "ce";
+        rhsC.classList.add('option-rhs-false');
         toCE.appendChild(rhsC);
       }
     });

diff --git a/frontend/public/style/widgets/general.css b/frontend/public/style/widgets/general.css
@@ -430,4 +430,12 @@ span.badge.new {
 
 .wide-row {
 	width: 55%;
+}
+
+.option-rhs-true {
+	background-color: var(--color-teal-light);
+}
+
+.option-rhs-false {
+	background-color: var(--color-orange-light);
 }