From 116026428fdd0064785c42a9c4d0f9024930a7b4 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Thu, 9 Feb 2023 15:34:37 +0100 Subject: [PATCH] show lemma and tactic docs --- client/src/components/Inventory.tsx | 50 +++++++++++++++---- client/src/components/inventory.css | 22 +++++++- client/src/state/api.ts | 11 +++- server/leanserver/GameServer/Commands.lean | 5 -- .../leanserver/GameServer/EnvExtensions.lean | 8 +++ server/leanserver/GameServer/Game.lean | 41 ++++++++++++++- 6 files changed, 118 insertions(+), 19 deletions(-) diff --git a/client/src/components/Inventory.tsx b/client/src/components/Inventory.tsx index 915186c..e90ac1e 100644 --- a/client/src/components/Inventory.tsx +++ b/client/src/components/Inventory.tsx @@ -4,31 +4,61 @@ import './inventory.css' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faLock, faLockOpen, faBook, faHammer, faBan } from '@fortawesome/free-solid-svg-icons' import Markdown from './Markdown'; +import { useLoadDocQuery } from '../state/api'; function Inventory({ tactics, lemmas } : {lemmas: {name: string, locked: boolean, disabled: boolean}[], tactics: {name: string, locked: boolean, disabled: boolean}[]}) { + const [docName, setDocName] = useState(null) + const [docType, setDocType] = useState(null) + + return ( - <>
- { tactics.map(tac => ) } - {/* TODO: Click on Tactic: show info - TODO: click on paste icon -> paste into command line */} -
+

Tactics

+
+ { tactics.map(tac => + {setDocName(tac.name); setDocType("tactic")}} + name={tac.name} locked={tac.locked} disabled={tac.disabled} />) } + {/* TODO: Click on Tactic: show info + TODO: click on paste icon -> paste into command line */} +
-
- { lemmas.map(lem => ) } +

Lemmas

+
+ { lemmas.map(lem => + {setDocName(lem.name); setDocType("lemma")}} + name={lem.name} locked={lem.locked} disabled={lem.disabled} />) } +
+ + {docName && }
- ) } -function InventoryItem({name, locked, disabled}) { +function InventoryItem({name, locked, disabled, showDoc}) { const icon = locked ? : disabled ? : "" const className = locked ? "locked" : disabled ? "disabled" : "" - return
{icon} {name}
+ + const handleClick = () => { + if (!locked && !disabled) { + showDoc() + } + } + + return
{icon} {name}
+} + +function Documentation({name, type}) { + + const doc = useLoadDocQuery({type: type, name: name}) + + return <> +

{doc.data?.name}

+ {doc.data?.text} + } export default Inventory; diff --git a/client/src/components/inventory.css b/client/src/components/inventory.css index 0cd3c44..82aa370 100644 --- a/client/src/components/inventory.css +++ b/client/src/components/inventory.css @@ -1,8 +1,23 @@ .inventory { + padding: 0 1em; +} + +.inventory h2 { + font-size: 1.5em; + margin-top: 1em; + margin-bottom: .2em; +} + + +.inventory h2.doc { + margin-top: 1.5em; + font-weight: 900; +} + +.inventory-list { display: flex; gap: .5em; flex-wrap : wrap; - padding: 1em } .inventory .item { @@ -14,3 +29,8 @@ .inventory .item.disabled { color: #aaa; } + + +.inventory .item:not(.locked):not(.disabled) { + cursor: pointer; +} diff --git a/client/src/state/api.ts b/client/src/state/api.ts index 5fb947c..0d94ba2 100644 --- a/client/src/state/api.ts +++ b/client/src/state/api.ts @@ -20,6 +20,12 @@ interface LevelInfo { descrFormat: null|string, } +interface Doc { + name: string, + text: string +} + + const customBaseQuery = async ( args : {method: string, params?: any}, { signal, dispatch, getState, extra }, @@ -48,9 +54,12 @@ export const apiSlice = createApi({ loadLevel: builder.query({ query: ({world, level}) => {return {method: "loadLevel", params: {world, level}}}, }), + loadDoc: builder.query({ + query: ({name, type}) => {return {method: "loadDoc", params: {name, type}}}, + }), }), }) // Export hooks for usage in functional components, which are // auto-generated based on the defined endpoints -export const { useGetGameInfoQuery, useLoadLevelQuery } = apiSlice +export const { useGetGameInfoQuery, useLoadLevelQuery, useLoadDocQuery } = apiSlice diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean index 6e3085e..9068e41 100644 --- a/server/leanserver/GameServer/Commands.lean +++ b/server/leanserver/GameServer/Commands.lean @@ -250,11 +250,6 @@ elab "NewLemmas" args:ident* : command => do /-! ## Make Game -/ -def getTacticDoc! (tac : Name) : CommandElabM TacticDocEntry := do - match (tacticDocExt.getState (← getEnv)).find? (·.name = tac) with - | some doc => return doc - | none => throwError "Tactic documentation not found: {tac}" - /-- Make the final Game. This command will precompute various things about the game, such as which tactics are available in each level etc. -/ elab "MakeGame" : command => do diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean index 1dc476c..9c1f13d 100644 --- a/server/leanserver/GameServer/EnvExtensions.lean +++ b/server/leanserver/GameServer/EnvExtensions.lean @@ -41,6 +41,10 @@ initialize tacticDocExt : SimplePersistentEnvExtension TacticDocEntry (Array Tac addImportedFn := Array.concatMap id } +def getTacticDoc? {m : Type → Type} [Monad m] [MonadEnv m] (tac : Name) : + m (Option TacticDocEntry) := do + return (tacticDocExt.getState (← getEnv)).find? (·.name = tac) + open Elab Command in /-- Print a registered tactic doc for debugging purposes. -/ elab "#print_tactic_doc" : command => do @@ -64,6 +68,10 @@ initialize lemmaDocExt : SimplePersistentEnvExtension LemmaDocEntry (Array Lemma addImportedFn := Array.concatMap id } +def getLemmaDoc? {m : Type → Type} [Monad m] [MonadEnv m] (tac : Name) : + m (Option LemmaDocEntry) := do + return (lemmaDocExt.getState (← getEnv)).find? (·.name = tac) + open Elab Command in /-- Print a lemma doc for debugging purposes. -/ elab "#print_lemma_doc" : command => do diff --git a/server/leanserver/GameServer/Game.lean b/server/leanserver/GameServer/Game.lean index 4cedcda..9c0b073 100644 --- a/server/leanserver/GameServer/Game.lean +++ b/server/leanserver/GameServer/Game.lean @@ -53,6 +53,32 @@ structure LoadLevelParams where level : Nat deriving ToJson, FromJson +structure Doc where + name: String + text: String +deriving ToJson + +inductive TacOrLem := | tactic | «lemma» +deriving ToJson, FromJson + +structure LoadDocParams where + name : Name + type : TacOrLem +deriving ToJson, FromJson + +def mkDoc (name : Name) (type : TacOrLem) : GameServerM (Option Doc) := do + match type with + | .tactic => do + let doc ← getTacticDoc? name + return doc.map fun doc => + { name := doc.name.toString + text := doc.content } + | .lemma => do + let doc ← getLemmaDoc? name + return doc.map fun doc => + { name := doc.name.toString + text := doc.content } + partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do match ev with | ServerEvent.clientMsg msg => @@ -68,8 +94,9 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do let c ← read let some lvl ← getLevel? {game := s.game, world := p.world, level := p.level} | do - c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Level not found: world {p.world}, level {p.level}", none⟩ - return true + c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Level not found: world {p.world}, level {p.level}", none⟩ + return true + let levelInfo : LevelInfo := { index := lvl.index, title := lvl.title, @@ -80,6 +107,16 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do introduction := lvl.introduction } c.hOut.writeLspResponse ⟨id, ToJson.toJson levelInfo⟩ return true + | Message.request id "loadDoc" params => + let p ← parseParams LoadDocParams (toJson params) + let s ← get + let c ← read + let some doc ← mkDoc p.name p.type + | do + c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Documentation not found: {p.name}", none⟩ + return true + c.hOut.writeLspResponse ⟨id, ToJson.toJson doc⟩ + return true | _ => return false | _ => return false