doc panel

client/src/components/Inventory.tsx

@@ -6,17 +6,14 @@ import { faLock, faLockOpen, faBook, faHammer, faBan } from '@fortawesome/free-s
 import Markdown from './Markdown';
 import { useLoadDocQuery, ComputedInventoryItem } from '../state/api';
 
-function Inventory({ tactics, lemmas, definitions } :
+export function Inventory({ tactics, lemmas, definitions, setInventoryDoc } :
   {lemmas: ComputedInventoryItem[],
   tactics: ComputedInventoryItem[],
-  definitions: ComputedInventoryItem[]}) {
-
-  const [docName, setDocName] = useState(null)
-  const [docType, setDocType] = useState(null)
+  definitions: ComputedInventoryItem[],
+  setInventoryDoc: (inventoryDoc: {name: string, type: string}) => void}) {
 
   function openDoc(name, type) {
-    setDocName(name)
-    setDocType(type)
+    setInventoryDoc({name, type})
   }
 
   return (
@@ -31,8 +28,6 @@ function Inventory({ tactics, lemmas, definitions } :
 
       <h2>Lemmas</h2>
       <InventoryList items={lemmas} docType="Lemma" openDoc={openDoc} />
-
-      {docName && <Documentation name={docName} type={docType} />}
     </div>
   )
 }
@@ -81,7 +76,7 @@ function InventoryItem({name, locked, disabled, showDoc}) {
   return <div className={`item ${className}`} onClick={handleClick}>{icon} {name}</div>
 }
 
-function Documentation({name, type}) {
+export function Documentation({name, type}) {
 
   const doc = useLoadDocQuery({type: type, name: name})
 
@@ -90,5 +85,3 @@ function Documentation({name, type}) {
     <Markdown>{doc.data?.text}</Markdown>
   </>
 }
-
-export default Inventory;

client/src/components/Level.tsx

@@ -9,7 +9,7 @@ import { Link, useParams } from 'react-router-dom';
 import { Box, CircularProgress, FormControlLabel, FormGroup, Switch, IconButton } from '@mui/material';
 import MuiDrawer from '@mui/material/Drawer';
 import Grid from '@mui/material/Unstable_Grid2';
-import Inventory from './Inventory';
+import {Inventory, Documentation} from './Inventory';
 import { LeanTaskGutter } from 'lean4web/client/src/editor/taskgutter';
 import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider';
 import 'lean4web/client/src/editor/vscode.css';
@@ -132,6 +132,8 @@ function Level() {
   const {editor, infoProvider, editorConnection} =
   useLevelEditor(worldId, levelId, codeviewRef, initialCode, onDidChangeContent)
 
+  const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null)
+
   // TODO: This is a hack for having an introduction (i.e. level 0)
   // for each world.
   if (levelId == 0) {
@@ -241,11 +243,13 @@ function Level() {
 
         </div>}
       </div>
-      <div className="doc-panel">
-        {!level.isLoading && <Inventory tactics={level?.data?.tactics} lemmas={level?.data?.lemmas} definitions={level?.data?.definitions} />}
+      <div className="inventory-panel">
+        {!level.isLoading &&
+          <Inventory tactics={level?.data?.tactics} lemmas={level?.data?.lemmas}
+            definitions={level?.data?.definitions} setInventoryDoc={setInventoryDoc} />}
       </div>
-      <div className="side-panel">
-        <p>Display Tactic documentation here?</p>
+      <div className="doc-panel">
+        {inventoryDoc && <Documentation name={inventoryDoc.name} type={inventoryDoc.type} />}
       </div>
     </Split>
   </>

client/src/components/inventory.css

@@ -8,12 +8,6 @@
   margin-bottom: .2em;
 }
 
-
-.inventory h2.doc {
-  margin-top: 1.5em;
-  font-weight: 900;
-}
-
 .inventory-list {
   display: flex;
   gap: .5em;
@@ -58,3 +52,15 @@
   color: black;
   border-bottom: 0.3em solid var(--clr-primary);
 }
+
+
+.doc-panel {
+  padding: 0 1em;
+}
+
+.doc-panel h2 {
+  font-size: 1.5em;
+  margin-top: 1em;
+  margin-bottom: .2em;
+  font-weight: 900;
+}