add submenu for inventory categories

leanprover-community · May 3, 2024 · 5765c78 · 5765c78
1 parent b9112bf
commit 5765c78
Show file tree

Hide file tree

Showing 2 changed files with 34 additions and 11 deletions.
diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx
@@ -24,22 +24,29 @@ export function Inventory({levelInfo, openDoc, lemmaTab, setLemmaTab, enableAll=
   }) {
   const { t } = useTranslation()
 
+  // TODO: this state should be preserved when loading a different level.
+  const [tab, setTab] = useState<"tactic"|"theorem"|"definition">("theorem")
+
+  let newTheorems = levelInfo?.lemmas?.filter(item => item.new).length > 0
+  let newTactics = levelInfo?.tactics?.filter(item => item.new).length > 0
+  let newDefinitions = levelInfo?.definitions?.filter(item => item.new).length > 0
+
   return (
     <div className="inventory">
-    {/* TODO: Click on Tactic: show info
-      TODO: click on paste icon -> paste into command line */}
-      <h2>{t("Tactics")}</h2>
-      {levelInfo?.tactics &&
+      <div className="tab-bar major">
+        <div className={`tab${(tab == "theorem") ? " active": ""}${newTheorems ? " new" : ""}`} onClick={() => { setTab("theorem") }}>{t("Theorems")}</div>
+        <div className={`tab${(tab == "tactic") ? " active": ""}${newTactics ? " new" : ""}`} onClick={() => { setTab("tactic") }}>{t("Tactics")}</div>
+        <div className={`tab${(tab == "definition") ? " active": ""}${newDefinitions ? " new" : ""}`} onClick={() => { setTab("definition") }}>{t("Definitions")}</div>
+      </div>
+      { (tab == "theorem") && levelInfo?.lemmas &&
+        <InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} level={levelInfo} enableAll={enableAll} tab={lemmaTab} setTab={setLemmaTab}/>
+      }
+      { (tab == "tactic") && levelInfo?.tactics &&
         <InventoryList items={levelInfo?.tactics} docType="Tactic" openDoc={openDoc} enableAll={enableAll}/>
       }
-      <h2>{t("Definitions")}</h2>
-      {levelInfo?.definitions &&
+      { (tab == "definition") && levelInfo?.definitions &&
         <InventoryList items={levelInfo?.definitions} docType="Definition" openDoc={openDoc} enableAll={enableAll}/>
       }
-      <h2>{t("Theorems")}</h2>
-      {levelInfo?.lemmas &&
-        <InventoryList items={levelInfo?.lemmas} docType="Lemma" openDoc={openDoc} level={levelInfo} enableAll={enableAll} tab={lemmaTab} setTab={setLemmaTab}/>
-      }
     </div>
   )
 }

diff --git a/client/src/css/inventory.css b/client/src/css/inventory.css
@@ -55,7 +55,7 @@
 
 .tab-bar {
   border-bottom: 0.1em solid var(--clr-dark-gray);
-  margin-bottom: 0.5em;
+  margin-bottom: 1em;
 }
 
 .tab {
@@ -70,6 +70,22 @@
   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);