diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index 04ae774..92fb3ed 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -44,8 +44,15 @@ export const MonacoEditorContext = React.createContext<monaco.editor.IStandalone
 
 export const InputModeContext = React.createContext<{
   commandLineMode: boolean,
-  setCommandLineMode: React.Dispatch<React.SetStateAction<boolean>>
-}>({commandLineMode: true, setCommandLineMode: () => {}});
+  setCommandLineMode: React.Dispatch<React.SetStateAction<boolean>>,
+  commandLineInput: string,
+  setCommandLineInput: React.Dispatch<React.SetStateAction<string>>
+}>({
+  commandLineMode: true,
+  setCommandLineMode: () => {},
+  commandLineInput: "",
+  setCommandLineInput: () => {},
+});
 
 function Level() {
 
@@ -56,9 +63,12 @@ function Level() {
   const codeviewRef = useRef<HTMLDivElement>(null)
   const introductionPanelRef = useRef<HTMLDivElement>(null)
 
+  const initialCode = useSelector(selectCode(worldId, levelId))
+
   const [commandLineMode, setCommandLineMode] = useState(true)
+  const [commandLineInput, setCommandLineInput] = useState("")
   const [showSidePanel, setShowSidePanel] = useState(true)
-  const [canUndo, setCanUndo] = useState(true)
+  const [canUndo, setCanUndo] = useState(initialCode.trim() !== "")
 
   const toggleSidePanel = () => {
     setShowSidePanel(!showSidePanel)
@@ -119,7 +129,6 @@ function Level() {
     setCanUndo(code.trim() !== "")
   }
 
-  const initialCode = useSelector(selectCode(worldId, levelId))
 
   const {editor, infoProvider, editorConnection} =
     useLevelEditor(worldId, levelId, codeviewRef, initialCode, onDidChangeContent)
@@ -168,7 +177,7 @@ function Level() {
 
         <EditorContext.Provider value={editorConnection}>
           <MonacoEditorContext.Provider value={editor}>
-            <InputModeContext.Provider value={{commandLineMode, setCommandLineMode}}>
+            <InputModeContext.Provider value={{commandLineMode, setCommandLineMode, commandLineInput, setCommandLineInput}}>
               {editorConnection && <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />}
             </InputModeContext.Provider>
           </MonacoEditorContext.Provider>
diff --git a/client/src/components/infoview/CommandLine.tsx b/client/src/components/infoview/CommandLine.tsx
index 06960e4..45ef83c 100644
--- a/client/src/components/infoview/CommandLine.tsx
+++ b/client/src/components/infoview/CommandLine.tsx
@@ -1,5 +1,5 @@
 import * as React from 'react'
-import { useRef, useState } from 'react'
+import { useRef, useState, useEffect } from 'react'
 import { LspDiagnosticsContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
 import { useServerNotificationEffect } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
@@ -8,69 +8,204 @@ import { InputModeContext, MonacoEditorContext } from '../Level'
 
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faWandMagicSparkles } from '@fortawesome/free-solid-svg-icons'
+import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter';
+import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider';
 
+import { Registry } from 'monaco-textmate' // peer dependency
+import { wireTmGrammars } from 'monaco-editor-textmate'
+import * as lightPlusTheme from 'lean4web/client/src/lightPlus.json'
+import * as leanSyntax from 'lean4web/client/src/syntaxes/lean.json'
+import * as leanMarkdownSyntax from 'lean4web/client/src/syntaxes/lean-markdown.json'
+import * as codeblockSyntax from 'lean4web/client/src/syntaxes/codeblock.json'
+import languageConfig from 'lean4/language-configuration.json';
 
-function hasErrorsOrWarnings(diags) {
-  return diags.some(
-    (d) =>
-      !d.message.startsWith("unsolved goals") &&
-      (d.severity == DiagnosticSeverity.Error || d.severity == DiagnosticSeverity.Warning)
-  )
-}
+
+/* We register a new language `leancmd` that looks like lean4, but does not use the lsp server. */
+
+// register Monaco languages
+monaco.languages.register({
+  id: 'lean4cmd',
+  extensions: ['.leancmd']
+})
+
+// map of monaco "language id's" to TextMate scopeNames
+const grammars = new Map()
+grammars.set('lean4', 'source.lean')
+grammars.set('lean4cmd', 'source.lean')
+
+const registry = new Registry({
+  getGrammarDefinition: async (scopeName) => {
+    if (scopeName === 'source.lean') {
+      return {
+          format: 'json',
+          content: JSON.stringify(leanSyntax)
+      }
+    } else if (scopeName === 'source.lean.markdown') {
+      return {
+          format: 'json',
+          content: JSON.stringify(leanMarkdownSyntax)
+      }
+    } else {
+      return {
+          format: 'json',
+          content: JSON.stringify(codeblockSyntax)
+      }
+    }
+  }
+});
+
+wireTmGrammars(monaco, registry, grammars)
+
+let config: any = { ...languageConfig }
+config.autoClosingPairs = config.autoClosingPairs.map(
+  pair => { return {'open': pair[0], 'close': pair[1]} }
+)
+monaco.languages.setLanguageConfiguration('lean4cmd', config);
 
 export function CommandLine() {
 
+  /** Reference to the hidden multi-line editor */
   const editor = React.useContext(MonacoEditorContext)
-  const commandInput = useRef<HTMLInputElement>()
+  const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
   const [processing, setProcessing] = useState(false)
 
-  const { commandLineMode } = React.useContext(InputModeContext)
-  const allDiags = React.useContext(LspDiagnosticsContext)
-  const diags = allDiags.get(editor.getModel().uri.toString())
+  const { commandLineMode, commandLineInput, setCommandLineInput } = React.useContext(InputModeContext)
 
-  React.useEffect(() => {
-    if (commandLineMode) {
-      const endPos = editor.getModel().getFullModelRange().getEndPosition()
-      if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") {
-        editor.executeEdits("command-line", [{
-          range: monaco.Selection.fromPositions(endPos, endPos),
-          text: "\n",
-          forceMoveMarkers: false
-        }]);
-      }
-      editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
-    }
-  }, [commandLineMode])
+  const inputRef = useRef()
 
-  const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
-    ev.preventDefault()
+  // Run the command
+  const runCommand = React.useCallback(() => {
+    if (processing) return;
     const pos = editor.getPosition()
     editor.executeEdits("command-line", [{
       range: monaco.Selection.fromPositions(
         pos,
         editor.getModel().getFullModelRange().getEndPosition()
       ),
-      text: commandInput.current!.value + "\n",
+      text: commandLineInput + "\n",
       forceMoveMarkers: false
     }]);
     editor.setPosition(pos)
     setProcessing(true)
-  }
+  }, [commandLineInput, editor])
+
+  useEffect(() => {
+    if (oneLineEditor && oneLineEditor.getValue() !== commandLineInput) {
+      oneLineEditor.setValue(commandLineInput)
+    }
+  }, [commandLineInput])
 
+  // React when answer from the server comes back
   useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
     if (params.uri == editor.getModel().uri.toString()) {
       setProcessing(false)
       if (!hasErrorsOrWarnings(params.diagnostics)) {
-        commandInput.current!.value = "";
+        setCommandLineInput("")
         editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
       }
     }
   }, []);
 
+  useEffect(() => {
+    const myEditor = monaco.editor.create(inputRef.current!, {
+      value: commandLineInput,
+      language: "lean4cmd",
+      quickSuggestions: false,
+      lightbulb: {
+        enabled: true
+      },
+      unicodeHighlight: {
+          ambiguousCharacters: false,
+      },
+      automaticLayout: true,
+      minimap: {
+        enabled: false
+      },
+      lineNumbers: 'off',
+      glyphMargin: false,
+      folding: false,
+      lineDecorationsWidth: 0,
+      lineNumbersMinChars: 0,
+      'semanticHighlighting.enabled': true,
+      overviewRulerLanes: 0,
+      hideCursorInOverviewRuler: true,
+      scrollbar: {
+        vertical: 'hidden',
+        horizontalScrollbarSize: 3
+      },
+      overviewRulerBorder: false,
+      theme: 'vs-code-theme-converted',
+      contextmenu: false
+    })
+
+    setOneLineEditor(myEditor)
+
+    const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), myEditor.getModel(), myEditor)
+
+    return () => {abbrevRewriter.dispose(); myEditor.dispose()}
+  }, [])
+
+  useEffect(() => {
+    if (!oneLineEditor) return
+    // Ensure that our one-line editor can only have a single line
+    const l = oneLineEditor.getModel().onDidChangeContent((e) => {
+      const value = oneLineEditor.getValue()
+      setCommandLineInput(value)
+      const newValue = value.replace(/[\n\r]/g, '')
+      if (value != newValue) {
+        oneLineEditor.setValue(newValue)
+      }
+    })
+    return () => { l.dispose() }
+  }, [oneLineEditor, setCommandLineInput])
+
+  useEffect(() => {
+    if (!oneLineEditor) return
+    // Run command when pressing enter
+    const l = oneLineEditor.onKeyUp((ev) => {
+      if (ev.code === "Enter") {
+        runCommand()
+      }
+    })
+    return () => { l.dispose() }
+  }, [oneLineEditor, runCommand])
+
+  // Effect when command line mode gets enabled
+  useEffect(() => {
+    if (commandLineMode) {
+      const endPos = editor.getModel().getFullModelRange().getEndPosition()
+      if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") {
+        editor.executeEdits("command-line", [{
+          range: monaco.Selection.fromPositions(endPos, endPos),
+          text: commandLineInput + "\n",
+          forceMoveMarkers: false
+        }]);
+      }
+      editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
+    }
+  }, [commandLineMode])
+
+  const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
+    ev.preventDefault()
+    runCommand()
+  }
+
   return <div className="command-line">
       <form onSubmit={handleSubmit}>
-        <input type="text" ref={commandInput} disabled={processing} />
+        <div className="command-line-input-wrapper">
+          <div ref={inputRef} className="command-line-input" />
+        </div>
         <button type="submit" disabled={processing} className="btn btn-inverted"><FontAwesomeIcon icon={faWandMagicSparkles} /> Run</button>
       </form>
     </div>
 }
+
+/** Checks whether the diagnostics contain any errors or warnings to check whether the level has
+   been completed.*/
+function hasErrorsOrWarnings(diags) {
+  return diags.some(
+    (d) =>
+      !d.message.startsWith("unsolved goals") &&
+      (d.severity == DiagnosticSeverity.Error || d.severity == DiagnosticSeverity.Warning)
+  )
+}
diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx
index 0ee317f..6393c0c 100644
--- a/client/src/components/infoview/goals.tsx
+++ b/client/src/components/infoview/goals.tsx
@@ -118,13 +118,14 @@ interface GoalProps {
     goal: InteractiveGoal
     filter: GoalFilterState
     showHints?: boolean
+    commandLine: boolean
 }
 
 /**
  * Displays the hypotheses, target type and optional case label of a goal according to the
  * provided `filter`. */
 export const Goal = React.memo((props: GoalProps) => {
-    const { goal, filter, showHints } = props
+    const { goal, filter, showHints, commandLine } = props
 
     const filteredList = getFilteredHypotheses(goal.hyps, filter);
     const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList;
@@ -159,7 +160,7 @@ export const Goal = React.memo((props: GoalProps) => {
         { assumptionHyps.length > 0 &&
             <div className="hyp-group"><div className="hyp-group-title">Assumptions:</div>
             {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
-        {commandLineMode && <CommandLine />}
+        {commandLine && commandLineMode && <CommandLine />}
         {!filter.reverse && goalLi}
         {showHints && hints}
     </div>
@@ -175,7 +176,7 @@ export function Goals({ goals, filter }: GoalsProps) {
         return <>No goals</>
     } else {
         return <>
-            {goals.goals.map((g, i) => <Goal key={i} goal={g} filter={filter} />)}
+            {goals.goals.map((g, i) => <Goal commandLine={false} key={i} goal={g} filter={filter} />)}
         </>
     }
 }
diff --git a/client/src/components/infoview/info.tsx b/client/src/components/infoview/info.tsx
index dfe66a9..3958b5f 100644
--- a/client/src/components/infoview/info.tsx
+++ b/client/src/components/infoview/info.tsx
@@ -16,6 +16,7 @@ import { PanelWidgetDisplay } from '../../../../node_modules/lean4-infoview/src/
 import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
 import { GoalsLocation, Locations, LocationsContext } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation';
 import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode'
+import { Troubleshoot } from '@mui/icons-material';
 
 type InfoStatus = 'updating' | 'error' | 'ready';
 type InfoKind = 'cursor' | 'pin';
@@ -123,7 +124,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
             <div className="goals-section">
                 { goals && goals.goals.length > 0
                   ? <><div className="goals-section-title">Main Goal</div>
-                    <Goal filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} /></>
+                    <Goal commandLine={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} /></>
                   : <div className="goals-section-title">No Goals</div> }
             </div>
         </LocationsContext.Provider>
@@ -149,7 +150,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                     <div className="goals-section-title">Other Goals</div>
 
                     {goals.goals.slice(1).map((goal, i) =>
-                        <details key={i}><summary><InteractiveCode fmt={goal.type} /></summary> <Goal filter={goalFilter} goal={goal} /></details>)}
+                        <details key={i}><summary><InteractiveCode fmt={goal.type} /></summary> <Goal commandLine={false} filter={goalFilter} goal={goal} /></details>)}
                 </div>}
         </LocationsContext.Provider>
     </>
diff --git a/client/src/components/infoview/infoview.css b/client/src/components/infoview/infoview.css
index c3d4145..e91bc49 100644
--- a/client/src/components/infoview/infoview.css
+++ b/client/src/components/infoview/infoview.css
@@ -44,10 +44,6 @@
   margin: 0.2em 0;
 }
 
-.command-line input[type="text"] {
-  font-family: var(--vscode-editor-font-family);
-}
-
 .command-line form {
   display: flex;
 }
@@ -56,8 +52,21 @@
   display: block;
 }
 
-.command-line form>input[type="text"]{
+.command-line .command-line-input-wrapper{
   flex: 1;
-  padding: 0.2em .6em;
+  padding: 0.4em .6em 0;
   font-size: 1rem;
+  background: white;
+}
+
+.command-line .command-line-input{
+  height: 1.2em;
+}
+
+/* Turn off some monaco decorations: */
+.command-line-input .monaco-editor .view-overlays .current-line {
+  border: 0;
+}
+.command-line-input .monaco-editor .scroll-decoration {
+  box-shadow: none;
 }
diff --git a/client/src/components/level.css b/client/src/components/level.css
index 542c587..e601ea6 100644
--- a/client/src/components/level.css
+++ b/client/src/components/level.css
@@ -117,6 +117,27 @@ td code  {
   white-space:nowrap;
 }
 
+/* Styling in the editor while typing abbreviations such as "\alpha" */
+.abbreviation {
+  text-decoration: underline;
+}
+
+/* Styling in the left margin of the editor when processing */
+.processing {
+  background: linear-gradient(
+    to right,
+    rgba(255, 165, 0, 1) 0%,
+    rgba(255, 165, 0, 1) 30%,
+    transparent 30%,
+    transparent  100%
+  );
+}
+
+/* Styling in the left margin of the editor on error */
+.glyph-margin-error {
+  background: rgba(255, 0, 0, 1);
+}
+
 /***************************************/
 /* TODO: For development purposes only */
 /***************************************/
diff --git a/package-lock.json b/package-lock.json
index 872ea83..e4f50b9 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -72,9 +72,9 @@
       }
     },
     "node_modules/@babel/cli": {
-      "version": "7.19.3",
-      "resolved": "https://registry.npmjs.org/@babel/cli/-/cli-7.19.3.tgz",
-      "integrity": "sha512-643/TybmaCAe101m2tSVHi9UKpETXP9c/Ff4mD2tAwkdP6esKIfaauZFc67vGEM6r9fekbEGid+sZhbEnSe3dg==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/cli/-/cli-7.20.7.tgz",
+      "integrity": "sha512-WylgcELHB66WwQqItxNILsMlaTd8/SO6SgTTjMp4uCI7P4QyH1r3nqgFmO3BfM4AtfniHgFMH3EpYFj/zynBkQ==",
       "dev": true,
       "dependencies": {
         "@jridgewell/trace-mapping": "^0.3.8",
@@ -112,32 +112,32 @@
       }
     },
     "node_modules/@babel/compat-data": {
-      "version": "7.20.5",
-      "resolved": "https://registry.npmjs.org/@babel/compat-data/-/compat-data-7.20.5.tgz",
-      "integrity": "sha512-KZXo2t10+/jxmkhNXc7pZTqRvSOIvVv/+lJwHS+B2rErwOyjuVRh60yVpb7liQ1U5t7lLJ1bz+t8tSypUZdm0g==",
+      "version": "7.20.14",
+      "resolved": "https://registry.npmjs.org/@babel/compat-data/-/compat-data-7.20.14.tgz",
+      "integrity": "sha512-0YpKHD6ImkWMEINCyDAD0HLLUH/lPCefG8ld9it8DJB2wnApraKuhgYTvTY1z7UFIfBTGy5LwncZ+5HWWGbhFw==",
       "engines": {
         "node": ">=6.9.0"
       }
     },
     "node_modules/@babel/core": {
-      "version": "7.20.5",
-      "resolved": "https://registry.npmjs.org/@babel/core/-/core-7.20.5.tgz",
-      "integrity": "sha512-UdOWmk4pNWTm/4DlPUl/Pt4Gz4rcEMb7CY0Y3eJl5Yz1vI8ZJGmHWaVE55LoxRjdpx0z259GE9U5STA9atUinQ==",
+      "version": "7.20.12",
+      "resolved": "https://registry.npmjs.org/@babel/core/-/core-7.20.12.tgz",
+      "integrity": "sha512-XsMfHovsUYHFMdrIHkZphTN/2Hzzi78R08NuHfDBehym2VsPDL6Zn/JAD/JQdnRvbSsbQc4mVaU1m6JgtTEElg==",
       "dependencies": {
         "@ampproject/remapping": "^2.1.0",
         "@babel/code-frame": "^7.18.6",
-        "@babel/generator": "^7.20.5",
-        "@babel/helper-compilation-targets": "^7.20.0",
-        "@babel/helper-module-transforms": "^7.20.2",
-        "@babel/helpers": "^7.20.5",
-        "@babel/parser": "^7.20.5",
-        "@babel/template": "^7.18.10",
-        "@babel/traverse": "^7.20.5",
-        "@babel/types": "^7.20.5",
+        "@babel/generator": "^7.20.7",
+        "@babel/helper-compilation-targets": "^7.20.7",
+        "@babel/helper-module-transforms": "^7.20.11",
+        "@babel/helpers": "^7.20.7",
+        "@babel/parser": "^7.20.7",
+        "@babel/template": "^7.20.7",
+        "@babel/traverse": "^7.20.12",
+        "@babel/types": "^7.20.7",
         "convert-source-map": "^1.7.0",
         "debug": "^4.1.0",
         "gensync": "^1.0.0-beta.2",
-        "json5": "^2.2.1",
+        "json5": "^2.2.2",
         "semver": "^6.3.0"
       },
       "engines": {
@@ -149,11 +149,11 @@
       }
     },
     "node_modules/@babel/generator": {
-      "version": "7.20.5",
-      "resolved": "https://registry.npmjs.org/@babel/generator/-/generator-7.20.5.tgz",
-      "integrity": "sha512-jl7JY2Ykn9S0yj4DQP82sYvPU+T3g0HFcWTqDLqiuA9tGRNIj9VfbtXGAYTTkyNEnQk1jkMGOdYka8aG/lulCA==",
+      "version": "7.20.14",
+      "resolved": "https://registry.npmjs.org/@babel/generator/-/generator-7.20.14.tgz",
+      "integrity": "sha512-AEmuXHdcD3A52HHXxaTmYlb8q/xMEhoRP67B3T4Oq7lbmSoqroMZzjnGj3+i1io3pdnF8iBYVu4Ilj+c4hBxYg==",
       "dependencies": {
-        "@babel/types": "^7.20.5",
+        "@babel/types": "^7.20.7",
         "@jridgewell/gen-mapping": "^0.3.2",
         "jsesc": "^2.5.1"
       },
@@ -200,13 +200,14 @@
       }
     },
     "node_modules/@babel/helper-compilation-targets": {
-      "version": "7.20.0",
-      "resolved": "https://registry.npmjs.org/@babel/helper-compilation-targets/-/helper-compilation-targets-7.20.0.tgz",
-      "integrity": "sha512-0jp//vDGp9e8hZzBc6N/KwA5ZK3Wsm/pfm4CrY7vzegkVxc65SgSn6wYOnwHe9Js9HRQ1YTCKLGPzDtaS3RoLQ==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/helper-compilation-targets/-/helper-compilation-targets-7.20.7.tgz",
+      "integrity": "sha512-4tGORmfQcrc+bvrjb5y3dG9Mx1IOZjsHqQVUz7XCNHO+iTmqxWnVg3KRygjGmpRLJGdQSKuvFinbIb0CnZwHAQ==",
       "dependencies": {
-        "@babel/compat-data": "^7.20.0",
+        "@babel/compat-data": "^7.20.5",
         "@babel/helper-validator-option": "^7.18.6",
         "browserslist": "^4.21.3",
+        "lru-cache": "^5.1.1",
         "semver": "^6.3.0"
       },
       "engines": {
@@ -217,17 +218,18 @@
       }
     },
     "node_modules/@babel/helper-create-class-features-plugin": {
-      "version": "7.20.5",
-      "resolved": "https://registry.npmjs.org/@babel/helper-create-class-features-plugin/-/helper-create-class-features-plugin-7.20.5.tgz",
-      "integrity": "sha512-3RCdA/EmEaikrhayahwToF0fpweU/8o2p8vhc1c/1kftHOdTKuC65kik/TLc+qfbS8JKw4qqJbne4ovICDhmww==",
+      "version": "7.20.12",
+      "resolved": "https://registry.npmjs.org/@babel/helper-create-class-features-plugin/-/helper-create-class-features-plugin-7.20.12.tgz",
+      "integrity": "sha512-9OunRkbT0JQcednL0UFvbfXpAsUXiGjUk0a7sN8fUXX7Mue79cUSMjHGDRRi/Vz9vYlpIhLV5fMD5dKoMhhsNQ==",
       "dev": true,
       "dependencies": {
         "@babel/helper-annotate-as-pure": "^7.18.6",
         "@babel/helper-environment-visitor": "^7.18.9",
         "@babel/helper-function-name": "^7.19.0",
-        "@babel/helper-member-expression-to-functions": "^7.18.9",
+        "@babel/helper-member-expression-to-functions": "^7.20.7",
         "@babel/helper-optimise-call-expression": "^7.18.6",
-        "@babel/helper-replace-supers": "^7.19.1",
+        "@babel/helper-replace-supers": "^7.20.7",
+        "@babel/helper-skip-transparent-expression-wrappers": "^7.20.0",
         "@babel/helper-split-export-declaration": "^7.18.6"
       },
       "engines": {
@@ -314,12 +316,12 @@
       }
     },
     "node_modules/@babel/helper-member-expression-to-functions": {
-      "version": "7.18.9",
-      "resolved": "https://registry.npmjs.org/@babel/helper-member-expression-to-functions/-/helper-member-expression-to-functions-7.18.9.tgz",
-      "integrity": "sha512-RxifAh2ZoVU67PyKIO4AMi1wTenGfMR/O/ae0CCRqwgBAt5v7xjdtRw7UoSbsreKrQn5t7r89eruK/9JjYHuDg==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/helper-member-expression-to-functions/-/helper-member-expression-to-functions-7.20.7.tgz",
+      "integrity": "sha512-9J0CxJLq315fEdi4s7xK5TQaNYjZw+nDVpVqr1axNGKzdrdwYBD5b4uKv3n75aABG0rCCTK8Im8Ww7eYfMrZgw==",
       "dev": true,
       "dependencies": {
-        "@babel/types": "^7.18.9"
+        "@babel/types": "^7.20.7"
       },
       "engines": {
         "node": ">=6.9.0"
@@ -337,18 +339,18 @@
       }
     },
     "node_modules/@babel/helper-module-transforms": {
-      "version": "7.20.2",
-      "resolved": "https://registry.npmjs.org/@babel/helper-module-transforms/-/helper-module-transforms-7.20.2.tgz",
-      "integrity": "sha512-zvBKyJXRbmK07XhMuujYoJ48B5yvvmM6+wcpv6Ivj4Yg6qO7NOZOSnvZN9CRl1zz1Z4cKf8YejmCMh8clOoOeA==",
+      "version": "7.20.11",
+      "resolved": "https://registry.npmjs.org/@babel/helper-module-transforms/-/helper-module-transforms-7.20.11.tgz",
+      "integrity": "sha512-uRy78kN4psmji1s2QtbtcCSaj/LILFDp0f/ymhpQH5QY3nljUZCaNWz9X1dEj/8MBdBEFECs7yRhKn8i7NjZgg==",
       "dependencies": {
         "@babel/helper-environment-visitor": "^7.18.9",
         "@babel/helper-module-imports": "^7.18.6",
         "@babel/helper-simple-access": "^7.20.2",
         "@babel/helper-split-export-declaration": "^7.18.6",
         "@babel/helper-validator-identifier": "^7.19.1",
-        "@babel/template": "^7.18.10",
-        "@babel/traverse": "^7.20.1",
-        "@babel/types": "^7.20.2"
+        "@babel/template": "^7.20.7",
+        "@babel/traverse": "^7.20.10",
+        "@babel/types": "^7.20.7"
       },
       "engines": {
         "node": ">=6.9.0"
@@ -393,16 +395,17 @@
       }
     },
     "node_modules/@babel/helper-replace-supers": {
-      "version": "7.19.1",
-      "resolved": "https://registry.npmjs.org/@babel/helper-replace-supers/-/helper-replace-supers-7.19.1.tgz",
-      "integrity": "sha512-T7ahH7wV0Hfs46SFh5Jz3s0B6+o8g3c+7TMxu7xKfmHikg7EAZ3I2Qk9LFhjxXq8sL7UkP5JflezNwoZa8WvWw==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/helper-replace-supers/-/helper-replace-supers-7.20.7.tgz",
+      "integrity": "sha512-vujDMtB6LVfNW13jhlCrp48QNslK6JXi7lQG736HVbHz/mbf4Dc7tIRh1Xf5C0rF7BP8iiSxGMCmY6Ci1ven3A==",
       "dev": true,
       "dependencies": {
         "@babel/helper-environment-visitor": "^7.18.9",
-        "@babel/helper-member-expression-to-functions": "^7.18.9",
+        "@babel/helper-member-expression-to-functions": "^7.20.7",
         "@babel/helper-optimise-call-expression": "^7.18.6",
-        "@babel/traverse": "^7.19.1",
-        "@babel/types": "^7.19.0"
+        "@babel/template": "^7.20.7",
+        "@babel/traverse": "^7.20.7",
+        "@babel/types": "^7.20.7"
       },
       "engines": {
         "node": ">=6.9.0"
@@ -482,13 +485,13 @@
       }
     },
     "node_modules/@babel/helpers": {
-      "version": "7.20.6",
-      "resolved": "https://registry.npmjs.org/@babel/helpers/-/helpers-7.20.6.tgz",
-      "integrity": "sha512-Pf/OjgfgFRW5bApskEz5pvidpim7tEDPlFtKcNRXWmfHGn9IEI2W2flqRQXTFb7gIPTyK++N6rVHuwKut4XK6w==",
+      "version": "7.20.13",
+      "resolved": "https://registry.npmjs.org/@babel/helpers/-/helpers-7.20.13.tgz",
+      "integrity": "sha512-nzJ0DWCL3gB5RCXbUO3KIMMsBY2Eqbx8mBpKGE/02PgyRQFcPQLbkQ1vyy596mZLaP+dAfD+R4ckASzNVmW3jg==",
       "dependencies": {
-        "@babel/template": "^7.18.10",
-        "@babel/traverse": "^7.20.5",
-        "@babel/types": "^7.20.5"
+        "@babel/template": "^7.20.7",
+        "@babel/traverse": "^7.20.13",
+        "@babel/types": "^7.20.7"
       },
       "engines": {
         "node": ">=6.9.0"
@@ -508,9 +511,9 @@
       }
     },
     "node_modules/@babel/parser": {
-      "version": "7.20.5",
-      "resolved": "https://registry.npmjs.org/@babel/parser/-/parser-7.20.5.tgz",
-      "integrity": "sha512-r27t/cy/m9uKLXQNWWebeCUHgnAZq0CpG1OwKRxzJMP1vpSU4bSIK2hq+/cp0bQxetkXx38n09rNu8jVkcK/zA==",
+      "version": "7.20.15",
+      "resolved": "https://registry.npmjs.org/@babel/parser/-/parser-7.20.15.tgz",
+      "integrity": "sha512-DI4a1oZuf8wC+oAJA9RW6ga3Zbe8RZFt7kD9i4qAspz3I/yHet1VvC3DiSy/fsUvv5pvJuNPh0LPOdCcqinDPg==",
       "bin": {
         "parser": "bin/babel-parser.js"
       },
@@ -534,14 +537,14 @@
       }
     },
     "node_modules/@babel/plugin-bugfix-v8-spread-parameters-in-optional-chaining": {
-      "version": "7.18.9",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-bugfix-v8-spread-parameters-in-optional-chaining/-/plugin-bugfix-v8-spread-parameters-in-optional-chaining-7.18.9.tgz",
-      "integrity": "sha512-AHrP9jadvH7qlOj6PINbgSuphjQUAK7AOT7DPjBo9EHoLhQTnnK5u45e1Hd4DbSQEO9nqPWtQ89r+XEOWFScKg==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-bugfix-v8-spread-parameters-in-optional-chaining/-/plugin-bugfix-v8-spread-parameters-in-optional-chaining-7.20.7.tgz",
+      "integrity": "sha512-sbr9+wNE5aXMBBFBICk01tt7sBf2Oc9ikRFEcem/ZORup9IMUdNhW7/wVLEbbtlWOsEubJet46mHAL2C8+2jKQ==",
       "dev": true,
       "dependencies": {
-        "@babel/helper-plugin-utils": "^7.18.9",
-        "@babel/helper-skip-transparent-expression-wrappers": "^7.18.9",
-        "@babel/plugin-proposal-optional-chaining": "^7.18.9"
+        "@babel/helper-plugin-utils": "^7.20.2",
+        "@babel/helper-skip-transparent-expression-wrappers": "^7.20.0",
+        "@babel/plugin-proposal-optional-chaining": "^7.20.7"
       },
       "engines": {
         "node": ">=6.9.0"
@@ -551,13 +554,13 @@
       }
     },
     "node_modules/@babel/plugin-proposal-async-generator-functions": {
-      "version": "7.20.1",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-proposal-async-generator-functions/-/plugin-proposal-async-generator-functions-7.20.1.tgz",
-      "integrity": "sha512-Gh5rchzSwE4kC+o/6T8waD0WHEQIsDmjltY8WnWRXHUdH8axZhuH86Ov9M72YhJfDrZseQwuuWaaIT/TmePp3g==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-proposal-async-generator-functions/-/plugin-proposal-async-generator-functions-7.20.7.tgz",
+      "integrity": "sha512-xMbiLsn/8RK7Wq7VeVytytS2L6qE69bXPB10YCmMdDZbKF4okCqY74pI/jJQ/8U0b/F6NrT2+14b8/P9/3AMGA==",
       "dev": true,
       "dependencies": {
         "@babel/helper-environment-visitor": "^7.18.9",
-        "@babel/helper-plugin-utils": "^7.19.0",
+        "@babel/helper-plugin-utils": "^7.20.2",
         "@babel/helper-remap-async-to-generator": "^7.18.9",
         "@babel/plugin-syntax-async-generators": "^7.8.4"
       },
@@ -585,13 +588,13 @@
       }
     },
     "node_modules/@babel/plugin-proposal-class-static-block": {
-      "version": "7.18.6",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-proposal-class-static-block/-/plugin-proposal-class-static-block-7.18.6.tgz",
-      "integrity": "sha512-+I3oIiNxrCpup3Gi8n5IGMwj0gOCAjcJUSQEcotNnCCPMEnixawOQ+KeJPlgfjzx+FKQ1QSyZOWe7wmoJp7vhw==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-proposal-class-static-block/-/plugin-proposal-class-static-block-7.20.7.tgz",
+      "integrity": "sha512-AveGOoi9DAjUYYuUAG//Ig69GlazLnoyzMw68VCDux+c1tsnnH/OkYcpz/5xzMkEFC6UxjR5Gw1c+iY2wOGVeQ==",
       "dev": true,
       "dependencies": {
-        "@babel/helper-create-class-features-plugin": "^7.18.6",
-        "@babel/helper-plugin-utils": "^7.18.6",
+        "@babel/helper-create-class-features-plugin": "^7.20.7",
+        "@babel/helper-plugin-utils": "^7.20.2",
         "@babel/plugin-syntax-class-static-block": "^7.14.5"
       },
       "engines": {
@@ -650,12 +653,12 @@
       }
     },
     "node_modules/@babel/plugin-proposal-logical-assignment-operators": {
-      "version": "7.18.9",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-proposal-logical-assignment-operators/-/plugin-proposal-logical-assignment-operators-7.18.9.tgz",
-      "integrity": "sha512-128YbMpjCrP35IOExw2Fq+x55LMP42DzhOhX2aNNIdI9avSWl2PI0yuBWarr3RYpZBSPtabfadkH2yeRiMD61Q==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-proposal-logical-assignment-operators/-/plugin-proposal-logical-assignment-operators-7.20.7.tgz",
+      "integrity": "sha512-y7C7cZgpMIjWlKE5T7eJwp+tnRYM89HmRvWM5EQuB5BoHEONjmQ8lSNmBUwOyy/GFRsohJED51YBF79hE1djug==",
       "dev": true,
       "dependencies": {
-        "@babel/helper-plugin-utils": "^7.18.9",
+        "@babel/helper-plugin-utils": "^7.20.2",
         "@babel/plugin-syntax-logical-assignment-operators": "^7.10.4"
       },
       "engines": {
@@ -698,16 +701,16 @@
       }
     },
     "node_modules/@babel/plugin-proposal-object-rest-spread": {
-      "version": "7.20.2",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-proposal-object-rest-spread/-/plugin-proposal-object-rest-spread-7.20.2.tgz",
-      "integrity": "sha512-Ks6uej9WFK+fvIMesSqbAto5dD8Dz4VuuFvGJFKgIGSkJuRGcrwGECPA1fDgQK3/DbExBJpEkTeYeB8geIFCSQ==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-proposal-object-rest-spread/-/plugin-proposal-object-rest-spread-7.20.7.tgz",
+      "integrity": "sha512-d2S98yCiLxDVmBmE8UjGcfPvNEUbA1U5q5WxaWFUGRzJSVAZqm5W6MbPct0jxnegUZ0niLeNX+IOzEs7wYg9Dg==",
       "dev": true,
       "dependencies": {
-        "@babel/compat-data": "^7.20.1",
-        "@babel/helper-compilation-targets": "^7.20.0",
+        "@babel/compat-data": "^7.20.5",
+        "@babel/helper-compilation-targets": "^7.20.7",
         "@babel/helper-plugin-utils": "^7.20.2",
         "@babel/plugin-syntax-object-rest-spread": "^7.8.3",
-        "@babel/plugin-transform-parameters": "^7.20.1"
+        "@babel/plugin-transform-parameters": "^7.20.7"
       },
       "engines": {
         "node": ">=6.9.0"
@@ -733,13 +736,13 @@
       }
     },
     "node_modules/@babel/plugin-proposal-optional-chaining": {
-      "version": "7.18.9",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-proposal-optional-chaining/-/plugin-proposal-optional-chaining-7.18.9.tgz",
-      "integrity": "sha512-v5nwt4IqBXihxGsW2QmCWMDS3B3bzGIk/EQVZz2ei7f3NJl8NzAJVvUmpDW5q1CRNY+Beb/k58UAH1Km1N411w==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-proposal-optional-chaining/-/plugin-proposal-optional-chaining-7.20.7.tgz",
+      "integrity": "sha512-T+A7b1kfjtRM51ssoOfS1+wbyCVqorfyZhT99TvxxLMirPShD8CzKMRepMlCBGM5RpHMbn8s+5MMHnPstJH6mQ==",
       "dev": true,
       "dependencies": {
-        "@babel/helper-plugin-utils": "^7.18.9",
-        "@babel/helper-skip-transparent-expression-wrappers": "^7.18.9",
+        "@babel/helper-plugin-utils": "^7.20.2",
+        "@babel/helper-skip-transparent-expression-wrappers": "^7.20.0",
         "@babel/plugin-syntax-optional-chaining": "^7.8.3"
       },
       "engines": {
@@ -1021,12 +1024,12 @@
       }
     },
     "node_modules/@babel/plugin-transform-arrow-functions": {
-      "version": "7.18.6",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-arrow-functions/-/plugin-transform-arrow-functions-7.18.6.tgz",
-      "integrity": "sha512-9S9X9RUefzrsHZmKMbDXxweEH+YlE8JJEuat9FdvW9Qh1cw7W64jELCtWNkPBPX5En45uy28KGvA/AySqUh8CQ==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-arrow-functions/-/plugin-transform-arrow-functions-7.20.7.tgz",
+      "integrity": "sha512-3poA5E7dzDomxj9WXWwuD6A5F3kc7VXwIJO+E+J8qtDtS+pXPAhrgEyh+9GBwBgPq1Z+bB+/JD60lp5jsN7JPQ==",
       "dev": true,
       "dependencies": {
-        "@babel/helper-plugin-utils": "^7.18.6"
+        "@babel/helper-plugin-utils": "^7.20.2"
       },
       "engines": {
         "node": ">=6.9.0"
@@ -1036,14 +1039,14 @@
       }
     },
     "node_modules/@babel/plugin-transform-async-to-generator": {
-      "version": "7.18.6",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-async-to-generator/-/plugin-transform-async-to-generator-7.18.6.tgz",
-      "integrity": "sha512-ARE5wZLKnTgPW7/1ftQmSi1CmkqqHo2DNmtztFhvgtOWSDfq0Cq9/9L+KnZNYSNrydBekhW3rwShduf59RoXag==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-async-to-generator/-/plugin-transform-async-to-generator-7.20.7.tgz",
+      "integrity": "sha512-Uo5gwHPT9vgnSXQxqGtpdufUiWp96gk7yiP4Mp5bm1QMkEmLXBO7PAGYbKoJ6DhAwiNkcHFBol/x5zZZkL/t0Q==",
       "dev": true,
       "dependencies": {
         "@babel/helper-module-imports": "^7.18.6",
-        "@babel/helper-plugin-utils": "^7.18.6",
-        "@babel/helper-remap-async-to-generator": "^7.18.6"
+        "@babel/helper-plugin-utils": "^7.20.2",
+        "@babel/helper-remap-async-to-generator": "^7.18.9"
       },
       "engines": {
         "node": ">=6.9.0"
@@ -1068,9 +1071,9 @@
       }
     },
     "node_modules/@babel/plugin-transform-block-scoping": {
-      "version": "7.20.5",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-block-scoping/-/plugin-transform-block-scoping-7.20.5.tgz",
-      "integrity": "sha512-WvpEIW9Cbj9ApF3yJCjIEEf1EiNJLtXagOrL5LNWEZOo3jv8pmPoYTSNJQvqej8OavVlgOoOPw6/htGZro6IkA==",
+      "version": "7.20.15",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-block-scoping/-/plugin-transform-block-scoping-7.20.15.tgz",
+      "integrity": "sha512-Vv4DMZ6MiNOhu/LdaZsT/bsLRxgL94d269Mv4R/9sp6+Mp++X/JqypZYypJXLlM4mlL352/Egzbzr98iABH1CA==",
       "dev": true,
       "dependencies": {
         "@babel/helper-plugin-utils": "^7.20.2"
@@ -1083,18 +1086,18 @@
       }
     },
     "node_modules/@babel/plugin-transform-classes": {
-      "version": "7.20.2",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-classes/-/plugin-transform-classes-7.20.2.tgz",
-      "integrity": "sha512-9rbPp0lCVVoagvtEyQKSo5L8oo0nQS/iif+lwlAz29MccX2642vWDlSZK+2T2buxbopotId2ld7zZAzRfz9j1g==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-classes/-/plugin-transform-classes-7.20.7.tgz",
+      "integrity": "sha512-LWYbsiXTPKl+oBlXUGlwNlJZetXD5Am+CyBdqhPsDVjM9Jc8jwBJFrKhHf900Kfk2eZG1y9MAG3UNajol7A4VQ==",
       "dev": true,
       "dependencies": {
         "@babel/helper-annotate-as-pure": "^7.18.6",
-        "@babel/helper-compilation-targets": "^7.20.0",
+        "@babel/helper-compilation-targets": "^7.20.7",
         "@babel/helper-environment-visitor": "^7.18.9",
         "@babel/helper-function-name": "^7.19.0",
         "@babel/helper-optimise-call-expression": "^7.18.6",
         "@babel/helper-plugin-utils": "^7.20.2",
-        "@babel/helper-replace-supers": "^7.19.1",
+        "@babel/helper-replace-supers": "^7.20.7",
         "@babel/helper-split-export-declaration": "^7.18.6",
         "globals": "^11.1.0"
       },
@@ -1106,12 +1109,13 @@
       }
     },
     "node_modules/@babel/plugin-transform-computed-properties": {
-      "version": "7.18.9",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-computed-properties/-/plugin-transform-computed-properties-7.18.9.tgz",
-      "integrity": "sha512-+i0ZU1bCDymKakLxn5srGHrsAPRELC2WIbzwjLhHW9SIE1cPYkLCL0NlnXMZaM1vhfgA2+M7hySk42VBvrkBRw==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-computed-properties/-/plugin-transform-computed-properties-7.20.7.tgz",
+      "integrity": "sha512-Lz7MvBK6DTjElHAmfu6bfANzKcxpyNPeYBGEafyA6E5HtRpjpZwU+u7Qrgz/2OR0z+5TvKYbPdphfSaAcZBrYQ==",
       "dev": true,
       "dependencies": {
-        "@babel/helper-plugin-utils": "^7.18.9"
+        "@babel/helper-plugin-utils": "^7.20.2",
+        "@babel/template": "^7.20.7"
       },
       "engines": {
         "node": ">=6.9.0"
@@ -1121,9 +1125,9 @@
       }
     },
     "node_modules/@babel/plugin-transform-destructuring": {
-      "version": "7.20.2",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-destructuring/-/plugin-transform-destructuring-7.20.2.tgz",
-      "integrity": "sha512-mENM+ZHrvEgxLTBXUiQ621rRXZes3KWUv6NdQlrnr1TkWVw+hUjQBZuP2X32qKlrlG2BzgR95gkuCRSkJl8vIw==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-destructuring/-/plugin-transform-destructuring-7.20.7.tgz",
+      "integrity": "sha512-Xwg403sRrZb81IVB79ZPqNQME23yhugYVqgTxAhT99h485F4f+GMELFhhOsscDUB7HCswepKeCKLn/GZvUKoBA==",
       "dev": true,
       "dependencies": {
         "@babel/helper-plugin-utils": "^7.20.2"
@@ -1245,13 +1249,13 @@
       }
     },
     "node_modules/@babel/plugin-transform-modules-amd": {
-      "version": "7.19.6",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-modules-amd/-/plugin-transform-modules-amd-7.19.6.tgz",
-      "integrity": "sha512-uG3od2mXvAtIFQIh0xrpLH6r5fpSQN04gIVovl+ODLdUMANokxQLZnPBHcjmv3GxRjnqwLuHvppjjcelqUFZvg==",
+      "version": "7.20.11",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-modules-amd/-/plugin-transform-modules-amd-7.20.11.tgz",
+      "integrity": "sha512-NuzCt5IIYOW0O30UvqktzHYR2ud5bOWbY0yaxWZ6G+aFzOMJvrs5YHNikrbdaT15+KNO31nPOy5Fim3ku6Zb5g==",
       "dev": true,
       "dependencies": {
-        "@babel/helper-module-transforms": "^7.19.6",
-        "@babel/helper-plugin-utils": "^7.19.0"
+        "@babel/helper-module-transforms": "^7.20.11",
+        "@babel/helper-plugin-utils": "^7.20.2"
       },
       "engines": {
         "node": ">=6.9.0"
@@ -1261,14 +1265,14 @@
       }
     },
     "node_modules/@babel/plugin-transform-modules-commonjs": {
-      "version": "7.19.6",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-modules-commonjs/-/plugin-transform-modules-commonjs-7.19.6.tgz",
-      "integrity": "sha512-8PIa1ym4XRTKuSsOUXqDG0YaOlEuTVvHMe5JCfgBMOtHvJKw/4NGovEGN33viISshG/rZNVrACiBmPQLvWN8xQ==",
+      "version": "7.20.11",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-modules-commonjs/-/plugin-transform-modules-commonjs-7.20.11.tgz",
+      "integrity": "sha512-S8e1f7WQ7cimJQ51JkAaDrEtohVEitXjgCGAS2N8S31Y42E+kWwfSz83LYz57QdBm7q9diARVqanIaH2oVgQnw==",
       "dev": true,
       "dependencies": {
-        "@babel/helper-module-transforms": "^7.19.6",
-        "@babel/helper-plugin-utils": "^7.19.0",
-        "@babel/helper-simple-access": "^7.19.4"
+        "@babel/helper-module-transforms": "^7.20.11",
+        "@babel/helper-plugin-utils": "^7.20.2",
+        "@babel/helper-simple-access": "^7.20.2"
       },
       "engines": {
         "node": ">=6.9.0"
@@ -1278,14 +1282,14 @@
       }
     },
     "node_modules/@babel/plugin-transform-modules-systemjs": {
-      "version": "7.19.6",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-modules-systemjs/-/plugin-transform-modules-systemjs-7.19.6.tgz",
-      "integrity": "sha512-fqGLBepcc3kErfR9R3DnVpURmckXP7gj7bAlrTQyBxrigFqszZCkFkcoxzCp2v32XmwXLvbw+8Yq9/b+QqksjQ==",
+      "version": "7.20.11",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-modules-systemjs/-/plugin-transform-modules-systemjs-7.20.11.tgz",
+      "integrity": "sha512-vVu5g9BPQKSFEmvt2TA4Da5N+QVS66EX21d8uoOihC+OCpUoGvzVsXeqFdtAEfVa5BILAeFt+U7yVmLbQnAJmw==",
       "dev": true,
       "dependencies": {
         "@babel/helper-hoist-variables": "^7.18.6",
-        "@babel/helper-module-transforms": "^7.19.6",
-        "@babel/helper-plugin-utils": "^7.19.0",
+        "@babel/helper-module-transforms": "^7.20.11",
+        "@babel/helper-plugin-utils": "^7.20.2",
         "@babel/helper-validator-identifier": "^7.19.1"
       },
       "engines": {
@@ -1359,9 +1363,9 @@
       }
     },
     "node_modules/@babel/plugin-transform-parameters": {
-      "version": "7.20.5",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-parameters/-/plugin-transform-parameters-7.20.5.tgz",
-      "integrity": "sha512-h7plkOmcndIUWXZFLgpbrh2+fXAi47zcUX7IrOQuZdLD0I0KvjJ6cvo3BEcAOsDOcZhVKGJqv07mkSqK0y2isQ==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-parameters/-/plugin-transform-parameters-7.20.7.tgz",
+      "integrity": "sha512-WiWBIkeHKVOSYPO0pWkxGPfKeWrCJyD3NJ53+Lrp/QMSZbsVPovrVl2aWZ19D/LTVnaDv5Ap7GJ/B2CTOZdrfA==",
       "dev": true,
       "dependencies": {
         "@babel/helper-plugin-utils": "^7.20.2"
@@ -1404,16 +1408,16 @@
       }
     },
     "node_modules/@babel/plugin-transform-react-jsx": {
-      "version": "7.19.0",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-react-jsx/-/plugin-transform-react-jsx-7.19.0.tgz",
-      "integrity": "sha512-UVEvX3tXie3Szm3emi1+G63jyw1w5IcMY0FSKM+CRnKRI5Mr1YbCNgsSTwoTwKphQEG9P+QqmuRFneJPZuHNhg==",
+      "version": "7.20.13",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-react-jsx/-/plugin-transform-react-jsx-7.20.13.tgz",
+      "integrity": "sha512-MmTZx/bkUrfJhhYAYt3Urjm+h8DQGrPrnKQ94jLo7NLuOU+T89a7IByhKmrb8SKhrIYIQ0FN0CHMbnFRen4qNw==",
       "dev": true,
       "dependencies": {
         "@babel/helper-annotate-as-pure": "^7.18.6",
         "@babel/helper-module-imports": "^7.18.6",
-        "@babel/helper-plugin-utils": "^7.19.0",
+        "@babel/helper-plugin-utils": "^7.20.2",
         "@babel/plugin-syntax-jsx": "^7.18.6",
-        "@babel/types": "^7.19.0"
+        "@babel/types": "^7.20.7"
       },
       "engines": {
         "node": ">=6.9.0"
@@ -1500,13 +1504,13 @@
       }
     },
     "node_modules/@babel/plugin-transform-spread": {
-      "version": "7.19.0",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-spread/-/plugin-transform-spread-7.19.0.tgz",
-      "integrity": "sha512-RsuMk7j6n+r752EtzyScnWkQyuJdli6LdO5Klv8Yx0OfPVTcQkIUfS8clx5e9yHXzlnhOZF3CbQ8C2uP5j074w==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-spread/-/plugin-transform-spread-7.20.7.tgz",
+      "integrity": "sha512-ewBbHQ+1U/VnH1fxltbJqDeWBU1oNLG8Dj11uIv3xVf7nrQu0bPGe5Rf716r7K5Qz+SqtAOVswoVunoiBtGhxw==",
       "dev": true,
       "dependencies": {
-        "@babel/helper-plugin-utils": "^7.19.0",
-        "@babel/helper-skip-transparent-expression-wrappers": "^7.18.9"
+        "@babel/helper-plugin-utils": "^7.20.2",
+        "@babel/helper-skip-transparent-expression-wrappers": "^7.20.0"
       },
       "engines": {
         "node": ">=6.9.0"
@@ -1561,12 +1565,12 @@
       }
     },
     "node_modules/@babel/plugin-transform-typescript": {
-      "version": "7.20.2",
-      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-typescript/-/plugin-transform-typescript-7.20.2.tgz",
-      "integrity": "sha512-jvS+ngBfrnTUBfOQq8NfGnSbF9BrqlR6hjJ2yVxMkmO5nL/cdifNbI30EfjRlN4g5wYWNnMPyj5Sa6R1pbLeag==",
+      "version": "7.20.13",
+      "resolved": "https://registry.npmjs.org/@babel/plugin-transform-typescript/-/plugin-transform-typescript-7.20.13.tgz",
+      "integrity": "sha512-O7I/THxarGcDZxkgWKMUrk7NK1/WbHAg3Xx86gqS6x9MTrNL6AwIluuZ96ms4xeDe6AVx6rjHbWHP7x26EPQBA==",
       "dev": true,
       "dependencies": {
-        "@babel/helper-create-class-features-plugin": "^7.20.2",
+        "@babel/helper-create-class-features-plugin": "^7.20.12",
         "@babel/helper-plugin-utils": "^7.20.2",
         "@babel/plugin-syntax-typescript": "^7.20.0"
       },
@@ -1751,9 +1755,9 @@
       }
     },
     "node_modules/@babel/runtime": {
-      "version": "7.20.6",
-      "resolved": "https://registry.npmjs.org/@babel/runtime/-/runtime-7.20.6.tgz",
-      "integrity": "sha512-Q+8MqP7TiHMWzSfwiJwXCjyf4GYA4Dgw3emg/7xmwsdLJOZUp+nMqcOwOzzYheuM1rhDu8FSj2l0aoMygEuXuA==",
+      "version": "7.20.13",
+      "resolved": "https://registry.npmjs.org/@babel/runtime/-/runtime-7.20.13.tgz",
+      "integrity": "sha512-gt3PKXs0DBoL9xCvOIIZ2NEqAGZqHjAnmVbfQtB620V0uReIQutpel14KcneZuer7UioY8ALKZ7iocavvzTNFA==",
       "dependencies": {
         "regenerator-runtime": "^0.13.11"
       },
@@ -1762,31 +1766,31 @@
       }
     },
     "node_modules/@babel/template": {
-      "version": "7.18.10",
-      "resolved": "https://registry.npmjs.org/@babel/template/-/template-7.18.10.tgz",
-      "integrity": "sha512-TI+rCtooWHr3QJ27kJxfjutghu44DLnasDMwpDqCXVTal9RLp3RSYNh4NdBrRP2cQAoG9A8juOQl6P6oZG4JxA==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/template/-/template-7.20.7.tgz",
+      "integrity": "sha512-8SegXApWe6VoNw0r9JHpSteLKTpTiLZ4rMlGIm9JQ18KiCtyQiAMEazujAHrUS5flrcqYZa75ukev3P6QmUwUw==",
       "dependencies": {
         "@babel/code-frame": "^7.18.6",
-        "@babel/parser": "^7.18.10",
-        "@babel/types": "^7.18.10"
+        "@babel/parser": "^7.20.7",
+        "@babel/types": "^7.20.7"
       },
       "engines": {
         "node": ">=6.9.0"
       }
     },
     "node_modules/@babel/traverse": {
-      "version": "7.20.5",
-      "resolved": "https://registry.npmjs.org/@babel/traverse/-/traverse-7.20.5.tgz",
-      "integrity": "sha512-WM5ZNN3JITQIq9tFZaw1ojLU3WgWdtkxnhM1AegMS+PvHjkM5IXjmYEGY7yukz5XS4sJyEf2VzWjI8uAavhxBQ==",
+      "version": "7.20.13",
+      "resolved": "https://registry.npmjs.org/@babel/traverse/-/traverse-7.20.13.tgz",
+      "integrity": "sha512-kMJXfF0T6DIS9E8cgdLCSAL+cuCK+YEZHWiLK0SXpTo8YRj5lpJu3CDNKiIBCne4m9hhTIqUg6SYTAI39tAiVQ==",
       "dependencies": {
         "@babel/code-frame": "^7.18.6",
-        "@babel/generator": "^7.20.5",
+        "@babel/generator": "^7.20.7",
         "@babel/helper-environment-visitor": "^7.18.9",
         "@babel/helper-function-name": "^7.19.0",
         "@babel/helper-hoist-variables": "^7.18.6",
         "@babel/helper-split-export-declaration": "^7.18.6",
-        "@babel/parser": "^7.20.5",
-        "@babel/types": "^7.20.5",
+        "@babel/parser": "^7.20.13",
+        "@babel/types": "^7.20.7",
         "debug": "^4.1.0",
         "globals": "^11.1.0"
       },
@@ -1795,9 +1799,9 @@
       }
     },
     "node_modules/@babel/types": {
-      "version": "7.20.5",
-      "resolved": "https://registry.npmjs.org/@babel/types/-/types-7.20.5.tgz",
-      "integrity": "sha512-c9fst/h2/dcF7H+MJKZ2T0KjEQ8hY/BNnDk/H3XY8C4Aw/eWQXWn/lWntHF9ooUBnGmEvbfGrTgLWc+um0YDUg==",
+      "version": "7.20.7",
+      "resolved": "https://registry.npmjs.org/@babel/types/-/types-7.20.7.tgz",
+      "integrity": "sha512-69OnhBxSSgK0OzTJai4kyPDiKTIe3j+ctaHdIGVbRahTLAT7L3R9oeXHC2aVSuGYt3cVnoAMDmOCgJ2yaiLMvg==",
       "dependencies": {
         "@babel/helper-string-parser": "^7.19.4",
         "@babel/helper-validator-identifier": "^7.19.1",
@@ -1967,9 +1971,9 @@
       "integrity": "sha512-CnD7zLItIzt86q4Sj3kZUiLcBk1dSk81qcqgMGaZe7SQ1P8hFNxhMl5AZthK1zrDM5m74VVhaOpuMGIL4gagaA=="
     },
     "node_modules/@fontsource/roboto-mono": {
-      "version": "4.5.8",
-      "resolved": "https://registry.npmjs.org/@fontsource/roboto-mono/-/roboto-mono-4.5.8.tgz",
-      "integrity": "sha512-AW44UkbQD0w1CT5mzDbsvhGZ6/bb0YmZzoELj6Sx8vcVEzcbYGUdt2Dtl5zqlOuYMWQFY1mniwWyVv+Bm/lVxw=="
+      "version": "4.5.10",
+      "resolved": "https://registry.npmjs.org/@fontsource/roboto-mono/-/roboto-mono-4.5.10.tgz",
+      "integrity": "sha512-KrJdmkqz6DszT2wV/bbhXef4r0hV3B0vw2mAqei8A2kRnvq+gcJLmmIeQ94vu9VEXrUQzos5M9lH1TAAXpRphw=="
     },
     "node_modules/@fortawesome/fontawesome-common-types": {
       "version": "6.2.1",
@@ -2083,11 +2087,11 @@
       }
     },
     "node_modules/@leanprover/infoview": {
-      "version": "0.4.1",
-      "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.4.1.tgz",
-      "integrity": "sha512-hdwIybZZqlpb2poOyWqfRfMqzI5pyE0gIWG5ahTVB/IWww0pWIh2gilZ+i/xC6Y/nfUKBQkR1svJDtPrKMR6Jg==",
+      "version": "0.4.2",
+      "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.4.2.tgz",
+      "integrity": "sha512-Bj+q/7n1xlnpRd4xsJ75uikZPwW5id/G4G1JPqhbbfMacTwAgzLNFaqJhzBrIUuF5nxJYGKRqRIeFtkalGxJ0g==",
       "dependencies": {
-        "@leanprover/infoview-api": "~0.2.0",
+        "@leanprover/infoview-api": "~0.2.1",
         "@vscode/codicons": "^0.0.32",
         "es-module-shims": "^1.6.2",
         "marked": "^4.2.2",
@@ -2108,14 +2112,14 @@
       "dev": true
     },
     "node_modules/@mui/base": {
-      "version": "5.0.0-alpha.111",
-      "resolved": "https://registry.npmjs.org/@mui/base/-/base-5.0.0-alpha.111.tgz",
-      "integrity": "sha512-2wfIPpl97S4dPzD0QOM3UIzQ/EuXCYQvHmXxTpfKxev/cfkzOe7Ik/McoYUBbtM1bSOqH3W276R/L2LF9cyXqQ==",
+      "version": "5.0.0-alpha.116",
+      "resolved": "https://registry.npmjs.org/@mui/base/-/base-5.0.0-alpha.116.tgz",
+      "integrity": "sha512-VwhifWdrfHc4/ZdqRZ4Gf+7P39sovNN24By1YVZdvJ9fvp0Sr8sNftGUCjYXXz+xCXVBQDXvhfxMwZrj2MvJvA==",
       "dependencies": {
-        "@babel/runtime": "^7.20.6",
+        "@babel/runtime": "^7.20.7",
         "@emotion/is-prop-valid": "^1.2.0",
         "@mui/types": "^7.2.3",
-        "@mui/utils": "^5.11.1",
+        "@mui/utils": "^5.11.7",
         "@popperjs/core": "^2.11.6",
         "clsx": "^1.2.1",
         "prop-types": "^15.8.1",
@@ -2140,9 +2144,9 @@
       }
     },
     "node_modules/@mui/core-downloads-tracker": {
-      "version": "5.11.1",
-      "resolved": "https://registry.npmjs.org/@mui/core-downloads-tracker/-/core-downloads-tracker-5.11.1.tgz",
-      "integrity": "sha512-QVqVNlZ2K+LqUDE5kFgYd0r4KekR/dv2cNYbAutQWbfOA8VPVUVrDz0ELrEcoe8TjM/CwnsmGvaDh/YSNl/ALA==",
+      "version": "5.11.7",
+      "resolved": "https://registry.npmjs.org/@mui/core-downloads-tracker/-/core-downloads-tracker-5.11.7.tgz",
+      "integrity": "sha512-lZgX7XQTk0zVcpwEa80r+T4y09dosnUxWvFPSikU/2Hh5wnyNOek8WfJwGCNsaRiXJHMi5eHY+z8oku4u5lgNw==",
       "funding": {
         "type": "opencollective",
         "url": "https://opencollective.com/mui"
@@ -2174,16 +2178,16 @@
       }
     },
     "node_modules/@mui/material": {
-      "version": "5.11.1",
-      "resolved": "https://registry.npmjs.org/@mui/material/-/material-5.11.1.tgz",
-      "integrity": "sha512-yaZiXvcrl2vgUK+VO24780BWRgwdAMmAyuMVZnRTts1Yu0tWd6PjIYq2ZtaOlpj6/LbaSS+Q2kSfxYnDQ20CEQ==",
-      "dependencies": {
-        "@babel/runtime": "^7.20.6",
-        "@mui/base": "5.0.0-alpha.111",
-        "@mui/core-downloads-tracker": "^5.11.1",
-        "@mui/system": "^5.11.1",
+      "version": "5.11.7",
+      "resolved": "https://registry.npmjs.org/@mui/material/-/material-5.11.7.tgz",
+      "integrity": "sha512-wDv7Pc6kMe9jeWkmCLt4JChd1lPc2u23JQHpB35L2VwQowpNFoDfIwqi0sYCnZTMKlRc7lza8LqwSwHl2G52Rw==",
+      "dependencies": {
+        "@babel/runtime": "^7.20.7",
+        "@mui/base": "5.0.0-alpha.116",
+        "@mui/core-downloads-tracker": "^5.11.7",
+        "@mui/system": "^5.11.7",
         "@mui/types": "^7.2.3",
-        "@mui/utils": "^5.11.1",
+        "@mui/utils": "^5.11.7",
         "@types/react-transition-group": "^4.4.5",
         "clsx": "^1.2.1",
         "csstype": "^3.1.1",
@@ -2218,12 +2222,12 @@
       }
     },
     "node_modules/@mui/private-theming": {
-      "version": "5.11.1",
-      "resolved": "https://registry.npmjs.org/@mui/private-theming/-/private-theming-5.11.1.tgz",
-      "integrity": "sha512-nnHg7kA5RwFRhy0wiDYe59sLCVGORpPypL1JcEdhv0+N0Zbmc2E/y4z2zqMRZ62MAEscpro7cQbvv244ThA84A==",
+      "version": "5.11.7",
+      "resolved": "https://registry.npmjs.org/@mui/private-theming/-/private-theming-5.11.7.tgz",
+      "integrity": "sha512-XzRTSZdc8bhuUdjablTNv3kFkZ/XIMlKkOqqJCU0G8W3tWGXpau2DXkafPd1ddjPhF9zF3qLKNGgKCChYItjgA==",
       "dependencies": {
-        "@babel/runtime": "^7.20.6",
-        "@mui/utils": "^5.11.1",
+        "@babel/runtime": "^7.20.7",
+        "@mui/utils": "^5.11.7",
         "prop-types": "^15.8.1"
       },
       "engines": {
@@ -2275,15 +2279,15 @@
       }
     },
     "node_modules/@mui/system": {
-      "version": "5.11.1",
-      "resolved": "https://registry.npmjs.org/@mui/system/-/system-5.11.1.tgz",
-      "integrity": "sha512-BEA2S0hay8n8CcZftkeAVsi0nsb5ZjdnZRCahv5lX7QJYwDjO4ucJ6lnvxHe2v/9Te1LLjTO7ojxu/qM6CE5Cg==",
+      "version": "5.11.7",
+      "resolved": "https://registry.npmjs.org/@mui/system/-/system-5.11.7.tgz",
+      "integrity": "sha512-uGB6hBxGlAdlmbLdTtUZYNPXkgQGGnKxHdkRATqsu7UlCxNsc/yS5NCEWy/3c4pnelD1LDLD39WrntP9mwhfkQ==",
       "dependencies": {
-        "@babel/runtime": "^7.20.6",
-        "@mui/private-theming": "^5.11.1",
+        "@babel/runtime": "^7.20.7",
+        "@mui/private-theming": "^5.11.7",
         "@mui/styled-engine": "^5.11.0",
         "@mui/types": "^7.2.3",
-        "@mui/utils": "^5.11.1",
+        "@mui/utils": "^5.11.7",
         "clsx": "^1.2.1",
         "csstype": "^3.1.1",
         "prop-types": "^15.8.1"
@@ -2327,11 +2331,11 @@
       }
     },
     "node_modules/@mui/utils": {
-      "version": "5.11.1",
-      "resolved": "https://registry.npmjs.org/@mui/utils/-/utils-5.11.1.tgz",
-      "integrity": "sha512-lMAPgIJoil8V9ZxsMbEflMsvZmWcHbRVMc4JDY9jPO9V4welpF43h/O267b1RqlcRnC5MEbVQV605GYkTZY29Q==",
+      "version": "5.11.7",
+      "resolved": "https://registry.npmjs.org/@mui/utils/-/utils-5.11.7.tgz",
+      "integrity": "sha512-8uyNDeVHZA804Ego20Erv8TpxlbqTe/EbhTI2H1UYr4/RiIbBprat8W4Qqr2UQIsC/b3DLz+0RQ6R/E5BxEcLA==",
       "dependencies": {
-        "@babel/runtime": "^7.20.6",
+        "@babel/runtime": "^7.20.7",
         "@types/prop-types": "^15.7.5",
         "@types/react-is": "^16.7.1 || ^17.0.0",
         "prop-types": "^15.8.1",
@@ -2455,9 +2459,9 @@
       }
     },
     "node_modules/@reduxjs/toolkit": {
-      "version": "1.9.1",
-      "resolved": "https://registry.npmjs.org/@reduxjs/toolkit/-/toolkit-1.9.1.tgz",
-      "integrity": "sha512-HikrdY+IDgRfRYlCTGUQaiCxxDDgM1mQrRbZ6S1HFZX5ZYuJ4o8EstNmhTwHdPl2rTmLxzwSu0b3AyeyTlR+RA==",
+      "version": "1.9.2",
+      "resolved": "https://registry.npmjs.org/@reduxjs/toolkit/-/toolkit-1.9.2.tgz",
+      "integrity": "sha512-5ZAZ7hwAKWSii5T6NTPmgIBUqyVdlDs+6JjThz6J6dmHLDm6zCzv2OjHIFAi3Vvs1qjmXU0bm6eBojukYXjVMQ==",
       "dependencies": {
         "immer": "^9.0.16",
         "redux": "^4.2.0",
@@ -2478,22 +2482,22 @@
       }
     },
     "node_modules/@remix-run/router": {
-      "version": "1.1.0",
-      "resolved": "https://registry.npmjs.org/@remix-run/router/-/router-1.1.0.tgz",
-      "integrity": "sha512-rGl+jH/7x1KBCQScz9p54p0dtPLNeKGb3e0wD2H5/oZj41bwQUnXdzbj2TbUAFhvD7cp9EyEQA4dEgpUFa1O7Q==",
+      "version": "1.3.1",
+      "resolved": "https://registry.npmjs.org/@remix-run/router/-/router-1.3.1.tgz",
+      "integrity": "sha512-+eun1Wtf72RNRSqgU7qM2AMX/oHp+dnx7BHk1qhK5ZHzdHTUU4LA1mGG1vT+jMc8sbhG3orvsfOmryjzx2PzQw==",
       "engines": {
         "node": ">=14"
       }
     },
     "node_modules/@testing-library/dom": {
-      "version": "8.19.0",
-      "resolved": "https://registry.npmjs.org/@testing-library/dom/-/dom-8.19.0.tgz",
-      "integrity": "sha512-6YWYPPpxG3e/xOo6HIWwB/58HukkwIVTOaZ0VwdMVjhRUX/01E4FtQbck9GazOOj7MXHc5RBzMrU86iBJHbI+A==",
+      "version": "8.20.0",
+      "resolved": "https://registry.npmjs.org/@testing-library/dom/-/dom-8.20.0.tgz",
+      "integrity": "sha512-d9ULIT+a4EXLX3UU8FBjauG9NnsZHkHztXoIcTsOKoOw030fyjheN9svkTULjJxtYag9DZz5Jz5qkWZDPxTFwA==",
       "dev": true,
       "dependencies": {
         "@babel/code-frame": "^7.10.4",
         "@babel/runtime": "^7.12.5",
-        "@types/aria-query": "^4.2.0",
+        "@types/aria-query": "^5.0.1",
         "aria-query": "^5.0.0",
         "chalk": "^4.1.0",
         "dom-accessibility-api": "^0.5.9",
@@ -2593,9 +2597,9 @@
       }
     },
     "node_modules/@types/aria-query": {
-      "version": "4.2.2",
-      "resolved": "https://registry.npmjs.org/@types/aria-query/-/aria-query-4.2.2.tgz",
-      "integrity": "sha512-HnYpAE1Y6kRyKM/XkEuiRQhTHvkzMBurTHnpFLYLBGPIylZNPs9jJcuOOYWxPLJCSEtmZT0Y8rHDokKN7rRTig==",
+      "version": "5.0.1",
+      "resolved": "https://registry.npmjs.org/@types/aria-query/-/aria-query-5.0.1.tgz",
+      "integrity": "sha512-XTIieEY+gvJ39ChLcB4If5zHtPxt3Syj5rgZR+e1ctpmK8NjPf0zFqsz4JpLJT0xla9GFDKjy8Cpu331nrmE1Q==",
       "dev": true
     },
     "node_modules/@types/body-parser": {
@@ -2650,9 +2654,9 @@
       }
     },
     "node_modules/@types/eslint": {
-      "version": "8.4.10",
-      "resolved": "https://registry.npmjs.org/@types/eslint/-/eslint-8.4.10.tgz",
-      "integrity": "sha512-Sl/HOqN8NKPmhWo2VBEPm0nvHnu2LL3v9vKo8MEq0EtbJ4eVzGPl41VNPvn5E1i5poMk4/XD8UriLHpJvEP/Nw==",
+      "version": "8.21.0",
+      "resolved": "https://registry.npmjs.org/@types/eslint/-/eslint-8.21.0.tgz",
+      "integrity": "sha512-35EhHNOXgxnUgh4XCJsGhE7zdlDhYDN/aMG6UbkByCFFNgQ7b3U+uVoqBpicFydR8JEfgdjCF7SJ7MiJfzuiTA==",
       "dev": true,
       "dependencies": {
         "@types/estree": "*",
@@ -2676,21 +2680,21 @@
       "dev": true
     },
     "node_modules/@types/express": {
-      "version": "4.17.15",
-      "resolved": "https://registry.npmjs.org/@types/express/-/express-4.17.15.tgz",
-      "integrity": "sha512-Yv0k4bXGOH+8a+7bELd2PqHQsuiANB+A8a4gnQrkRWzrkKlb6KHaVvyXhqs04sVW/OWlbPyYxRgYlIXLfrufMQ==",
+      "version": "4.17.17",
+      "resolved": "https://registry.npmjs.org/@types/express/-/express-4.17.17.tgz",
+      "integrity": "sha512-Q4FmmuLGBG58btUnfS1c1r/NQdlp3DMfGDGig8WhfpA2YRUtEkxAjkZb0yvplJGYdF1fsQ81iMDcH24sSCNC/Q==",
       "dev": true,
       "dependencies": {
         "@types/body-parser": "*",
-        "@types/express-serve-static-core": "^4.17.31",
+        "@types/express-serve-static-core": "^4.17.33",
         "@types/qs": "*",
         "@types/serve-static": "*"
       }
     },
     "node_modules/@types/express-serve-static-core": {
-      "version": "4.17.31",
-      "resolved": "https://registry.npmjs.org/@types/express-serve-static-core/-/express-serve-static-core-4.17.31.tgz",
-      "integrity": "sha512-DxMhY+NAsTwMMFHBTtJFNp5qiHKJ7TeqOo23zVEM9alT1Ml27Q3xcTH0xwxn7Q0BbMcVEJOs/7aQtUWupUQN3Q==",
+      "version": "4.17.33",
+      "resolved": "https://registry.npmjs.org/@types/express-serve-static-core/-/express-serve-static-core-4.17.33.tgz",
+      "integrity": "sha512-TPBqmR/HRYI3eC2E5hmiivIzv+bidAfXofM+sbonAGvyDhySGw9/PQZFt2BLOrjUUR++4eJVpx6KnLQK1Fk9tA==",
       "dev": true,
       "dependencies": {
         "@types/node": "*",
@@ -2760,9 +2764,9 @@
       "integrity": "sha512-iiUgKzV9AuaEkZqkOLDIvlQiL6ltuZd9tGcW3gwpnX8JbuiuhFlEGmmFXEXkN50Cvq7Os88IY2v0dkDqXYWVgA=="
     },
     "node_modules/@types/node": {
-      "version": "18.11.17",
-      "resolved": "https://registry.npmjs.org/@types/node/-/node-18.11.17.tgz",
-      "integrity": "sha512-HJSUJmni4BeDHhfzn6nF0sVmd1SMezP7/4F0Lq+aXzmp2xm9O7WXrUtHW/CHlYVtZUbByEvWidHqRtcJXGF2Ng==",
+      "version": "18.11.19",
+      "resolved": "https://registry.npmjs.org/@types/node/-/node-18.11.19.tgz",
+      "integrity": "sha512-YUgMWAQBWLObABqrvx8qKO1enAvBUdjZOAWQ5grBAkp5LQv45jBvYKZ3oFS9iKRCQyFjqw6iuEa1vmFqtxYLZw==",
       "dev": true
     },
     "node_modules/@types/parse-json": {
@@ -2770,11 +2774,6 @@
       "resolved": "https://registry.npmjs.org/@types/parse-json/-/parse-json-4.0.0.tgz",
       "integrity": "sha512-//oorEZjL6sbPcKUaCdIGlIUeH26mgzimjBB77G6XRgnDl/L5wOnpyBGRe/Mmf5CVW3PwEBE1NjiMZ/ssFh4wA=="
     },
-    "node_modules/@types/parse5": {
-      "version": "6.0.3",
-      "resolved": "https://registry.npmjs.org/@types/parse5/-/parse5-6.0.3.tgz",
-      "integrity": "sha512-SuT16Q1K51EAVPz1K29DJ/sXjhSQ0zjvsypYJ6tlwVsRV9jwW5Adq2ch8Dq8kDBCkYnELS7N7VNCSB5nC56t/g=="
-    },
     "node_modules/@types/prop-types": {
       "version": "15.7.5",
       "resolved": "https://registry.npmjs.org/@types/prop-types/-/prop-types-15.7.5.tgz",
@@ -2793,9 +2792,9 @@
       "dev": true
     },
     "node_modules/@types/react": {
-      "version": "18.0.26",
-      "resolved": "https://registry.npmjs.org/@types/react/-/react-18.0.26.tgz",
-      "integrity": "sha512-hCR3PJQsAIXyxhTNSiDFY//LhnMZWpNNr5etoCqx/iUfGc5gXWtQR2Phl908jVR6uPXacojQWTg4qRpkxTuGug==",
+      "version": "18.0.27",
+      "resolved": "https://registry.npmjs.org/@types/react/-/react-18.0.27.tgz",
+      "integrity": "sha512-3vtRKHgVxu3Jp9t718R9BuzoD4NcQ8YJ5XRzsSKxNDiDonD2MXIT1TmSkenxuCycZJoQT5d2vE8LwWJxBC1gmA==",
       "dependencies": {
         "@types/prop-types": "*",
         "@types/scheduler": "*",
@@ -2803,9 +2802,9 @@
       }
     },
     "node_modules/@types/react-dom": {
-      "version": "18.0.9",
-      "resolved": "https://registry.npmjs.org/@types/react-dom/-/react-dom-18.0.9.tgz",
-      "integrity": "sha512-qnVvHxASt/H7i+XG1U1xMiY5t+IHcPGUK7TDMDzom08xa7e86eCeKOiLZezwCKVxJn6NEiiy2ekgX8aQssjIKg==",
+      "version": "18.0.10",
+      "resolved": "https://registry.npmjs.org/@types/react-dom/-/react-dom-18.0.10.tgz",
+      "integrity": "sha512-E42GW/JA4Qv15wQdqJq8DL4JhNpB3prJgjgapN3qJT9K2zO5IIAQh4VXvCEDupoqAwnz0cY4RlXeC/ajX5SFHg==",
       "devOptional": true,
       "dependencies": {
         "@types/react": "*"
@@ -2820,9 +2819,9 @@
       }
     },
     "node_modules/@types/react-router": {
-      "version": "5.1.19",
-      "resolved": "https://registry.npmjs.org/@types/react-router/-/react-router-5.1.19.tgz",
-      "integrity": "sha512-Fv/5kb2STAEMT3wHzdKQK2z8xKq38EDIGVrutYLmQVVLe+4orDFquU52hQrULnEHinMKv9FSA6lf9+uNT1ITtA==",
+      "version": "5.1.20",
+      "resolved": "https://registry.npmjs.org/@types/react-router/-/react-router-5.1.20.tgz",
+      "integrity": "sha512-jGjmu/ZqS7FjSH6owMcD5qpq19+1RS9DeVRqfl1FeBMxTDQAGwlMWOcs52NDoXaNKyG3d1cYQFMs9rCrb88o9Q==",
       "dependencies": {
         "@types/history": "^4.7.11",
         "@types/react": "*"
@@ -2896,9 +2895,9 @@
       "integrity": "sha512-EwmlvuaxPNej9+T4v5AuBPJa2x2UOJVdjCtDHgcDqitUeOtjnJKJ+apYjVcAoBEMjKW1VVFGZLUb5+qqa09XFA=="
     },
     "node_modules/@types/ws": {
-      "version": "8.5.3",
-      "resolved": "https://registry.npmjs.org/@types/ws/-/ws-8.5.3.tgz",
-      "integrity": "sha512-6YOoWjruKj1uLf3INHH7D3qTXwFfEsg1kf3c0uDdSBJwfa/llkwIjrAGV7j7mVgGNbzTQ3HiHKKDXl6bJPD97w==",
+      "version": "8.5.4",
+      "resolved": "https://registry.npmjs.org/@types/ws/-/ws-8.5.4.tgz",
+      "integrity": "sha512-zdQDHKUgcX/zBc4GrwsE/7dVdAD8JR4EuiAXiiUhhfyIJXXb2+PrGshFyeXWQPMmmZ2XxgaqclgpIC7eTXc1mg==",
       "dev": true,
       "dependencies": {
         "@types/node": "*"
@@ -3122,9 +3121,9 @@
       }
     },
     "node_modules/acorn": {
-      "version": "8.8.1",
-      "resolved": "https://registry.npmjs.org/acorn/-/acorn-8.8.1.tgz",
-      "integrity": "sha512-7zFpHzhnqYKrkYdUjF1HI1bzd0VygEGX8lFk4k5zVMqHEoES+P+7TKI+EvLO9WVMJ8eekdO0aDEK044xTXwPPA==",
+      "version": "8.8.2",
+      "resolved": "https://registry.npmjs.org/acorn/-/acorn-8.8.2.tgz",
+      "integrity": "sha512-xjIYgE8HBrkpd/sJqOGNspf8uHG+NOHGOw6a/Urj8taM2EXfdNAH2oFcPeIFfsv3+kz/mJrS5VuMqbNLjCa2vw==",
       "dev": true,
       "bin": {
         "acorn": "bin/acorn"
@@ -3176,9 +3175,9 @@
       }
     },
     "node_modules/ajv-formats/node_modules/ajv": {
-      "version": "8.11.2",
-      "resolved": "https://registry.npmjs.org/ajv/-/ajv-8.11.2.tgz",
-      "integrity": "sha512-E4bfmKAhGiSTvMfL1Myyycaub+cUEU2/IvpylXkUu7CHBkBj1f/ikdzbD7YQ6FKUbixDxeYvB/xY4fvyroDlQg==",
+      "version": "8.12.0",
+      "resolved": "https://registry.npmjs.org/ajv/-/ajv-8.12.0.tgz",
+      "integrity": "sha512-sRu1kpcO9yLtYxBKvqfTeh9KzZEwO3STyX1HT+4CaDzC6HpTGYhIhPIzj9XuKU7KYDwnaeh5hcOwjy1QuJzBPA==",
       "dev": true,
       "dependencies": {
         "fast-deep-equal": "^3.1.1",
@@ -3465,9 +3464,9 @@
       "integrity": "sha512-Tpp60P6IUJDTuOq/5Z8cdskzJujfwqfOTkrwIwj7IRISpnkJnT6SyJ4PCPnGMoFjC9ddhal5KVIYtAt97ix05A=="
     },
     "node_modules/bonjour-service": {
-      "version": "1.0.14",
-      "resolved": "https://registry.npmjs.org/bonjour-service/-/bonjour-service-1.0.14.tgz",
-      "integrity": "sha512-HIMbgLnk1Vqvs6B4Wq5ep7mxvj9sGz5d1JJyDNSGNIdA/w2MCz6GTjWTdjqOJV1bEPj+6IkxDvWNFKEBxNt4kQ==",
+      "version": "1.1.0",
+      "resolved": "https://registry.npmjs.org/bonjour-service/-/bonjour-service-1.1.0.tgz",
+      "integrity": "sha512-LVRinRB3k1/K0XzZ2p58COnWvkQknIY6sf0zF2rpErvcJXpMBttEPQSxK+HEXSS9VmpZlDoDnQWv8ftJT20B0Q==",
       "dev": true,
       "dependencies": {
         "array-flatten": "^2.1.2",
@@ -3509,9 +3508,9 @@
       }
     },
     "node_modules/browserslist": {
-      "version": "4.21.4",
-      "resolved": "https://registry.npmjs.org/browserslist/-/browserslist-4.21.4.tgz",
-      "integrity": "sha512-CBHJJdDmgjl3daYjN5Cp5kbTf1mUhZoS+beLklHIvkOWscs83YAhLlF3Wsh/lciQYAcbBJgTOD44VtG31ZM4Hw==",
+      "version": "4.21.5",
+      "resolved": "https://registry.npmjs.org/browserslist/-/browserslist-4.21.5.tgz",
+      "integrity": "sha512-tUkiguQGW7S3IhB7N+c2MV/HZPSCPAAiYBZXLsBhFB/PCy6ZKKsZrmBayHV9fdGV/ARIfJ14NkxKzRDjvp7L6w==",
       "funding": [
         {
           "type": "opencollective",
@@ -3523,10 +3522,10 @@
         }
       ],
       "dependencies": {
-        "caniuse-lite": "^1.0.30001400",
-        "electron-to-chromium": "^1.4.251",
-        "node-releases": "^2.0.6",
-        "update-browserslist-db": "^1.0.9"
+        "caniuse-lite": "^1.0.30001449",
+        "electron-to-chromium": "^1.4.284",
+        "node-releases": "^2.0.8",
+        "update-browserslist-db": "^1.0.10"
       },
       "bin": {
         "browserslist": "cli.js"
@@ -3575,9 +3574,9 @@
       }
     },
     "node_modules/caniuse-lite": {
-      "version": "1.0.30001439",
-      "resolved": "https://registry.npmjs.org/caniuse-lite/-/caniuse-lite-1.0.30001439.tgz",
-      "integrity": "sha512-1MgUzEkoMO6gKfXflStpYgZDlFM7M/ck/bgfVCACO5vnAf0fXoNVHdWtqGU+MYca+4bL9Z5bpOVmR33cWW9G2A==",
+      "version": "1.0.30001450",
+      "resolved": "https://registry.npmjs.org/caniuse-lite/-/caniuse-lite-1.0.30001450.tgz",
+      "integrity": "sha512-qMBmvmQmFXaSxexkjjfMvD5rnDL0+m+dUMZKoDYsGG8iZN29RuYh9eRoMvKsT6uMAWlyUUGDEQGJJYjzCIO9ew==",
       "funding": [
         {
           "type": "opencollective",
@@ -3983,9 +3982,9 @@
       }
     },
     "node_modules/content-type": {
-      "version": "1.0.4",
-      "resolved": "https://registry.npmjs.org/content-type/-/content-type-1.0.4.tgz",
-      "integrity": "sha512-hIP3EEPs8tB9AT1L+NUqtwOAps4mk2Zob89MWXMHjHWg9milF/j4osnnQLXBCBFBk/tvIG/tUc9mOUJiPBhPXA==",
+      "version": "1.0.5",
+      "resolved": "https://registry.npmjs.org/content-type/-/content-type-1.0.5.tgz",
+      "integrity": "sha512-nTjqfcBFEipKdXCv4YDQWCfmcLZKm81ldF0pAopTvyrFGVbcR6P/VAAd5G7N+0tTr8QqiU0tFadD6FK4NtJwOA==",
       "engines": {
         "node": ">= 0.6"
       }
@@ -4009,9 +4008,9 @@
       "integrity": "sha512-QADzlaHc8icV8I7vbaJXJwod9HWYp8uCqf1xa4OfNu1T7JVxQIrUgOWtHdNDtPiywmFbiS12VjotIXLrKM3orQ=="
     },
     "node_modules/core-js-compat": {
-      "version": "3.26.1",
-      "resolved": "https://registry.npmjs.org/core-js-compat/-/core-js-compat-3.26.1.tgz",
-      "integrity": "sha512-622/KzTudvXCDLRw70iHW4KKs1aGpcRcowGWyYJr2DEBfRrd6hNJybxSWJFuZYD4ma86xhrwDDHxmDaIq4EA8A==",
+      "version": "3.27.2",
+      "resolved": "https://registry.npmjs.org/core-js-compat/-/core-js-compat-3.27.2.tgz",
+      "integrity": "sha512-welaYuF7ZtbYKGrIy7y3eb40d37rG1FvzEOfe7hSLd2iD6duMDqUhRfSvCGyC46HhR6Y8JXXdZ2lnRUMkPBpvg==",
       "dev": true,
       "dependencies": {
         "browserslist": "^4.21.4"
@@ -4022,9 +4021,9 @@
       }
     },
     "node_modules/core-js-pure": {
-      "version": "3.26.1",
-      "resolved": "https://registry.npmjs.org/core-js-pure/-/core-js-pure-3.26.1.tgz",
-      "integrity": "sha512-VVXcDpp/xJ21KdULRq/lXdLzQAtX7+37LzpyfFM973il0tWSsDEoyzG38G14AjTpK9VTfiNM9jnFauq/CpaWGQ==",
+      "version": "3.27.2",
+      "resolved": "https://registry.npmjs.org/core-js-pure/-/core-js-pure-3.27.2.tgz",
+      "integrity": "sha512-Cf2jqAbXgWH3VVzjyaaFkY1EBazxugUepGymDoeteyYr9ByX51kD2jdHZlsEF/xnJMyN3Prua7mQuzwMg6Zc9A==",
       "dev": true,
       "hasInstallScript": true,
       "funding": {
@@ -4239,17 +4238,19 @@
       }
     },
     "node_modules/deep-equal": {
-      "version": "2.1.0",
-      "resolved": "https://registry.npmjs.org/deep-equal/-/deep-equal-2.1.0.tgz",
-      "integrity": "sha512-2pxgvWu3Alv1PoWEyVg7HS8YhGlUFUV7N5oOvfL6d+7xAmLSemMwv/c8Zv/i9KFzxV5Kt5CAvQc70fLwVuf4UA==",
+      "version": "2.2.0",
+      "resolved": "https://registry.npmjs.org/deep-equal/-/deep-equal-2.2.0.tgz",
+      "integrity": "sha512-RdpzE0Hv4lhowpIUKKMJfeH6C1pXdtT1/it80ubgWqwI3qpuxUBpC1S4hnHg+zjnuOoDkzUtUCEEkG+XG5l3Mw==",
       "dev": true,
       "dependencies": {
         "call-bind": "^1.0.2",
         "es-get-iterator": "^1.1.2",
         "get-intrinsic": "^1.1.3",
         "is-arguments": "^1.1.1",
+        "is-array-buffer": "^3.0.1",
         "is-date-object": "^1.0.5",
         "is-regex": "^1.1.4",
+        "is-shared-array-buffer": "^1.0.2",
         "isarray": "^2.0.5",
         "object-is": "^1.1.5",
         "object-keys": "^1.1.1",
@@ -4258,7 +4259,7 @@
         "side-channel": "^1.0.4",
         "which-boxed-primitive": "^1.0.2",
         "which-collection": "^1.0.1",
-        "which-typed-array": "^1.1.8"
+        "which-typed-array": "^1.1.9"
       },
       "funding": {
         "url": "https://github.com/sponsors/ljharb"
@@ -4359,9 +4360,9 @@
       }
     },
     "node_modules/dom-accessibility-api": {
-      "version": "0.5.14",
-      "resolved": "https://registry.npmjs.org/dom-accessibility-api/-/dom-accessibility-api-0.5.14.tgz",
-      "integrity": "sha512-NMt+m9zFMPZe0JcY9gN224Qvk6qLIdqex29clBvc/y75ZBX9YA9wNK3frsYvu2DI1xcCIwxwnX+TlsJ2DSOADg==",
+      "version": "0.5.16",
+      "resolved": "https://registry.npmjs.org/dom-accessibility-api/-/dom-accessibility-api-0.5.16.tgz",
+      "integrity": "sha512-X7BJ2yElsnOJ30pZF4uIIDfBEVgF4XEBxL9Bxhy6dnrm5hkzqmsWHGTiHqRiITNhMyFLyAiWndIJP7Z1NTteDg==",
       "dev": true
     },
     "node_modules/dom-helpers": {
@@ -4430,9 +4431,9 @@
       "integrity": "sha512-WMwm9LhRUo+WUaRN+vRuETqG89IgZphVSNkdFgeb6sS/E4OrDIN7t48CAewSHXc6C8lefD8KKfr5vY61brQlow=="
     },
     "node_modules/electron-to-chromium": {
-      "version": "1.4.284",
-      "resolved": "https://registry.npmjs.org/electron-to-chromium/-/electron-to-chromium-1.4.284.tgz",
-      "integrity": "sha512-M8WEXFuKXMYMVr45fo8mq0wUrrJHheiKZf6BArTKk9ZBYCKJEOU5H8cdWgDT+qCVZf7Na4lVUaZsA+h6uA9+PA=="
+      "version": "1.4.286",
+      "resolved": "https://registry.npmjs.org/electron-to-chromium/-/electron-to-chromium-1.4.286.tgz",
+      "integrity": "sha512-Vp3CVhmYpgf4iXNKAucoQUDcCrBQX3XLBtwgFqP9BUXuucgvAV9zWp1kYU7LL9j4++s9O+12cb3wMtN4SJy6UQ=="
     },
     "node_modules/emoji-regex": {
       "version": "8.0.0",
@@ -4511,19 +4512,20 @@
       }
     },
     "node_modules/es-get-iterator": {
-      "version": "1.1.2",
-      "resolved": "https://registry.npmjs.org/es-get-iterator/-/es-get-iterator-1.1.2.tgz",
-      "integrity": "sha512-+DTO8GYwbMCwbywjimwZMHp8AuYXOS2JZFWoi2AlPOS3ebnII9w/NLpNZtA7A0YLaVDw+O7KFCeoIV7OPvM7hQ==",
+      "version": "1.1.3",
+      "resolved": "https://registry.npmjs.org/es-get-iterator/-/es-get-iterator-1.1.3.tgz",
+      "integrity": "sha512-sPZmqHBe6JIiTfN5q2pEi//TwxmAFHwj/XEuYjTuse78i8KxaqMTTzxPoFKuzRpDpTJ+0NAbpfenkmH2rePtuw==",
       "dev": true,
       "dependencies": {
         "call-bind": "^1.0.2",
-        "get-intrinsic": "^1.1.0",
-        "has-symbols": "^1.0.1",
-        "is-arguments": "^1.1.0",
+        "get-intrinsic": "^1.1.3",
+        "has-symbols": "^1.0.3",
+        "is-arguments": "^1.1.1",
         "is-map": "^2.0.2",
         "is-set": "^2.0.2",
-        "is-string": "^1.0.5",
-        "isarray": "^2.0.5"
+        "is-string": "^1.0.7",
+        "isarray": "^2.0.5",
+        "stop-iteration-iterator": "^1.0.0"
       },
       "funding": {
         "url": "https://github.com/sponsors/ljharb"
@@ -4536,9 +4538,9 @@
       "dev": true
     },
     "node_modules/es-module-shims": {
-      "version": "1.6.2",
-      "resolved": "https://registry.npmjs.org/es-module-shims/-/es-module-shims-1.6.2.tgz",
-      "integrity": "sha512-VISkM/sF/TlQzFY3WlyCXj3Fkv7+L3pErEFmrDHj0URx54EMY9GpSbW3CE04ZqWk6qrC/YsRDBTu9QvU2n0dZw=="
+      "version": "1.6.3",
+      "resolved": "https://registry.npmjs.org/es-module-shims/-/es-module-shims-1.6.3.tgz",
+      "integrity": "sha512-+BQyPRZczeV9JH/17X1nu1GbD+SZvdPKD4Nrt2S61J94A2yc8DpWBlzv9KgF9cOXUZKifEShy8/qLelSVNo/rA=="
     },
     "node_modules/escalade": {
       "version": "3.1.1",
@@ -4921,6 +4923,20 @@
       "integrity": "sha512-OO0pH2lK6a0hZnAdau5ItzHPI6pUlvI7jMVnxUQRtw4owF2wk8lOSabtGDCTP4Ggrg2MbGnWO9X8K1t4+fGMDw==",
       "dev": true
     },
+    "node_modules/fsevents": {
+      "version": "2.3.2",
+      "resolved": "https://registry.npmjs.org/fsevents/-/fsevents-2.3.2.tgz",
+      "integrity": "sha512-xiqMQR4xAeHTuB9uWm+fFRcIOgKBMiOBP+eXiyT7jsgVCq1bkVygt00oASowB7EdtpOHaaPgKt812P9ab+DDKA==",
+      "dev": true,
+      "hasInstallScript": true,
+      "optional": true,
+      "os": [
+        "darwin"
+      ],
+      "engines": {
+        "node": "^8.16.0 || ^10.6.0 || >=11.0.0"
+      }
+    },
     "node_modules/function-bind": {
       "version": "1.1.1",
       "resolved": "https://registry.npmjs.org/function-bind/-/function-bind-1.1.1.tgz",
@@ -4953,9 +4969,9 @@
       }
     },
     "node_modules/get-intrinsic": {
-      "version": "1.1.3",
-      "resolved": "https://registry.npmjs.org/get-intrinsic/-/get-intrinsic-1.1.3.tgz",
-      "integrity": "sha512-QJVz1Tj7MS099PevUG5jvnt9tSkXN8K14dxQlikJuPt4uD9hHAHjLyLBiLR5zELelBdD9QNRAXZzsJx0WaDL9A==",
+      "version": "1.2.0",
+      "resolved": "https://registry.npmjs.org/get-intrinsic/-/get-intrinsic-1.2.0.tgz",
+      "integrity": "sha512-L049y6nFOuom5wGyRc3/gdTLO94dySVKRACj1RmJZBQXlbTMhtNIgkWkUHq+jYmZvKf14EW1EoJnnjbmoHij0Q==",
       "dependencies": {
         "function-bind": "^1.1.1",
         "has": "^1.0.3",
@@ -5114,12 +5130,11 @@
       }
     },
     "node_modules/hast-util-from-parse5": {
-      "version": "7.1.0",
-      "resolved": "https://registry.npmjs.org/hast-util-from-parse5/-/hast-util-from-parse5-7.1.0.tgz",
-      "integrity": "sha512-m8yhANIAccpU4K6+121KpPP55sSl9/samzQSQGpb0mTExcNh2WlvjtMwSWFhg6uqD4Rr6Nfa8N6TMypQM51rzQ==",
+      "version": "7.1.1",
+      "resolved": "https://registry.npmjs.org/hast-util-from-parse5/-/hast-util-from-parse5-7.1.1.tgz",
+      "integrity": "sha512-R6PoNcUs89ZxLJmMWsVbwSWuz95/9OriyQZ3e2ybwqGsRXzhA6gv49rgGmQvLbZuSNDv9fCg7vV7gXUsvtUFaA==",
       "dependencies": {
         "@types/hast": "^2.0.0",
-        "@types/parse5": "^6.0.0",
         "@types/unist": "^2.0.0",
         "hastscript": "^7.0.0",
         "property-information": "^6.0.0",
@@ -5133,9 +5148,9 @@
       }
     },
     "node_modules/hast-util-is-element": {
-      "version": "2.1.2",
-      "resolved": "https://registry.npmjs.org/hast-util-is-element/-/hast-util-is-element-2.1.2.tgz",
-      "integrity": "sha512-thjnlGAnwP8ef/GSO1Q8BfVk2gundnc2peGQqEg2kUt/IqesiGg/5mSwN2fE7nLzy61pg88NG6xV+UrGOrx9EA==",
+      "version": "2.1.3",
+      "resolved": "https://registry.npmjs.org/hast-util-is-element/-/hast-util-is-element-2.1.3.tgz",
+      "integrity": "sha512-O1bKah6mhgEq2WtVMk+Ta5K7pPMqsBBlmzysLdcwKVrqzZQ0CHqUPiIVspNhAG1rvxpvJjtGee17XfauZYKqVA==",
       "dependencies": {
         "@types/hast": "^2.0.0",
         "@types/unist": "^2.0.0"
@@ -5146,9 +5161,9 @@
       }
     },
     "node_modules/hast-util-parse-selector": {
-      "version": "3.1.0",
-      "resolved": "https://registry.npmjs.org/hast-util-parse-selector/-/hast-util-parse-selector-3.1.0.tgz",
-      "integrity": "sha512-AyjlI2pTAZEOeu7GeBPZhROx0RHBnydkQIXlhnFzDi0qfXTmGUWoCYZtomHbrdrheV4VFUlPcfJ6LMF5T6sQzg==",
+      "version": "3.1.1",
+      "resolved": "https://registry.npmjs.org/hast-util-parse-selector/-/hast-util-parse-selector-3.1.1.tgz",
+      "integrity": "sha512-jdlwBjEexy1oGz0aJ2f4GKMaVKkA9jwjr4MjAAI22E5fM/TXVZHuS5OpONtdeIkRKqAaryQ2E9xNQxijoThSZA==",
       "dependencies": {
         "@types/hast": "^2.0.0"
       },
@@ -5158,11 +5173,12 @@
       }
     },
     "node_modules/hast-util-to-text": {
-      "version": "3.1.1",
-      "resolved": "https://registry.npmjs.org/hast-util-to-text/-/hast-util-to-text-3.1.1.tgz",
-      "integrity": "sha512-7S3mOBxACy8syL45hCn3J7rHqYaXkxRfsX6LXEU5Shz4nt4GxdjtMUtG+T6G/ZLUHd7kslFAf14kAN71bz30xA==",
+      "version": "3.1.2",
+      "resolved": "https://registry.npmjs.org/hast-util-to-text/-/hast-util-to-text-3.1.2.tgz",
+      "integrity": "sha512-tcllLfp23dJJ+ju5wCCZHVpzsQQ43+moJbqVX3jNWPB7z/KFC4FyZD6R7y94cHL6MQ33YtMZL8Z0aIXXI4XFTw==",
       "dependencies": {
         "@types/hast": "^2.0.0",
+        "@types/unist": "^2.0.0",
         "hast-util-is-element": "^2.0.0",
         "unist-util-find-after": "^4.0.0"
       },
@@ -5172,18 +5188,18 @@
       }
     },
     "node_modules/hast-util-whitespace": {
-      "version": "2.0.0",
-      "resolved": "https://registry.npmjs.org/hast-util-whitespace/-/hast-util-whitespace-2.0.0.tgz",
-      "integrity": "sha512-Pkw+xBHuV6xFeJprJe2BBEoDV+AvQySaz3pPDRUs5PNZEMQjpXJJueqrpcHIXxnWTcAGi/UOCgVShlkY6kLoqg==",
+      "version": "2.0.1",
+      "resolved": "https://registry.npmjs.org/hast-util-whitespace/-/hast-util-whitespace-2.0.1.tgz",
+      "integrity": "sha512-nAxA0v8+vXSBDt3AnRUNjyRIQ0rD+ntpbAp4LnPkumc5M9yUbSMa4XDU9Q6etY4f1Wp4bNgvc1yjiZtsTTrSng==",
       "funding": {
         "type": "opencollective",
         "url": "https://opencollective.com/unified"
       }
     },
     "node_modules/hastscript": {
-      "version": "7.1.0",
-      "resolved": "https://registry.npmjs.org/hastscript/-/hastscript-7.1.0.tgz",
-      "integrity": "sha512-uBjaTTLN0MkCZxY/R2fWUOcu7FRtUVzKRO5P/RAfgsu3yFiMB1JWCO4AjeVkgHxAira1f2UecHK5WfS9QurlWA==",
+      "version": "7.2.0",
+      "resolved": "https://registry.npmjs.org/hastscript/-/hastscript-7.2.0.tgz",
+      "integrity": "sha512-TtYPq24IldU8iKoJQqvZOuhi5CyCQRAbvDOX0x1eW6rsHSxa/1i2CCiptNTotGHJ3VoHRGmqiv6/D3q113ikkw==",
       "dependencies": {
         "@types/hast": "^2.0.0",
         "comma-separated-tokens": "^2.0.0",
@@ -5402,9 +5418,9 @@
       "dev": true
     },
     "node_modules/immer": {
-      "version": "9.0.16",
-      "resolved": "https://registry.npmjs.org/immer/-/immer-9.0.16.tgz",
-      "integrity": "sha512-qenGE7CstVm1NrHQbMh8YaSzTZTFNP3zPqr3YU0S0UY441j4bJTg4A2Hh5KAhwgaiU6ZZ1Ar6y/2f4TblnMReQ==",
+      "version": "9.0.19",
+      "resolved": "https://registry.npmjs.org/immer/-/immer-9.0.19.tgz",
+      "integrity": "sha512-eY+Y0qcsB4TZKwgQzLaE/lqYMlKhv5J9dyd2RhhtGhNo2njPXDqU9XPfcNfa3MIDsdtZt5KlkIsirlo4dHsWdQ==",
       "funding": {
         "type": "opencollective",
         "url": "https://opencollective.com/immer"
@@ -5464,6 +5480,20 @@
       "resolved": "https://registry.npmjs.org/inline-style-parser/-/inline-style-parser-0.1.1.tgz",
       "integrity": "sha512-7NXolsK4CAS5+xvdj5OMMbI962hU/wvwoxk+LWR9Ek9bVtyuuYScDN6eS0rUm6TxApFpw7CX1o4uJzcd4AyD3Q=="
     },
+    "node_modules/internal-slot": {
+      "version": "1.0.4",
+      "resolved": "https://registry.npmjs.org/internal-slot/-/internal-slot-1.0.4.tgz",
+      "integrity": "sha512-tA8URYccNzMo94s5MQZgH8NB/XTa6HsOo0MLfXTKKEnHVVdegzaQoFZ7Jp44bdvLvY2waT5dc+j5ICEswhi7UQ==",
+      "dev": true,
+      "dependencies": {
+        "get-intrinsic": "^1.1.3",
+        "has": "^1.0.3",
+        "side-channel": "^1.0.4"
+      },
+      "engines": {
+        "node": ">= 0.4"
+      }
+    },
     "node_modules/interpret": {
       "version": "2.2.0",
       "resolved": "https://registry.npmjs.org/interpret/-/interpret-2.2.0.tgz",
@@ -5502,6 +5532,20 @@
         "url": "https://github.com/sponsors/ljharb"
       }
     },
+    "node_modules/is-array-buffer": {
+      "version": "3.0.1",
+      "resolved": "https://registry.npmjs.org/is-array-buffer/-/is-array-buffer-3.0.1.tgz",
+      "integrity": "sha512-ASfLknmY8Xa2XtB4wmbz13Wu202baeA18cJBCeCy0wXUHZF0IPyVEXqKEcd+t2fNSLLL1vC6k7lxZEojNbISXQ==",
+      "dev": true,
+      "dependencies": {
+        "call-bind": "^1.0.2",
+        "get-intrinsic": "^1.1.3",
+        "is-typed-array": "^1.1.10"
+      },
+      "funding": {
+        "url": "https://github.com/sponsors/ljharb"
+      }
+    },
     "node_modules/is-arrayish": {
       "version": "0.2.1",
       "resolved": "https://registry.npmjs.org/is-arrayish/-/is-arrayish-0.2.1.tgz",
@@ -5733,6 +5777,18 @@
         "url": "https://github.com/sponsors/ljharb"
       }
     },
+    "node_modules/is-shared-array-buffer": {
+      "version": "1.0.2",
+      "resolved": "https://registry.npmjs.org/is-shared-array-buffer/-/is-shared-array-buffer-1.0.2.tgz",
+      "integrity": "sha512-sqN2UDu1/0y6uvXyStCOzyhAjCSlHceFoMKJW8W9EU9cvic/QdsZ0kEU93HEy3IUEFZIiH/3w+AH/UQbPHNdhA==",
+      "dev": true,
+      "dependencies": {
+        "call-bind": "^1.0.2"
+      },
+      "funding": {
+        "url": "https://github.com/sponsors/ljharb"
+      }
+    },
     "node_modules/is-stream": {
       "version": "2.0.1",
       "resolved": "https://registry.npmjs.org/is-stream/-/is-stream-2.0.1.tgz",
@@ -5915,9 +5971,9 @@
       "dev": true
     },
     "node_modules/json5": {
-      "version": "2.2.2",
-      "resolved": "https://registry.npmjs.org/json5/-/json5-2.2.2.tgz",
-      "integrity": "sha512-46Tk9JiOL2z7ytNQWFLpj99RZkVgeHf87yGQKsIkaPz1qSH9UczKH1rO7K3wgRselo0tYMUNfecYpm/p1vC7tQ==",
+      "version": "2.2.3",
+      "resolved": "https://registry.npmjs.org/json5/-/json5-2.2.3.tgz",
+      "integrity": "sha512-XmOWe7eyHYH14cLdVPoyg+GOH3rYX++KpzrylJwSW98t3Nk+U8XOl8FWKOgwtzdb8lXGf6zYwDUzeHMWfxasyg==",
       "bin": {
         "json5": "lib/cli.js"
       },
@@ -5993,7 +6049,7 @@
       "name": "@leanprover/infoview",
       "version": "0.4.2",
       "resolved": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?master",
-      "integrity": "sha512-fNrNu9Hte4WqGsuGOcJiifbovphjV9Cz4NJjg/AZcjL7i+JAjR1hy8J2t/p2sMHVaaY+NRKEfRcbyq+jpOI91A==",
+      "integrity": "sha512-XthMPhgRGoP/3lClX5LEQNXQYmzEcIQQBuK6AZ4RC5NKcTU7XUpA0qtZTQcWkPeZbOqz02FX5Dg8f4P1CDMuGw==",
       "license": "Apache-2.0",
       "dependencies": {
         "@leanprover/infoview-api": "~0.2.1",
@@ -6059,7 +6115,7 @@
     },
     "node_modules/lean4web": {
       "version": "0.1.0",
-      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#635cd1aeefa0e47609ba98966ba4b9d189ad67ff",
+      "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#7602273506de9cb3ec22d7dd552035566c50d6c5",
       "dependencies": {
         "@fontsource/roboto": "^4.5.8",
         "@fontsource/roboto-mono": "^4.5.8",
@@ -6212,9 +6268,9 @@
       }
     },
     "node_modules/marked": {
-      "version": "4.2.4",
-      "resolved": "https://registry.npmjs.org/marked/-/marked-4.2.4.tgz",
-      "integrity": "sha512-Wcc9ikX7Q5E4BYDPvh1C6QNSxrjC9tBgz+A/vAhp59KXUgachw++uMvMKiSW8oA85nopmPZcEvBoex/YLMsiyA==",
+      "version": "4.2.12",
+      "resolved": "https://registry.npmjs.org/marked/-/marked-4.2.12.tgz",
+      "integrity": "sha512-yr8hSKa3Fv4D3jdZmtMMPghgVt6TWbk86WQaWhDloQjRSQhMMYCAro7jP7VDJrjjdV8pxVxMssXS8B8Y5DZ5aw==",
       "bin": {
         "marked": "bin/marked.js"
       },
@@ -6223,9 +6279,9 @@
       }
     },
     "node_modules/mdast-util-definitions": {
-      "version": "5.1.1",
-      "resolved": "https://registry.npmjs.org/mdast-util-definitions/-/mdast-util-definitions-5.1.1.tgz",
-      "integrity": "sha512-rQ+Gv7mHttxHOBx2dkF4HWTg+EE+UR78ptQWDylzPKaQuVGdG4HIoY3SrS/pCp80nZ04greFvXbVFHT+uf0JVQ==",
+      "version": "5.1.2",
+      "resolved": "https://registry.npmjs.org/mdast-util-definitions/-/mdast-util-definitions-5.1.2.tgz",
+      "integrity": "sha512-8SVPMuHqlPME/z3gqVwWY4zVXn8lqKv/pAhC57FuJ40ImXyBpmO5ukh98zB2v7Blql2FiHjHv9LVztSIqjY+MA==",
       "dependencies": {
         "@types/mdast": "^3.0.0",
         "@types/unist": "^2.0.0",
@@ -6237,10 +6293,11 @@
       }
     },
     "node_modules/mdast-util-find-and-replace": {
-      "version": "2.2.1",
-      "resolved": "https://registry.npmjs.org/mdast-util-find-and-replace/-/mdast-util-find-and-replace-2.2.1.tgz",
-      "integrity": "sha512-SobxkQXFAdd4b5WmEakmkVoh18icjQRxGy5OWTCzgsLRm1Fu/KCtwD1HIQSsmq5ZRjVH0Ehwg6/Fn3xIUk+nKw==",
+      "version": "2.2.2",
+      "resolved": "https://registry.npmjs.org/mdast-util-find-and-replace/-/mdast-util-find-and-replace-2.2.2.tgz",
+      "integrity": "sha512-MTtdFRz/eMDHXzeK6W3dO7mXUlF82Gom4y0oOgvHhh/HXZAGvIQDUvQ0SuUx+j2tv44b8xTHOm8K/9OoRFnXKw==",
       "dependencies": {
+        "@types/mdast": "^3.0.0",
         "escape-string-regexp": "^5.0.0",
         "unist-util-is": "^5.0.0",
         "unist-util-visit-parents": "^5.0.0"
@@ -6262,9 +6319,9 @@
       }
     },
     "node_modules/mdast-util-from-markdown": {
-      "version": "1.2.0",
-      "resolved": "https://registry.npmjs.org/mdast-util-from-markdown/-/mdast-util-from-markdown-1.2.0.tgz",
-      "integrity": "sha512-iZJyyvKD1+K7QX1b5jXdE7Sc5dtoTry1vzV28UZZe8Z1xVnB/czKntJ7ZAkG0tANqRnBF6p3p7GpU1y19DTf2Q==",
+      "version": "1.3.0",
+      "resolved": "https://registry.npmjs.org/mdast-util-from-markdown/-/mdast-util-from-markdown-1.3.0.tgz",
+      "integrity": "sha512-HN3W1gRIuN/ZW295c7zi7g9lVBllMgZE40RxCX37wrTPWXCWtpvOZdfnuK+1WNpvZje6XuJeI3Wnb4TJEUem+g==",
       "dependencies": {
         "@types/mdast": "^3.0.0",
         "@types/unist": "^2.0.0",
@@ -6285,9 +6342,9 @@
       }
     },
     "node_modules/mdast-util-gfm": {
-      "version": "2.0.1",
-      "resolved": "https://registry.npmjs.org/mdast-util-gfm/-/mdast-util-gfm-2.0.1.tgz",
-      "integrity": "sha512-42yHBbfWIFisaAfV1eixlabbsa6q7vHeSPY+cg+BBjX51M8xhgMacqH9g6TftB/9+YkcI0ooV4ncfrJslzm/RQ==",
+      "version": "2.0.2",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm/-/mdast-util-gfm-2.0.2.tgz",
+      "integrity": "sha512-qvZ608nBppZ4icQlhQQIAdc6S3Ffj9RGmzwUKUWuEICFnd1LVkN3EktF7ZHAgfcEdvZB5owU9tQgt99e2TlLjg==",
       "dependencies": {
         "mdast-util-from-markdown": "^1.0.0",
         "mdast-util-gfm-autolink-literal": "^1.0.0",
@@ -6303,9 +6360,9 @@
       }
     },
     "node_modules/mdast-util-gfm-autolink-literal": {
-      "version": "1.0.2",
-      "resolved": "https://registry.npmjs.org/mdast-util-gfm-autolink-literal/-/mdast-util-gfm-autolink-literal-1.0.2.tgz",
-      "integrity": "sha512-FzopkOd4xTTBeGXhXSBU0OCDDh5lUj2rd+HQqG92Ld+jL4lpUfgX2AT2OHAVP9aEeDKp7G92fuooSZcYJA3cRg==",
+      "version": "1.0.3",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm-autolink-literal/-/mdast-util-gfm-autolink-literal-1.0.3.tgz",
+      "integrity": "sha512-My8KJ57FYEy2W2LyNom4n3E7hKTuQk/0SES0u16tjA9Z3oFkF4RrC/hPAPgjlSpezsOvI8ObcXcElo92wn5IGA==",
       "dependencies": {
         "@types/mdast": "^3.0.0",
         "ccount": "^2.0.0",
@@ -6318,9 +6375,9 @@
       }
     },
     "node_modules/mdast-util-gfm-footnote": {
-      "version": "1.0.1",
-      "resolved": "https://registry.npmjs.org/mdast-util-gfm-footnote/-/mdast-util-gfm-footnote-1.0.1.tgz",
-      "integrity": "sha512-p+PrYlkw9DeCRkTVw1duWqPRHX6Ywh2BNKJQcZbCwAuP/59B0Lk9kakuAd7KbQprVO4GzdW8eS5++A9PUSqIyw==",
+      "version": "1.0.2",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm-footnote/-/mdast-util-gfm-footnote-1.0.2.tgz",
+      "integrity": "sha512-56D19KOGbE00uKVj3sgIykpwKL179QsVFwx/DCW0u/0+URsryacI4MAdNJl0dh+u2PSsD9FtxPFbHCzJ78qJFQ==",
       "dependencies": {
         "@types/mdast": "^3.0.0",
         "mdast-util-to-markdown": "^1.3.0",
@@ -6332,9 +6389,9 @@
       }
     },
     "node_modules/mdast-util-gfm-strikethrough": {
-      "version": "1.0.2",
-      "resolved": "https://registry.npmjs.org/mdast-util-gfm-strikethrough/-/mdast-util-gfm-strikethrough-1.0.2.tgz",
-      "integrity": "sha512-T/4DVHXcujH6jx1yqpcAYYwd+z5lAYMw4Ls6yhTfbMMtCt0PHY4gEfhW9+lKsLBtyhUGKRIzcUA2FATVqnvPDA==",
+      "version": "1.0.3",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm-strikethrough/-/mdast-util-gfm-strikethrough-1.0.3.tgz",
+      "integrity": "sha512-DAPhYzTYrRcXdMjUtUjKvW9z/FNAMTdU0ORyMcbmkwYNbKocDpdk+PX1L1dQgOID/+vVs1uBQ7ElrBQfZ0cuiQ==",
       "dependencies": {
         "@types/mdast": "^3.0.0",
         "mdast-util-to-markdown": "^1.3.0"
@@ -6345,9 +6402,9 @@
       }
     },
     "node_modules/mdast-util-gfm-table": {
-      "version": "1.0.6",
-      "resolved": "https://registry.npmjs.org/mdast-util-gfm-table/-/mdast-util-gfm-table-1.0.6.tgz",
-      "integrity": "sha512-uHR+fqFq3IvB3Rd4+kzXW8dmpxUhvgCQZep6KdjsLK4O6meK5dYZEayLtIxNus1XO3gfjfcIFe8a7L0HZRGgag==",
+      "version": "1.0.7",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm-table/-/mdast-util-gfm-table-1.0.7.tgz",
+      "integrity": "sha512-jjcpmNnQvrmN5Vx7y7lEc2iIOEytYv7rTvu+MeyAsSHTASGCCRA79Igg2uKssgOs1i1po8s3plW0sTu1wkkLGg==",
       "dependencies": {
         "@types/mdast": "^3.0.0",
         "markdown-table": "^3.0.0",
@@ -6360,9 +6417,9 @@
       }
     },
     "node_modules/mdast-util-gfm-task-list-item": {
-      "version": "1.0.1",
-      "resolved": "https://registry.npmjs.org/mdast-util-gfm-task-list-item/-/mdast-util-gfm-task-list-item-1.0.1.tgz",
-      "integrity": "sha512-KZ4KLmPdABXOsfnM6JHUIjxEvcx2ulk656Z/4Balw071/5qgnhz+H1uGtf2zIGnrnvDC8xR4Fj9uKbjAFGNIeA==",
+      "version": "1.0.2",
+      "resolved": "https://registry.npmjs.org/mdast-util-gfm-task-list-item/-/mdast-util-gfm-task-list-item-1.0.2.tgz",
+      "integrity": "sha512-PFTA1gzfp1B1UaiJVyhJZA1rm0+Tzn690frc/L8vNX1Jop4STZgOE6bxUhnzdVSB+vm2GU1tIsuQcA9bxTQpMQ==",
       "dependencies": {
         "@types/mdast": "^3.0.0",
         "mdast-util-to-markdown": "^1.3.0"
@@ -6373,9 +6430,9 @@
       }
     },
     "node_modules/mdast-util-math": {
-      "version": "2.0.1",
-      "resolved": "https://registry.npmjs.org/mdast-util-math/-/mdast-util-math-2.0.1.tgz",
-      "integrity": "sha512-ZZtjyRwobsiVg4bY0Q5CzAZztpbjRIA7ZlMMb0PNkwTXOnJTUoHvzBhVG95LIuek5Mlj1l2P+jBvWviqW7G+0A==",
+      "version": "2.0.2",
+      "resolved": "https://registry.npmjs.org/mdast-util-math/-/mdast-util-math-2.0.2.tgz",
+      "integrity": "sha512-8gmkKVp9v6+Tgjtq6SYx9kGPpTf6FVYRa53/DLh479aldR9AyP48qeVOgNZ5X7QUK7nOy4yw7vg6mbiGcs9jWQ==",
       "dependencies": {
         "@types/mdast": "^3.0.0",
         "longest-streak": "^3.0.0",
@@ -6386,17 +6443,29 @@
         "url": "https://opencollective.com/unified"
       }
     },
+    "node_modules/mdast-util-phrasing": {
+      "version": "3.0.1",
+      "resolved": "https://registry.npmjs.org/mdast-util-phrasing/-/mdast-util-phrasing-3.0.1.tgz",
+      "integrity": "sha512-WmI1gTXUBJo4/ZmSk79Wcb2HcjPJBzM1nlI/OUWA8yk2X9ik3ffNbBGsU+09BFmXaL1IBb9fiuvq6/KMiNycSg==",
+      "dependencies": {
+        "@types/mdast": "^3.0.0",
+        "unist-util-is": "^5.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
     "node_modules/mdast-util-to-hast": {
-      "version": "12.2.4",
-      "resolved": "https://registry.npmjs.org/mdast-util-to-hast/-/mdast-util-to-hast-12.2.4.tgz",
-      "integrity": "sha512-a21xoxSef1l8VhHxS1Dnyioz6grrJkoaCUgGzMD/7dWHvboYX3VW53esRUfB5tgTyz4Yos1n25SPcj35dJqmAg==",
+      "version": "12.3.0",
+      "resolved": "https://registry.npmjs.org/mdast-util-to-hast/-/mdast-util-to-hast-12.3.0.tgz",
+      "integrity": "sha512-pits93r8PhnIoU4Vy9bjW39M2jJ6/tdHyja9rrot9uujkN7UTU9SDnE6WNJz/IGyQk3XHX6yNNtrBH6cQzm8Hw==",
       "dependencies": {
         "@types/hast": "^2.0.0",
         "@types/mdast": "^3.0.0",
         "mdast-util-definitions": "^5.0.0",
         "micromark-util-sanitize-uri": "^1.1.0",
         "trim-lines": "^3.0.0",
-        "unist-builder": "^3.0.0",
         "unist-util-generated": "^2.0.0",
         "unist-util-position": "^4.0.0",
         "unist-util-visit": "^4.0.0"
@@ -6407,13 +6476,14 @@
       }
     },
     "node_modules/mdast-util-to-markdown": {
-      "version": "1.4.0",
-      "resolved": "https://registry.npmjs.org/mdast-util-to-markdown/-/mdast-util-to-markdown-1.4.0.tgz",
-      "integrity": "sha512-IjXARf/O8VGx/pc5SZ7syfydq1DYL9vd92orsG5U0b4GNCmAvXzu+n7sbzfIKrXwB0AVrYk3NV2kXl0AIi9LCA==",
+      "version": "1.5.0",
+      "resolved": "https://registry.npmjs.org/mdast-util-to-markdown/-/mdast-util-to-markdown-1.5.0.tgz",
+      "integrity": "sha512-bbv7TPv/WC49thZPg3jXuqzuvI45IL2EVAr/KxF0BSdHsU0ceFHOmwQn6evxAh1GaoK/6GQ1wp4R4oW2+LFL/A==",
       "dependencies": {
         "@types/mdast": "^3.0.0",
         "@types/unist": "^2.0.0",
         "longest-streak": "^3.0.0",
+        "mdast-util-phrasing": "^3.0.0",
         "mdast-util-to-string": "^3.0.0",
         "micromark-util-decode-string": "^1.0.0",
         "unist-util-visit": "^4.0.0",
@@ -6425,9 +6495,12 @@
       }
     },
     "node_modules/mdast-util-to-string": {
-      "version": "3.1.0",
-      "resolved": "https://registry.npmjs.org/mdast-util-to-string/-/mdast-util-to-string-3.1.0.tgz",
-      "integrity": "sha512-n4Vypz/DZgwo0iMHLQL49dJzlp7YtAJP+N07MZHpjPf/5XJuHUWstviF4Mn2jEiR/GNmtnRRqnwsXExk3igfFA==",
+      "version": "3.1.1",
+      "resolved": "https://registry.npmjs.org/mdast-util-to-string/-/mdast-util-to-string-3.1.1.tgz",
+      "integrity": "sha512-tGvhT94e+cVnQt8JWE9/b3cUQZWS732TJxXHktvP+BYo62PpYD53Ls/6cC60rW21dW+txxiM4zMdc6abASvZKA==",
+      "dependencies": {
+        "@types/mdast": "^3.0.0"
+      },
       "funding": {
         "type": "opencollective",
         "url": "https://opencollective.com/unified"
@@ -6442,9 +6515,9 @@
       }
     },
     "node_modules/memfs": {
-      "version": "3.4.12",
-      "resolved": "https://registry.npmjs.org/memfs/-/memfs-3.4.12.tgz",
-      "integrity": "sha512-BcjuQn6vfqP+k100e0E9m61Hyqa//Brp+I3f0OBmN0ATHlFA8vx3Lt8z57R3u2bPqe3WGDBC+nF72fTH7isyEw==",
+      "version": "3.4.13",
+      "resolved": "https://registry.npmjs.org/memfs/-/memfs-3.4.13.tgz",
+      "integrity": "sha512-omTM41g3Skpvx5dSYeZIbXKcXoAVc/AoMNwn9TKx++L/gaen/+4TTttmu8ZSch5vfVJ8uJvGbroTsIlslRg6lg==",
       "dev": true,
       "dependencies": {
         "fs-monkey": "^1.0.3"
@@ -7259,9 +7332,9 @@
       }
     },
     "node_modules/node-releases": {
-      "version": "2.0.8",
-      "resolved": "https://registry.npmjs.org/node-releases/-/node-releases-2.0.8.tgz",
-      "integrity": "sha512-dFSmB8fFHEH/s81Xi+Y/15DQY6VHW81nXRj86EMSL3lmuTmK1e+aT4wrFCkTbm+gSwkw4KpX+rT/pMM2c1mF+A=="
+      "version": "2.0.10",
+      "resolved": "https://registry.npmjs.org/node-releases/-/node-releases-2.0.10.tgz",
+      "integrity": "sha512-5GFldHPXVG/YZmFzJvKK2zDSzPKhEp0+ZR5SVaoSag9fsL5YgHbUHDfnG5494ISANDcK4KwPXAx2xqVEydmd7w=="
     },
     "node_modules/nodemon": {
       "version": "2.0.20",
@@ -7365,9 +7438,9 @@
       }
     },
     "node_modules/object-inspect": {
-      "version": "1.12.2",
-      "resolved": "https://registry.npmjs.org/object-inspect/-/object-inspect-1.12.2.tgz",
-      "integrity": "sha512-z+cPxW0QGUp0mcqcsgQyLVRDoXFQbXOwBaqyF7VIgI4TWNQsDHrBpUQslRmIfAoYWdYzs6UlKJtB2XJpTaNSpQ==",
+      "version": "1.12.3",
+      "resolved": "https://registry.npmjs.org/object-inspect/-/object-inspect-1.12.3.tgz",
+      "integrity": "sha512-geUvdk7c+eizMNUDkRpW1wJwgfOiOeHbxBR/hLXK1aT6zmVSO0jsQcs7fj6MGw89jC/cjGfLcNOrtMYtGqm81g==",
       "funding": {
         "url": "https://github.com/sponsors/ljharb"
       }
@@ -7742,9 +7815,9 @@
       }
     },
     "node_modules/postcss": {
-      "version": "8.4.20",
-      "resolved": "https://registry.npmjs.org/postcss/-/postcss-8.4.20.tgz",
-      "integrity": "sha512-6Q04AXR1212bXr5fh03u8aAwbLxAQNGQ/Q1LNa0VfOI06ZAlhPHtQvE4OIdpj4kLThXilalPnmDSOD65DcHt+g==",
+      "version": "8.4.21",
+      "resolved": "https://registry.npmjs.org/postcss/-/postcss-8.4.21.tgz",
+      "integrity": "sha512-tP7u/Sn/dVxK2NnruI4H9BG+x+Wxz6oeZ1cJ8P6G/PZY0IKk4k/63TDsQf2kQq3+qoJeLm2kIBUNlZe3zgb4Zg==",
       "dev": true,
       "funding": [
         {
@@ -7924,9 +7997,9 @@
       "dev": true
     },
     "node_modules/punycode": {
-      "version": "2.1.1",
-      "resolved": "https://registry.npmjs.org/punycode/-/punycode-2.1.1.tgz",
-      "integrity": "sha512-XRsRjdf+j5ml+y/6GKHPZbrF/8p2Yga0JPtdqTIY2Xe5ohJPD9saDJJLPvp9+NSBprVvevdXZybnj2cv8OEd0A==",
+      "version": "2.3.0",
+      "resolved": "https://registry.npmjs.org/punycode/-/punycode-2.3.0.tgz",
+      "integrity": "sha512-rRV+zQD8tVFys26lAGR9WUuS4iUAngJScM+ZRSKtvl5tKeZ2t5bvdNFdNHBW9FWR4guGHlgmsZ1G7BSm2wTbuA==",
       "dev": true,
       "engines": {
         "node": ">=6"
@@ -8011,9 +8084,9 @@
       "integrity": "sha512-xWGDIW6x921xtzPkhiULtthJHoJvBbF3q26fzloPCK0hsvxtPVelvftw3zjbHWSkR2km9Z+4uxbDDK/6Zw9B8w=="
     },
     "node_modules/react-markdown": {
-      "version": "8.0.4",
-      "resolved": "https://registry.npmjs.org/react-markdown/-/react-markdown-8.0.4.tgz",
-      "integrity": "sha512-2oxHa6oDxc1apg/Gnc1Goh06t3B617xeywqI/92wmDV9FELI6ayRkwge7w7DoEqM0gRpZGTNU6xQG+YpJISnVg==",
+      "version": "8.0.5",
+      "resolved": "https://registry.npmjs.org/react-markdown/-/react-markdown-8.0.5.tgz",
+      "integrity": "sha512-jGJolWWmOWAvzf+xMdB9zwStViODyyFQhNB/bwCerbBKmrTmgmA599CGiOlP58OId1IMoIRsA8UdI1Lod4zb5A==",
       "dependencies": {
         "@types/hast": "^2.0.0",
         "@types/prop-types": "^15.0.0",
@@ -8026,7 +8099,7 @@
         "remark-parse": "^10.0.0",
         "remark-rehype": "^10.0.0",
         "space-separated-tokens": "^2.0.0",
-        "style-to-object": "^0.3.0",
+        "style-to-object": "^0.4.0",
         "unified": "^10.0.0",
         "unist-util-visit": "^4.0.0",
         "vfile": "^5.0.0"
@@ -8102,11 +8175,11 @@
       }
     },
     "node_modules/react-router": {
-      "version": "6.5.0",
-      "resolved": "https://registry.npmjs.org/react-router/-/react-router-6.5.0.tgz",
-      "integrity": "sha512-fqqUSU0NC0tSX0sZbyuxzuAzvGqbjiZItBQnyicWlOUmzhAU8YuLgRbaCL2hf3sJdtRy4LP/WBrWtARkMvdGPQ==",
+      "version": "6.8.0",
+      "resolved": "https://registry.npmjs.org/react-router/-/react-router-6.8.0.tgz",
+      "integrity": "sha512-760bk7y3QwabduExtudhWbd88IBbuD1YfwzpuDUAlJUJ7laIIcqhMvdhSVh1Fur1PE8cGl84L0dxhR3/gvHF7A==",
       "dependencies": {
-        "@remix-run/router": "1.1.0"
+        "@remix-run/router": "1.3.1"
       },
       "engines": {
         "node": ">=14"
@@ -8116,12 +8189,12 @@
       }
     },
     "node_modules/react-router-dom": {
-      "version": "6.5.0",
-      "resolved": "https://registry.npmjs.org/react-router-dom/-/react-router-dom-6.5.0.tgz",
-      "integrity": "sha512-/XzRc5fq80gW1ctiIGilyKFZC/j4kfe75uivMsTChFbkvrK4ZrF3P3cGIc1f/SSkQ4JiJozPrf+AwUHHWVehVg==",
+      "version": "6.8.0",
+      "resolved": "https://registry.npmjs.org/react-router-dom/-/react-router-dom-6.8.0.tgz",
+      "integrity": "sha512-hQouduSTywGJndE86CXJ2h7YEy4HYC6C/uh19etM+79FfQ6cFFFHnHyDlzO4Pq0eBUI96E4qVE5yUjA00yJZGQ==",
       "dependencies": {
-        "@remix-run/router": "1.1.0",
-        "react-router": "6.5.0"
+        "@remix-run/router": "1.3.1",
+        "react-router": "6.8.0"
       },
       "engines": {
         "node": ">=14"
@@ -8196,9 +8269,9 @@
       }
     },
     "node_modules/redux": {
-      "version": "4.2.0",
-      "resolved": "https://registry.npmjs.org/redux/-/redux-4.2.0.tgz",
-      "integrity": "sha512-oSBmcKKIuIR4ME29/AeNUnl5L+hvBq7OaJWzaptTQJAntaPvxIJqfnjbaEiCzzaIz+XmVILfqAM3Ob0aXLPfjA==",
+      "version": "4.2.1",
+      "resolved": "https://registry.npmjs.org/redux/-/redux-4.2.1.tgz",
+      "integrity": "sha512-LAUYz4lc+Do8/g7aeRa8JkyDErK6ekstQaqWQrNRW//MY1TvCEpMtpTWvlQ+FPbWCx+Xixu/6SHt5N0HR+SB4w==",
       "dependencies": {
         "@babel/runtime": "^7.9.2"
       }
@@ -8638,9 +8711,9 @@
       "integrity": "sha512-6FlzubTLZG3J2a/NVCAleEhjzq5oxgHyaCU9yYXvcLsvoVaHJq/s5xXI6/XXP6tz7R9xAOtHnSO/tXtF3WRTlA=="
     },
     "node_modules/serialize-javascript": {
-      "version": "6.0.0",
-      "resolved": "https://registry.npmjs.org/serialize-javascript/-/serialize-javascript-6.0.0.tgz",
-      "integrity": "sha512-Qr3TosvguFt8ePWqsvRfrKyQXIiW+nGbYpy8XK24NQHE83caxWt+mIymTT19DGFbNWNLfEwsrkSmN64lVWB9ag==",
+      "version": "6.0.1",
+      "resolved": "https://registry.npmjs.org/serialize-javascript/-/serialize-javascript-6.0.1.tgz",
+      "integrity": "sha512-owoXEFjWRllis8/M1Q+Cw5k8ZH40e3zhp/ovX+Xr/vi1qj6QesbyXXViFbpNvWvPNAD62SutwEXavefrLJWj7w==",
       "dev": true,
       "dependencies": {
         "randombytes": "^2.1.0"
@@ -8777,9 +8850,9 @@
       }
     },
     "node_modules/shell-quote": {
-      "version": "1.7.4",
-      "resolved": "https://registry.npmjs.org/shell-quote/-/shell-quote-1.7.4.tgz",
-      "integrity": "sha512-8o/QEhSSRb1a5i7TFR0iM4G16Z0vYB2OQVs4G3aAFXjn3T6yEx8AZxy1PgDF7I00LZHYA3WxaSYIf5e5sAX8Rw==",
+      "version": "1.8.0",
+      "resolved": "https://registry.npmjs.org/shell-quote/-/shell-quote-1.8.0.tgz",
+      "integrity": "sha512-QHsz8GgQIGKlRi24yFc6a6lN69Idnx634w49ay6+jA5yFh7a1UY+4Rp6HPx/L/1zcEDPEij8cIsiqR6bQsE5VQ==",
       "dev": true,
       "funding": {
         "url": "https://github.com/sponsors/ljharb"
@@ -8945,6 +9018,18 @@
         "node": ">= 0.8"
       }
     },
+    "node_modules/stop-iteration-iterator": {
+      "version": "1.0.0",
+      "resolved": "https://registry.npmjs.org/stop-iteration-iterator/-/stop-iteration-iterator-1.0.0.tgz",
+      "integrity": "sha512-iCGQj+0l0HOdZ2AEeBADlsRC+vsnDsZsbdSiH1yNSjcfKM7fdpCMfqAL/dwF5BLiw/XhRft/Wax6zQbhq2BcjQ==",
+      "dev": true,
+      "dependencies": {
+        "internal-slot": "^1.0.4"
+      },
+      "engines": {
+        "node": ">= 0.4"
+      }
+    },
     "node_modules/stream-http": {
       "version": "3.2.0",
       "resolved": "https://registry.npmjs.org/stream-http/-/stream-http-3.2.0.tgz",
@@ -9016,9 +9101,9 @@
       }
     },
     "node_modules/style-to-object": {
-      "version": "0.3.0",
-      "resolved": "https://registry.npmjs.org/style-to-object/-/style-to-object-0.3.0.tgz",
-      "integrity": "sha512-CzFnRRXhzWIdItT3OmF8SQfWyahHhjq3HwcMNCNLn+N7klOOqPjMeG/4JSu77D7ypZdGvSzvkrbyeTMizz2VrA==",
+      "version": "0.4.1",
+      "resolved": "https://registry.npmjs.org/style-to-object/-/style-to-object-0.4.1.tgz",
+      "integrity": "sha512-HFpbb5gr2ypci7Qw+IOhnP2zOU7e77b+rzM+wTzXzfi1PrtBCX0E7Pk4wL4iTLnhzZ+JgEGAhX81ebTg/aYjQw==",
       "dependencies": {
         "inline-style-parser": "0.1.1"
       }
@@ -9065,9 +9150,9 @@
       }
     },
     "node_modules/terser": {
-      "version": "5.16.1",
-      "resolved": "https://registry.npmjs.org/terser/-/terser-5.16.1.tgz",
-      "integrity": "sha512-xvQfyfA1ayT0qdK47zskQgRZeWLoOQ8JQ6mIgRGVNwZKdQMU+5FkCBjmv4QjcrTzyZquRw2FVtlJSRUmMKQslw==",
+      "version": "5.16.3",
+      "resolved": "https://registry.npmjs.org/terser/-/terser-5.16.3.tgz",
+      "integrity": "sha512-v8wWLaS/xt3nE9dgKEWhNUFP6q4kngO5B8eYFUuebsu7Dw/UNAnpUod6UHo04jSSkv8TzKHjZDSd7EXdDQAl8Q==",
       "dev": true,
       "dependencies": {
         "@jridgewell/source-map": "^0.3.2",
@@ -9318,9 +9403,9 @@
       "dev": true
     },
     "node_modules/tslib": {
-      "version": "2.4.1",
-      "resolved": "https://registry.npmjs.org/tslib/-/tslib-2.4.1.tgz",
-      "integrity": "sha512-tGyy4dAjRIEwI7BzsB0lynWgOpfqjUdq91XXAlIWD2OwKBH7oCl/GZG/HT4BOHrTlPMOASlMQ7veyTqpmRcrNA==",
+      "version": "2.5.0",
+      "resolved": "https://registry.npmjs.org/tslib/-/tslib-2.5.0.tgz",
+      "integrity": "sha512-336iVw3rtn2BUK7ORdIAHTyxHGRIHVReokCR3XjbckJMK7ms8FysBfhLR8IXnAgy7T0PTPNBWKiH514FOW/WSg==",
       "dev": true
     },
     "node_modules/type-is": {
@@ -9336,9 +9421,9 @@
       }
     },
     "node_modules/typescript": {
-      "version": "4.9.4",
-      "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.9.4.tgz",
-      "integrity": "sha512-Uz+dTXYzxXXbsFpM86Wh3dKCxrQqUcVMxwU54orwlJjOpO3ao8L7j5lH+dWfTwgCwIuM9GQ2kvVotzYJMXTBZg==",
+      "version": "4.9.5",
+      "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.9.5.tgz",
+      "integrity": "sha512-1FXk9E2Hm+QzZQ7z+McJiHL4NW1F2EzMu9Nq9i3zAaGqibafqYwCVU6WyWAuyQRRzOlxou8xZSyXLEN8oKj24g==",
       "dev": true,
       "bin": {
         "tsc": "bin/tsc",
@@ -9412,22 +9497,10 @@
         "url": "https://opencollective.com/unified"
       }
     },
-    "node_modules/unist-builder": {
-      "version": "3.0.0",
-      "resolved": "https://registry.npmjs.org/unist-builder/-/unist-builder-3.0.0.tgz",
-      "integrity": "sha512-GFxmfEAa0vi9i5sd0R2kcrI9ks0r82NasRq5QHh2ysGngrc6GiqD5CDf1FjPenY4vApmFASBIIlk/jj5J5YbmQ==",
-      "dependencies": {
-        "@types/unist": "^2.0.0"
-      },
-      "funding": {
-        "type": "opencollective",
-        "url": "https://opencollective.com/unified"
-      }
-    },
     "node_modules/unist-util-find-after": {
-      "version": "4.0.0",
-      "resolved": "https://registry.npmjs.org/unist-util-find-after/-/unist-util-find-after-4.0.0.tgz",
-      "integrity": "sha512-gfpsxKQde7atVF30n5Gff2fQhAc4/HTOV4CvkXpTg9wRfQhZWdXitpyXHWB6YcYgnsxLx+4gGHeVjCTAAp9sjw==",
+      "version": "4.0.1",
+      "resolved": "https://registry.npmjs.org/unist-util-find-after/-/unist-util-find-after-4.0.1.tgz",
+      "integrity": "sha512-QO/PuPMm2ERxC6vFXEPtmAutOopy5PknD+Oq64gGwxKtk4xwo9Z97t9Av1obPmGU0IyTa6EKYUfTrK2QJS3Ozw==",
       "dependencies": {
         "@types/unist": "^2.0.0",
         "unist-util-is": "^5.0.0"
@@ -9438,27 +9511,27 @@
       }
     },
     "node_modules/unist-util-generated": {
-      "version": "2.0.0",
-      "resolved": "https://registry.npmjs.org/unist-util-generated/-/unist-util-generated-2.0.0.tgz",
-      "integrity": "sha512-TiWE6DVtVe7Ye2QxOVW9kqybs6cZexNwTwSMVgkfjEReqy/xwGpAXb99OxktoWwmL+Z+Epb0Dn8/GNDYP1wnUw==",
+      "version": "2.0.1",
+      "resolved": "https://registry.npmjs.org/unist-util-generated/-/unist-util-generated-2.0.1.tgz",
+      "integrity": "sha512-qF72kLmPxAw0oN2fwpWIqbXAVyEqUzDHMsbtPvOudIlUzXYFIeQIuxXQCRCFh22B7cixvU0MG7m3MW8FTq/S+A==",
       "funding": {
         "type": "opencollective",
         "url": "https://opencollective.com/unified"
       }
     },
     "node_modules/unist-util-is": {
-      "version": "5.1.1",
-      "resolved": "https://registry.npmjs.org/unist-util-is/-/unist-util-is-5.1.1.tgz",
-      "integrity": "sha512-F5CZ68eYzuSvJjGhCLPL3cYx45IxkqXSetCcRgUXtbcm50X2L9oOWQlfUfDdAf+6Pd27YDblBfdtmsThXmwpbQ==",
+      "version": "5.2.0",
+      "resolved": "https://registry.npmjs.org/unist-util-is/-/unist-util-is-5.2.0.tgz",
+      "integrity": "sha512-Glt17jWwZeyqrFqOK0pF1Ded5U3yzJnFr8CG1GMjCWTp9zDo2p+cmD6pWbZU8AgM5WU3IzRv6+rBwhzsGh6hBQ==",
       "funding": {
         "type": "opencollective",
         "url": "https://opencollective.com/unified"
       }
     },
     "node_modules/unist-util-position": {
-      "version": "4.0.3",
-      "resolved": "https://registry.npmjs.org/unist-util-position/-/unist-util-position-4.0.3.tgz",
-      "integrity": "sha512-p/5EMGIa1qwbXjA+QgcBXaPWjSnZfQ2Sc3yBEEfgPwsEmJd8Qh+DSk3LGnmOM4S1bY2C0AjmMnB8RuEYxpPwXQ==",
+      "version": "4.0.4",
+      "resolved": "https://registry.npmjs.org/unist-util-position/-/unist-util-position-4.0.4.tgz",
+      "integrity": "sha512-kUBE91efOWfIVBo8xzh/uZQ7p9ffYRtUbMRZBNFYwf0RK8koUMx6dGUfwylLOKmaT2cs4wSW96QoYUSXAyEtpg==",
       "dependencies": {
         "@types/unist": "^2.0.0"
       },
@@ -9468,9 +9541,9 @@
       }
     },
     "node_modules/unist-util-remove-position": {
-      "version": "4.0.1",
-      "resolved": "https://registry.npmjs.org/unist-util-remove-position/-/unist-util-remove-position-4.0.1.tgz",
-      "integrity": "sha512-0yDkppiIhDlPrfHELgB+NLQD5mfjup3a8UYclHruTJWmY74je8g+CIFr79x5f6AkmzSwlvKLbs63hC0meOMowQ==",
+      "version": "4.0.2",
+      "resolved": "https://registry.npmjs.org/unist-util-remove-position/-/unist-util-remove-position-4.0.2.tgz",
+      "integrity": "sha512-TkBb0HABNmxzAcfLf4qsIbFbaPDvMO6wa3b3j4VcEzFVaw1LBKwnW4/sRJ/atSLSzoIg41JWEdnE7N6DIhGDGQ==",
       "dependencies": {
         "@types/unist": "^2.0.0",
         "unist-util-visit": "^4.0.0"
@@ -9481,9 +9554,9 @@
       }
     },
     "node_modules/unist-util-stringify-position": {
-      "version": "3.0.2",
-      "resolved": "https://registry.npmjs.org/unist-util-stringify-position/-/unist-util-stringify-position-3.0.2.tgz",
-      "integrity": "sha512-7A6eiDCs9UtjcwZOcCpM4aPII3bAAGv13E96IkawkOAW0OhH+yRxtY0lzo8KiHpzEMfH7Q+FizUmwp8Iqy5EWg==",
+      "version": "3.0.3",
+      "resolved": "https://registry.npmjs.org/unist-util-stringify-position/-/unist-util-stringify-position-3.0.3.tgz",
+      "integrity": "sha512-k5GzIBZ/QatR8N5X2y+drfpWG8IDBzdnVj6OInRNWm1oXrzydiaAT2OQiA8DPRRZyAKb9b6I2a6PxYklZD0gKg==",
       "dependencies": {
         "@types/unist": "^2.0.0"
       },
@@ -9493,9 +9566,9 @@
       }
     },
     "node_modules/unist-util-visit": {
-      "version": "4.1.1",
-      "resolved": "https://registry.npmjs.org/unist-util-visit/-/unist-util-visit-4.1.1.tgz",
-      "integrity": "sha512-n9KN3WV9k4h1DxYR1LoajgN93wpEi/7ZplVe02IoB4gH5ctI1AaF2670BLHQYbwj+pY83gFtyeySFiyMHJklrg==",
+      "version": "4.1.2",
+      "resolved": "https://registry.npmjs.org/unist-util-visit/-/unist-util-visit-4.1.2.tgz",
+      "integrity": "sha512-MSd8OUGISqHdVvfY9TPhyK2VdUrPgxkUtWSuMHF6XAAFuL4LokseigBnZtPnJMu+FbynTkFNnFlyjxpVKujMRg==",
       "dependencies": {
         "@types/unist": "^2.0.0",
         "unist-util-is": "^5.0.0",
@@ -9507,9 +9580,9 @@
       }
     },
     "node_modules/unist-util-visit-parents": {
-      "version": "5.1.1",
-      "resolved": "https://registry.npmjs.org/unist-util-visit-parents/-/unist-util-visit-parents-5.1.1.tgz",
-      "integrity": "sha512-gks4baapT/kNRaWxuGkl5BIhoanZo7sC/cUT/JToSRNL1dYoXRFl75d++NkjYk4TAu2uv2Px+l8guMajogeuiw==",
+      "version": "5.1.3",
+      "resolved": "https://registry.npmjs.org/unist-util-visit-parents/-/unist-util-visit-parents-5.1.3.tgz",
+      "integrity": "sha512-x6+y8g7wWMyQhL1iZfhIPhDAs7Xwbn9nRosDXl7qoPTSCy0yNxnKc+hWokFifWQIDGi154rdUqKvbCa4+1kLhg==",
       "dependencies": {
         "@types/unist": "^2.0.0",
         "unist-util-is": "^5.0.0"
@@ -9746,9 +9819,9 @@
       "peer": true
     },
     "node_modules/vscode-ws-jsonrpc": {
-      "version": "2.0.1",
-      "resolved": "https://registry.npmjs.org/vscode-ws-jsonrpc/-/vscode-ws-jsonrpc-2.0.1.tgz",
-      "integrity": "sha512-ne5DO8/qe8tHt1U4LafLiYS832Yd4OltkP4+YZVOQwqGEU5nwLwZowUBqqEWt8sOZ0eLdCLV9luotGC2aUQ+LA==",
+      "version": "2.0.2",
+      "resolved": "https://registry.npmjs.org/vscode-ws-jsonrpc/-/vscode-ws-jsonrpc-2.0.2.tgz",
+      "integrity": "sha512-gIOGdaWwKYwwqohgeRC8AtqqHSNghK8wA3oVcBi7UMAdZnRSAf8n4/Svtd+JHqGiIguYdNa/sC0s4IW3ZDF7mA==",
       "dependencies": {
         "vscode-jsonrpc": "8.0.2"
       },
@@ -9923,9 +9996,9 @@
       }
     },
     "node_modules/webpack-dev-middleware/node_modules/ajv": {
-      "version": "8.11.2",
-      "resolved": "https://registry.npmjs.org/ajv/-/ajv-8.11.2.tgz",
-      "integrity": "sha512-E4bfmKAhGiSTvMfL1Myyycaub+cUEU2/IvpylXkUu7CHBkBj1f/ikdzbD7YQ6FKUbixDxeYvB/xY4fvyroDlQg==",
+      "version": "8.12.0",
+      "resolved": "https://registry.npmjs.org/ajv/-/ajv-8.12.0.tgz",
+      "integrity": "sha512-sRu1kpcO9yLtYxBKvqfTeh9KzZEwO3STyX1HT+4CaDzC6HpTGYhIhPIzj9XuKU7KYDwnaeh5hcOwjy1QuJzBPA==",
       "dev": true,
       "dependencies": {
         "fast-deep-equal": "^3.1.1",
@@ -10031,9 +10104,9 @@
       }
     },
     "node_modules/webpack-dev-server/node_modules/ajv": {
-      "version": "8.11.2",
-      "resolved": "https://registry.npmjs.org/ajv/-/ajv-8.11.2.tgz",
-      "integrity": "sha512-E4bfmKAhGiSTvMfL1Myyycaub+cUEU2/IvpylXkUu7CHBkBj1f/ikdzbD7YQ6FKUbixDxeYvB/xY4fvyroDlQg==",
+      "version": "8.12.0",
+      "resolved": "https://registry.npmjs.org/ajv/-/ajv-8.12.0.tgz",
+      "integrity": "sha512-sRu1kpcO9yLtYxBKvqfTeh9KzZEwO3STyX1HT+4CaDzC6HpTGYhIhPIzj9XuKU7KYDwnaeh5hcOwjy1QuJzBPA==",
       "dev": true,
       "dependencies": {
         "fast-deep-equal": "^3.1.1",
@@ -10275,15 +10348,15 @@
       "dev": true
     },
     "node_modules/ws": {
-      "version": "8.11.0",
-      "resolved": "https://registry.npmjs.org/ws/-/ws-8.11.0.tgz",
-      "integrity": "sha512-HPG3wQd9sNQoT9xHyNCXoDUa+Xw/VevmY9FoHyQ+g+rrMn4j6FB4np7Z0OhdTgjx6MgQLK7jwSy1YecU1+4Asg==",
+      "version": "8.12.0",
+      "resolved": "https://registry.npmjs.org/ws/-/ws-8.12.0.tgz",
+      "integrity": "sha512-kU62emKIdKVeEIOIKVegvqpXMSTAMLJozpHZaJNDYqBjzlSYXQGviYwN1osDLJ9av68qHd4a2oSjd7yD4pacig==",
       "engines": {
         "node": ">=10.0.0"
       },
       "peerDependencies": {
         "bufferutil": "^4.0.1",
-        "utf-8-validate": "^5.0.2"
+        "utf-8-validate": ">=5.0.2"
       },
       "peerDependenciesMeta": {
         "bufferutil": {
diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean
index 27a8181..231a9a9 100644
--- a/server/leanserver/GameServer/Commands.lean
+++ b/server/leanserver/GameServer/Commands.lean
@@ -184,41 +184,20 @@ elab "TacticDoc" name:ident content:str : command =>
     name := name.getId,
     content := content.getString })
 
-/-- Declare a set of tactic documentation entries.
-Expect an identifier used as the set name then `:=` and a
-space separated list of identifiers.
--/
-elab "TacticSet" name:ident ":=" args:ident* : command => do
-  let docs := tacticDocExt.getState (← getEnv)
-  let mut entries : Array TacticDocEntry := #[]
-  for arg in args do
-    let name := arg.getId
-    match docs.find? (·.name = name) with
-    | some doc => entries := entries.push doc
-    | none => throwError "Documentation for tactic {name} wasn't found."
-  modifyEnv (tacticSetExt.addEntry · {
-    name := name.getId,
-    tactics := entries })
-
 instance : Quote TacticDocEntry `term :=
 ⟨λ entry => Syntax.mkCApp ``TacticDocEntry.mk #[quote entry.name, quote entry.content]⟩
 
-/-- Declare the list of tactics that will be displayed in the current level.
-Expects a space separated list of identifiers that refer to either a tactic doc
-entry or a tactic doc set. -/
-elab "Tactics" args:ident* : command => do
-  let env ← getEnv
-  let docs := tacticDocExt.getState env
-  let sets := tacticSetExt.getState env
-  let mut tactics : Array TacticDocEntry := #[]
-  for arg in args do
-    let name := arg.getId
-    match docs.find? (·.name = name) with
-    | some entry => tactics := tactics.push entry
-    | none => match sets.find? (·.name = name) with
-              | some entry => tactics := tactics ++ entry.tactics
-              | none => throwError "Tactic doc or tactic set {name} wasn't found."
-  modifyCurLevel fun level => pure {level with tactics := tactics}
+/-- Declare tactics that are introduced by this level. -/
+elab "NewTactics" args:ident* : command => do
+  modifyCurLevel fun level => pure {level with newTactics := args.map (·.getId)}
+
+/-- Declare tactics that are temporarily disabled in this level -/
+elab "DisabledTactics" args:ident* : command => do
+  modifyCurLevel fun level => pure {level with disabledTactics := args.map (·.getId)}
+
+/-- Temporarily disable all tactics except the ones declared here -/
+elab "OnlyTactics" args:ident* : command => do
+  modifyCurLevel fun level => pure {level with onlyTactics := args.map (·.getId)}
 
 /-! ## Lemmas -/
 
@@ -238,11 +217,11 @@ Expect an identifier used as the set name then `:=` and a
 space separated list of identifiers. -/
 elab "LemmaSet" name:ident ":" title:str ":=" args:ident* : command => do
   let docs := lemmaDocExt.getState (← getEnv)
-  let mut entries : Array LemmaDocEntry := #[]
+  let mut entries : Array Name := #[]
   for arg in args do
     let name := arg.getId
     match docs.find? (·.userName = name) with
-    | some doc => entries := entries.push doc
+    | some doc => entries := entries.push name
     | none => throwError "Lemma doc {name} wasn't found."
   modifyEnv (lemmaSetExt.addEntry · {
     name := name.getId,
@@ -255,16 +234,60 @@ instance : Quote LemmaDocEntry `term :=
 /-- Declare the list of lemmas that will be displayed in the current level.
 Expects a space separated list of identifiers that refer to either a lemma doc
 entry or a lemma doc set. -/
-elab "Lemmas" args:ident* : command => do
+elab "NewLemmas" args:ident* : command => do
   let env ← getEnv
   let docs := lemmaDocExt.getState env
   let sets := lemmaSetExt.getState env
-  let mut lemmas : Array LemmaDocEntry := #[]
+  let mut lemmas : Array Name := #[]
   for arg in args do
     let name := arg.getId
     match docs.find? (·.userName = name) with
-    | some entry => lemmas := lemmas.push entry
+    | some entry => lemmas := lemmas.push name
     | none => match sets.find? (·.name = name) with
               | some entry => lemmas := lemmas ++ entry.lemmas
               | none => throwError "Lemma doc or lemma set {name} wasn't found."
-  modifyCurLevel fun level => pure {level with lemmas := lemmas}
+  modifyCurLevel fun level => pure {level with newLemmas := lemmas}
+
+/-! ## 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
+  let game ← getCurGame
+
+  -- Check for loops in world graph
+  if game.worlds.hasLoops then
+    throwError "World graph has loops!"
+
+  -- Compute which tactics are available in which level:
+  let mut newTacticsInWorld : HashMap Name (HashSet Name) := {}
+  for (worldId, world) in game.worlds.nodes.toArray do
+    let mut newTactics : HashSet Name:= {}
+    for (_, level) in world.levels.toArray do
+      newTactics := newTactics.insertMany level.newTactics
+    newTacticsInWorld := newTacticsInWorld.insert worldId newTactics
+
+  let mut tacticsInWorld : HashMap Name (HashSet Name) := {}
+  for (worldId, _) in game.worlds.nodes.toArray do
+    let mut tactics : HashSet Name:= {}
+    let predecessors := game.worlds.predecessors worldId
+    for predWorldId in predecessors do
+      tactics := tactics.insertMany (newTacticsInWorld.find! predWorldId)
+    tacticsInWorld := tacticsInWorld.insert worldId tactics
+
+  for (worldId, world) in game.worlds.nodes.toArray do
+    let mut tactics := tacticsInWorld.find! worldId
+    logInfo m!"{tactics.toArray}"
+
+    let levels := world.levels.toArray.insertionSort fun a b => a.1 < b.1
+
+    for (levelId, level) in levels do
+      tactics := tactics.insertMany level.newTactics
+
+      modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
+        return {level with tactics := ← tactics.toArray.mapM getTacticDoc!}
diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean
index c4e97c6..6e726f5 100644
--- a/server/leanserver/GameServer/EnvExtensions.lean
+++ b/server/leanserver/GameServer/EnvExtensions.lean
@@ -1,4 +1,6 @@
 import Lean
+import GameServer.Graph
+
 /-! # Environment extensions
 
 The game framework stores almost all its game building data in environment extensions
@@ -45,25 +47,6 @@ elab "#print_tactic_doc" : command => do
   for entry in tacticDocExt.getState (← getEnv) do
     dbg_trace "{entry.name} : {entry.content}"
 
-structure TacticSetEntry where
-  name : Name
-  tactics : Array TacticDocEntry
-  deriving ToJson, Repr
-
-/-- Environment extension for tactic sets. -/
-initialize tacticSetExt : SimplePersistentEnvExtension TacticSetEntry (Array TacticSetEntry) ←
-  registerSimplePersistentEnvExtension {
-    name := `tactic_set
-    addEntryFn := Array.push
-    addImportedFn := Array.concatMap id
-  }
-
-open Elab Command in
-/-- Print all registered tactic sets for debugging purposes. -/
-elab "#print_tactic_set" : command => do
-  for entry in tacticSetExt.getState (← getEnv) do
-    dbg_trace "{entry.name} : {entry.tactics.map TacticDocEntry.name}"
-
 /-! ## Lemma documentation -/
 
 structure LemmaDocEntry where
@@ -90,7 +73,7 @@ elab "#print_lemma_doc" : command => do
 structure LemmaSetEntry where
   name : Name
   title : String
-  lemmas : Array LemmaDocEntry
+  lemmas : Array Name
   deriving ToJson, Repr
 
 /-- Environment extension for lemma sets. -/
@@ -105,26 +88,8 @@ open Elab Command in
 /-- Print all registered lemma sets for debugging purposes. -/
 elab "#print_lemma_set" : command => do
   for entry in lemmaSetExt.getState (← getEnv) do
-    dbg_trace "{entry.name} : {entry.lemmas.map LemmaDocEntry.name}"
-
-/-! ## Graph -/
-
-structure Graph (α β : Type) [inst : BEq α] [inst : Hashable α] where
-  nodes: HashMap α β := {}
-  edges: Array (α × α) := {}
-deriving Inhabited
-
-instance [ToJson β] : ToJson (Graph Name β) := {
-  toJson := fun graph => Json.mkObj [
-    ("nodes", Json.mkObj (graph.nodes.toList.map fun (a,b) => (a.toString, toJson b))),
-    ("edges", toJson graph.edges)
-  ]
-}
-
-instance [inst : BEq α] [inst : Hashable α] : EmptyCollection (Graph α β) := ⟨default⟩
+    dbg_trace "{entry.name} : {entry.lemmas}"
 
-def Graph.insertNode [inst : BEq α] [inst : Hashable α] (g : Graph α β) (a : α) (b : β) :=
-  {g with nodes := g.nodes.insert a b}
 
 /-! ## Environment extensions for game specification-/
 
@@ -198,7 +163,21 @@ structure GameLevel where
   introduction: String := default
   description: String := default
   conclusion: String := default
+  -- new tactics introduces by this level:
+  newTactics: Array Name := default
+  -- tactics exceptionally forbidden in this level:
+  disabledTactics: Array Name := default
+  -- only these tactics are allowed in this level (ignore if empty):
+  onlyTactics: Array Name := default
+  -- tactics in this level (computed by `MakeGame`):
   tactics: Array TacticDocEntry := default
+  -- new lemmas introduces by this level:
+  newLemmas: Array Name := default
+  -- lemmas exceptionally forbidden in this level:
+  disabledLemmas: Array Name := default
+  -- only these lemmas are allowed in this level (ignore if empty):
+  onlyLemmas: Array Name := default
+  -- lemmas in this level (computed by `MakeGame`):
   lemmas: Array LemmaDocEntry := default
   hints: Array GoalHintEntry := default
   goal : TSyntax `Lean.Parser.Command.declSig := default
@@ -329,3 +308,15 @@ def modifyCurLevel (fn : GameLevel → m GameLevel) [MonadError m] : m Unit := d
   modifyCurWorld fun world => do
     let level ← getCurLevel
     return {world with levels := world.levels.insert level.index (← fn level)}
+
+def modifyLevel (levelId : LevelId) (fn : GameLevel → m GameLevel) [MonadError m] : m Unit := do
+  let some game ← getGame? levelId.game
+    | throwError m!"Game {levelId.game} does not exist"
+  let some world := (← getCurGame).worlds.nodes.find? levelId.world
+    | throwError m!"World {levelId.world} does not exist"
+  let some level := world.levels.find? levelId.level
+    | throwError m!"Level {levelId.level} does not exist"
+  let level' ← fn level
+  let world' := {world with levels := world.levels.insert levelId.level level'}
+  let game' := {game with worlds := game.worlds.insertNode levelId.world world'}
+  insertGame levelId.game game'
diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean
index 1d1af42..88c7d61 100644
--- a/server/leanserver/GameServer/FileWorker.lean
+++ b/server/leanserver/GameServer/FileWorker.lean
@@ -17,7 +17,7 @@ private def mkErrorMessage (c : InputContext) (pos : String.Pos) (errorMsg : Str
 
 private def mkEOI (pos : String.Pos) : Syntax :=
   let atom := mkAtom (SourceInfo.original "".toSubstring pos "".toSubstring pos) ""
-  mkNode `Lean.Parser.Module.eoi #[atom]
+  mkNode ``Command.eoi #[atom]
 
 partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext)
   (mps : ModuleParserState) (messages : MessageLog) (couldBeEndSnap : Bool) :
@@ -64,6 +64,35 @@ open JsonRpc
 
 section Elab
 
+-- TODO: use HashSet for allowed tactics?
+/-- Find all tactics in syntax object that are forbidden according to a
+set `allowed` of allowed tactics. -/
+partial def findForbiddenTactics (inputCtx : Parser.InputContext) (level : GameLevel) (stx : Syntax)
+  : Elab.Command.CommandElabM Unit := do
+  match stx with
+  | .missing => return ()
+  | .node info kind args =>
+    for arg in args do
+      findForbiddenTactics inputCtx level arg
+  | .atom info val =>
+    -- ignore syntax elements that do not start with a letter
+    if 0 < val.length ∧ val.data[0]!.isAlpha then
+      if ¬ ((level.tactics.map (·.name.toString))).contains val then
+        addErrorMessage info s!"You have not unlocked the tactic '{val}' yet!"
+      else if level.disabledTactics.contains val
+        ∨ (¬ level.onlyTactics.isEmpty ∧ ¬ level.onlyTactics.contains val)then
+        addErrorMessage info s!"The tactic '{val}' is disabled in this level!"
+  | .ident info rawVal val preresolved => return ()
+where addErrorMessage (info : SourceInfo) (s : MessageData) :=
+  modify fun st => { st with
+    messages := st.messages.add {
+      fileName := inputCtx.fileName
+      severity := MessageSeverity.error
+      pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
+      data     := s
+    }
+  }
+
 open Elab Meta Expr in
 def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool) (couldBeEndSnap : Bool) : IO Snapshot := do
   let cmdState := snap.cmdState
@@ -98,15 +127,20 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
       Elab.Command.catchExceptions
         (getResetInfoTrees *> do
           let level ← GameServer.getLevelByFileName inputCtx.fileName
+
+          -- Check for forbidden tactics
+          findForbiddenTactics inputCtx level tacticStx
+
           -- Insert invisible `skip` command to make sure we always display the initial goal
           let skip := Syntax.node (.original default 0 default endOfWhitespace) ``Lean.Parser.Tactic.skip #[]
           -- Insert final `done` command to display unsolved goal error in the end
           let done := Syntax.node (.synthetic cmdParserState.pos cmdParserState.pos) ``Lean.Parser.Tactic.done #[]
           let tacticStx := (#[skip] ++ tacticStx.getArgs ++ #[done]).map (⟨.⟩)
           let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*)
+
           let cmdStx ← `(command|
             set_option tactic.hygienic false in
-            theorem my_theorem $(level.goal) := by {$(⟨tacticStx⟩)} )
+            theorem the_theorem $(level.goal) := by {$(⟨tacticStx⟩)} )
           Elab.Command.elabCommandTopLevel cmdStx)
         cmdCtx cmdStateRef
     let postNew := (← tacticCacheNew.get).post
@@ -122,6 +156,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           data     := output
         }
       }
+
     let postCmdSnap : Snapshot := {
       beginPos := cmdPos
       stx := tacticStx
diff --git a/server/leanserver/GameServer/Graph.lean b/server/leanserver/GameServer/Graph.lean
new file mode 100644
index 0000000..faf826e
--- /dev/null
+++ b/server/leanserver/GameServer/Graph.lean
@@ -0,0 +1,69 @@
+import Lean
+
+open Lean Meta
+
+/-! ## Graph -/
+
+variable [inst : BEq α] [inst : Hashable α]
+
+structure Graph (α β : Type) [inst : BEq α] [inst : Hashable α] where
+  nodes: HashMap α β := {}
+  edges: Array (α × α) := {}
+deriving Inhabited
+
+instance [ToJson β] : ToJson (Graph Name β) := {
+  toJson := fun graph => Json.mkObj [
+    ("nodes", Json.mkObj (graph.nodes.toList.map fun (a,b) => (a.toString, toJson b))),
+    ("edges", toJson graph.edges)
+  ]
+}
+
+instance  : EmptyCollection (Graph α β) := ⟨default⟩
+
+def Graph.insertNode (g : Graph α β) (a : α) (b : β) :=
+  {g with nodes := g.nodes.insert a b}
+
+/-- Check if graph contains loops -/
+partial def Graph.hasLoops (g : Graph α β) (visited0 : HashSet α := {}): Bool := Id.run do
+  let mut visited : HashSet α := visited0
+  let all : Array α := g.nodes.toArray.map (·.1)
+
+  -- find some node that we haven't visited
+  let some x := all.find? fun x => ¬ visited.contains x
+    | return false -- We have visted all nodes and found no loops
+  visited := visited.insert x
+
+  match visitSuccessors x x visited with -- visit all recursive successors of x
+  | some visited' => visited := visited'
+  | none => return true -- none means a loop has been found
+
+  g.hasLoops visited -- continue looking for unvisited nodes
+
+where
+  visitSuccessors (x : α) (x0 : α) (visited0 : HashSet α) : Option (HashSet α) := Id.run do
+    let mut visited : HashSet α := visited0
+
+    let directSuccessors := (g.edges.filter (·.1 == x)).map (·.2)
+    for y in directSuccessors do
+      if y == x0 then
+        return none -- loop found
+      if visited.contains y then
+        continue -- no loop possible here because the visited nodes do not lead to x0
+      visited := visited.insert y
+      match visitSuccessors y x0 visited with
+      | some visited' => visited := visited'
+      | none => return none
+
+    return some visited
+
+-- #eval Graph.hasLoops ⟨HashMap.ofList [(2,2), (1,1)], #[(2,1)]⟩
+
+partial def Graph.predecessors (g : Graph α β) (x : α) (acc : HashSet α := {}) : HashSet α := Id.run do
+  let mut res := acc
+  let directPredecessors := (g.edges.filter (·.2 == x)).map (·.1)
+  for y in directPredecessors do
+    if ¬ res.contains y then
+      res := res.insert y
+      res := g.predecessors y res
+
+  return res
diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean
index 246233a..eacf2ca 100644
--- a/server/testgame/TestGame.lean
+++ b/server/testgame/TestGame.lean
@@ -39,9 +39,12 @@ Conclusion
 
 
 Path Proposition → Implication → Predicate → Contradiction → LeanStuff
---Path Predicate → Prime
+-- Path Predicate → Prime
 Path Predicate → Induction → LeanStuff → Function → SetFunction
 
 Path LeanStuff → SetTheory → SetFunction
 
 Path SetTheory → SetTheory2
+
+
+MakeGame
diff --git a/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean b/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean
index 467ffee..b4b4ddf 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean
@@ -63,6 +63,6 @@ have k : ¬ B
 
 Conclusion ""
 
-Tactics contradiction rcases haveₓ assumption apply
+NewTactics contradiction rcases haveₓ assumption apply
 
-Lemmas Even Odd not_even not_odd
+NewLemmas Even Odd not_even not_odd
diff --git a/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean b/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean
index 29e586e..4f36b7a 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean
@@ -60,6 +60,6 @@ Hint (A : Prop) (B : Prop) (h : A → ¬ B) (g : A) (f : B) : False =>
 
 Conclusion ""
 
-Tactics contradiction apply assumption rcases sufficesₓ
+NewTactics contradiction apply assumption rcases sufficesₓ
 
-Lemmas Even Odd not_even not_odd
+NewLemmas Even Odd not_even not_odd
diff --git a/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean b/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean
index 17fadbf..50a5246 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean
@@ -52,4 +52,4 @@ HiddenHint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False =>
 
 Conclusion ""
 
-Tactics by_contra sufficesₓ haveₓ contradiction apply assumption
+NewTactics by_contra sufficesₓ haveₓ contradiction apply assumption
diff --git a/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean b/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean
index c4d44df..d3cbe73 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean
@@ -46,4 +46,4 @@ HiddenHint (A : Prop) (B : Prop) : A → B ↔ (¬ B → ¬ A) =>
 
 Conclusion ""
 
-Tactics contradiction constructor intro by_contra sufficesₓ haveₓ apply assumption
+NewTactics contradiction constructor intro by_contra sufficesₓ haveₓ apply assumption
diff --git a/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean b/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean
index ed3f32d..cec04e7 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean
@@ -61,5 +61,5 @@ Hint (n : ℕ) : Even n → ¬Odd (n ^ 2) =>
 Hint (n : ℕ) : Even n → Even (n ^ 2) =>
 "Diese Aussage hast du bereits als Lemma bewiesen, schau mal in der Bibliothek."
 
-Tactics contrapose rw apply
-Lemmas Even Odd not_even not_odd even_square
+NewTactics contrapose rw apply
+NewLemmas Even Odd not_even not_odd even_square
diff --git a/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean b/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean
index 20dc4ac..d700e70 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean
@@ -71,6 +71,6 @@ HiddenHint (n: ℕ) (h : Odd (n ^ 2)) (g : Even n) : Even (n ^ 2) =>
 "Probiers mit `apply ...`"
 
 
-Tactics contradiction by_contra rw apply assumption -- TODO: suffices, have
+NewTactics contradiction by_contra rw apply assumption -- TODO: suffices, have
 
-Lemmas Odd Even not_odd not_even even_square
+NewLemmas Odd Even not_odd not_even even_square
diff --git a/server/testgame/TestGame/Levels/Function/L01_xxx.lean b/server/testgame/TestGame/Levels/Function/L01_xxx.lean
index 651b853..4048f5a 100644
--- a/server/testgame/TestGame/Levels/Function/L01_xxx.lean
+++ b/server/testgame/TestGame/Levels/Function/L01_xxx.lean
@@ -23,4 +23,4 @@ Statement
     : True := by
   trivial
 
-Tactics rw
+NewTactics rw
diff --git a/server/testgame/TestGame/Levels/Implication/L01_Intro.lean b/server/testgame/TestGame/Levels/Implication/L01_Intro.lean
index d5735cf..292005b 100644
--- a/server/testgame/TestGame/Levels/Implication/L01_Intro.lean
+++ b/server/testgame/TestGame/Levels/Implication/L01_Intro.lean
@@ -37,4 +37,4 @@ HiddenHint (A : Prop) (B : Prop) (hb : B) : A → (A ∧ B) =>
 Hint (A : Prop) (B : Prop) (ha : A) (hb : B) : (A ∧ B) =>
 "Jetzt kannst du die Taktiken aus dem letzten Kapitel verwenden."
 
-Tactics intro constructor assumption
+NewTactics intro constructor assumption
diff --git a/server/testgame/TestGame/Levels/Implication/L02_Revert.lean b/server/testgame/TestGame/Levels/Implication/L02_Revert.lean
index e76d7eb..74452a8 100644
--- a/server/testgame/TestGame/Levels/Implication/L02_Revert.lean
+++ b/server/testgame/TestGame/Levels/Implication/L02_Revert.lean
@@ -39,4 +39,4 @@ dass $B$ wahr ist."
 HiddenHint (A : Prop) (B : Prop) (ha : A) (h : A → B): B =>
 "Mit `revert ha` kann man die Annahme `ha` als Implikationsprämisse vorne ans Goal anhängen."
 
-Tactics revert assumption
+NewTactics revert assumption
diff --git a/server/testgame/TestGame/Levels/Implication/L03_Apply.lean b/server/testgame/TestGame/Levels/Implication/L03_Apply.lean
index 7727721..71272b2 100644
--- a/server/testgame/TestGame/Levels/Implication/L03_Apply.lean
+++ b/server/testgame/TestGame/Levels/Implication/L03_Apply.lean
@@ -32,7 +32,7 @@ HiddenHint (A : Prop) (B : Prop) (hA : A) (g : A → B) : A =>
 "Nachdem du die Implikation `A → B` angewendet hast, musst du nur noch $A$ zeigen,
 dafür hast du bereits einen Beweis in den Annahmen."
 
-Tactics apply assumption
+NewTactics apply assumption
 
 -- Katex notes
 -- `\\(    \\)` or `$   $` for inline
diff --git a/server/testgame/TestGame/Levels/Implication/L04_Apply.lean b/server/testgame/TestGame/Levels/Implication/L04_Apply.lean
index 7d18abc..e227720 100644
--- a/server/testgame/TestGame/Levels/Implication/L04_Apply.lean
+++ b/server/testgame/TestGame/Levels/Implication/L04_Apply.lean
@@ -32,4 +32,4 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C)
 "Du willst $C$ beweisen. Suche also nach einer Implikation $\\ldots \\Rightarrow C$ und wende
 diese mit `apply` an."
 
-Tactics intro apply assumption revert
+NewTactics intro apply assumption revert
diff --git a/server/testgame/TestGame/Levels/Implication/L05_Apply.lean b/server/testgame/TestGame/Levels/Implication/L05_Apply.lean
index 155127c..83292a5 100644
--- a/server/testgame/TestGame/Levels/Implication/L05_Apply.lean
+++ b/server/testgame/TestGame/Levels/Implication/L05_Apply.lean
@@ -48,6 +48,6 @@ Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
     (i : D → E) (k : E → F) (m : C → F) : D =>
 "Sackgasse. Probier doch einen anderen Weg."
 
-Tactics apply assumption revert intro
+NewTactics apply assumption revert intro
 
 -- https://www.jmilne.org/not/Mamscd.pdf
diff --git a/server/testgame/TestGame/Levels/Implication/L06_Iff.lean b/server/testgame/TestGame/Levels/Implication/L06_Iff.lean
index 54b93c8..dee2b57 100644
--- a/server/testgame/TestGame/Levels/Implication/L06_Iff.lean
+++ b/server/testgame/TestGame/Levels/Implication/L06_Iff.lean
@@ -38,6 +38,6 @@ aus mehreren Einzelteilen besteht: `⟨A → B, B → A⟩`. Man sagt also Lean,
 ob das Goal aus solchen Einzelteilen \"konstruiert\" werden kann.
 "
 
-Tactics constructor assumption
+NewTactics constructor assumption
 
 -- TODO : `case mpr =>` ist mathematisch noch sinnvoll.
diff --git a/server/testgame/TestGame/Levels/Implication/L07_Rw.lean b/server/testgame/TestGame/Levels/Implication/L07_Rw.lean
index 93d67bd..17ca7d9 100644
--- a/server/testgame/TestGame/Levels/Implication/L07_Rw.lean
+++ b/server/testgame/TestGame/Levels/Implication/L07_Rw.lean
@@ -71,4 +71,4 @@ Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : D ↔
 "Das ist nicht der optimale Weg..."
 
 
-Tactics rw assumption
+NewTactics rw assumption
diff --git a/server/testgame/TestGame/Levels/Implication/L08_Iff.lean b/server/testgame/TestGame/Levels/Implication/L08_Iff.lean
index d0cabaf..0bf64f0 100644
--- a/server/testgame/TestGame/Levels/Implication/L08_Iff.lean
+++ b/server/testgame/TestGame/Levels/Implication/L08_Iff.lean
@@ -41,4 +41,4 @@ Hint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : B =
 
 Conclusion "Im nächsten Level findest du die zweite Option."
 
-Tactics apply assumption
+NewTactics apply assumption
diff --git a/server/testgame/TestGame/Levels/Implication/L09_Iff.lean b/server/testgame/TestGame/Levels/Implication/L09_Iff.lean
index 41f7c4f..a3c6fe2 100644
--- a/server/testgame/TestGame/Levels/Implication/L09_Iff.lean
+++ b/server/testgame/TestGame/Levels/Implication/L09_Iff.lean
@@ -36,7 +36,7 @@ Conclusion
 "
 "
 
-Tactics intro apply rcases assumption
+NewTactics intro apply rcases assumption
 
 -- -- TODO: The new `cases` works differntly. There is also `cases'`
 -- example (A B : Prop) : (A ↔ B) → (A → B) := by
diff --git a/server/testgame/TestGame/Levels/Implication/L10_Apply.lean b/server/testgame/TestGame/Levels/Implication/L10_Apply.lean
index 4b57f5c..4bea8e4 100644
--- a/server/testgame/TestGame/Levels/Implication/L10_Apply.lean
+++ b/server/testgame/TestGame/Levels/Implication/L10_Apply.lean
@@ -50,6 +50,6 @@ Conclusion
 "
 "
 
-Tactics apply left right assumption
+NewTactics apply left right assumption
 
-Lemmas not_or_of_imp
+NewLemmas not_or_of_imp
diff --git a/server/testgame/TestGame/Levels/Implication/L11_Rw.lean b/server/testgame/TestGame/Levels/Implication/L11_Rw.lean
index 6370dc9..1151fb4 100644
--- a/server/testgame/TestGame/Levels/Implication/L11_Rw.lean
+++ b/server/testgame/TestGame/Levels/Implication/L11_Rw.lean
@@ -34,6 +34,6 @@ Conclusion
 `rw` hat automatisch `rfl` ausgeführt und dadurch den Beweis beendet.
 "
 
-Tactics rw
+NewTactics rw
 
-Lemmas not_not not_or_of_imp
+NewLemmas not_not not_or_of_imp
diff --git a/server/testgame/TestGame/Levels/Implication/L12_Summary.lean b/server/testgame/TestGame/Levels/Implication/L12_Summary.lean
index 6569583..7a64ade 100644
--- a/server/testgame/TestGame/Levels/Implication/L12_Summary.lean
+++ b/server/testgame/TestGame/Levels/Implication/L12_Summary.lean
@@ -76,6 +76,6 @@ HiddenHint (A : Prop) (B: Prop) (h : ¬ A ∨ B) (ha : A) : B =>
 HiddenHint (A : Prop) (B: Prop) (ha : A) (ha' : ¬A) : B =>
 "Findest du einen Widerspruch?"
 
-Tactics rfl assumption trivial left right constructor rcases
+NewTactics rfl assumption trivial left right constructor rcases
 
-Lemmas not_not not_or_of_imp
+NewLemmas not_not not_or_of_imp
diff --git a/server/testgame/TestGame/Levels/Induction/L01_Simp.lean b/server/testgame/TestGame/Levels/Induction/L01_Simp.lean
index 8eef726..f1fd429 100644
--- a/server/testgame/TestGame/Levels/Induction/L01_Simp.lean
+++ b/server/testgame/TestGame/Levels/Induction/L01_Simp.lean
@@ -43,4 +43,4 @@ Statement
     (n : ℕ) : (∑ i : Fin n, (0 + 0)) = 0 := by
   simp
 
-Tactics simp
+NewTactics simp
diff --git a/server/testgame/TestGame/Levels/Induction/L02_Sum.lean b/server/testgame/TestGame/Levels/Induction/L02_Sum.lean
index 224ec3c..646dccd 100644
--- a/server/testgame/TestGame/Levels/Induction/L02_Sum.lean
+++ b/server/testgame/TestGame/Levels/Induction/L02_Sum.lean
@@ -34,4 +34,4 @@ Statement
   simp
   ring
 
-Tactics rw simp ring
+NewTactics rw simp ring
diff --git a/server/testgame/TestGame/Levels/Induction/L03_Induction.lean b/server/testgame/TestGame/Levels/Induction/L03_Induction.lean
index 3d37c74..a20396c 100644
--- a/server/testgame/TestGame/Levels/Induction/L03_Induction.lean
+++ b/server/testgame/TestGame/Levels/Induction/L03_Induction.lean
@@ -42,4 +42,4 @@ Statement arithmetic_sum
   simp_rw [Nat.succ_eq_one_add]
   ring
 
-Tactics ring
+NewTactics ring
diff --git a/server/testgame/TestGame/Levels/Induction/L04_SumOdd.lean b/server/testgame/TestGame/Levels/Induction/L04_SumOdd.lean
index 2741bdf..3e864a0 100644
--- a/server/testgame/TestGame/Levels/Induction/L04_SumOdd.lean
+++ b/server/testgame/TestGame/Levels/Induction/L04_SumOdd.lean
@@ -27,4 +27,4 @@ $\\sum_{i = 0}^n (2n + 1) = n ^ 2$."
   rw [hn, Nat.succ_eq_add_one]
   ring
 
-Tactics ring
+NewTactics ring
diff --git a/server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean b/server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean
index 02e4c0b..876b75c 100644
--- a/server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean
+++ b/server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean
@@ -44,4 +44,4 @@ Statement
   -- rw [mul_add, hn]
   -- ring
 
-Tactics ring
+NewTactics ring
diff --git a/server/testgame/TestGame/Levels/Induction/T00_Sum.lean b/server/testgame/TestGame/Levels/Induction/T00_Sum.lean
index c57f5f3..73a7454 100644
--- a/server/testgame/TestGame/Levels/Induction/T00_Sum.lean
+++ b/server/testgame/TestGame/Levels/Induction/T00_Sum.lean
@@ -44,4 +44,4 @@ Statement
     rw [hn]
 
 
-Tactics ring
+NewTactics ring
diff --git a/server/testgame/TestGame/Levels/Induction/T01_Induction.lean b/server/testgame/TestGame/Levels/Induction/T01_Induction.lean
index 8dd5c1e..296806c 100644
--- a/server/testgame/TestGame/Levels/Induction/T01_Induction.lean
+++ b/server/testgame/TestGame/Levels/Induction/T01_Induction.lean
@@ -29,4 +29,4 @@ example (n : ℕ) (h : 5 ≤ n) : n^2 < 2 ^ n
   sorry
 | n + 5  => by sorry
 
-Tactics rw simp ring
+NewTactics rw simp ring
diff --git a/server/testgame/TestGame/Levels/Induction/T02_Induction.lean b/server/testgame/TestGame/Levels/Induction/T02_Induction.lean
index 8b53ad1..7385153 100644
--- a/server/testgame/TestGame/Levels/Induction/T02_Induction.lean
+++ b/server/testgame/TestGame/Levels/Induction/T02_Induction.lean
@@ -23,10 +23,4 @@ Statement
   sorry
   sorry
 
-Tactics rw simp ring
-
--- example (n : ℕ) : (n - 1) * (n + 1) = (n ^ 2 - 1) := by
---   induction' n with n hn
---   ring
---   rw [Nat.succ_eq_one_add]
---   rw []
+NewTactics rw simp ring
diff --git a/server/testgame/TestGame/Levels/Induction/T03_SumComm.lean b/server/testgame/TestGame/Levels/Induction/T03_SumComm.lean
index f23163b..96e789f 100644
--- a/server/testgame/TestGame/Levels/Induction/T03_SumComm.lean
+++ b/server/testgame/TestGame/Levels/Induction/T03_SumComm.lean
@@ -21,7 +21,7 @@ Statement
     (n : ℕ) : True := by
   trivial
 
-Tactics simp
+NewTactics simp
 
 
 -- Σ_i Σ_j ... = Σ_j Σ_i ...
diff --git a/server/testgame/TestGame/Levels/LeanStuff/L01_xxx.lean b/server/testgame/TestGame/Levels/LeanStuff/L01_xxx.lean
index e7b21c8..f46dbdb 100644
--- a/server/testgame/TestGame/Levels/LeanStuff/L01_xxx.lean
+++ b/server/testgame/TestGame/Levels/LeanStuff/L01_xxx.lean
@@ -29,4 +29,4 @@ Statement
     "TODO" : True := by
   trivial
 
-Tactics rw
+NewTactics rw
diff --git a/server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean b/server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean
index 17930a8..e6f93aa 100644
--- a/server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean
+++ b/server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean
@@ -67,4 +67,4 @@ Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C ∧ A =>
 Hint (A : Prop) (B : Prop) (C : Prop) (h : A → C) : C ∧ A =>
 "Ein UND im Goal kann mit `constructor` aufgeteilt werden."
 
-Tactics left right assumption constructor rcases
+NewTactics left right assumption constructor rcases
diff --git a/server/testgame/TestGame/Levels/LeftOvers/L33_Prime.lean b/server/testgame/TestGame/Levels/LeftOvers/L33_Prime.lean
index acce168..ba06057 100644
--- a/server/testgame/TestGame/Levels/LeftOvers/L33_Prime.lean
+++ b/server/testgame/TestGame/Levels/LeftOvers/L33_Prime.lean
@@ -20,4 +20,4 @@ Conclusion
 "
 "
 
-Tactics ring
+NewTactics ring
diff --git a/server/testgame/TestGame/Levels/LeftOvers/L34_ExistsUnique.lean b/server/testgame/TestGame/Levels/LeftOvers/L34_ExistsUnique.lean
index de45f47..ce83d69 100644
--- a/server/testgame/TestGame/Levels/LeftOvers/L34_ExistsUnique.lean
+++ b/server/testgame/TestGame/Levels/LeftOvers/L34_ExistsUnique.lean
@@ -20,4 +20,4 @@ Conclusion
 "
 "
 
-Tactics ring
+NewTactics ring
diff --git a/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean b/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean
index b0f6232..610ec64 100644
--- a/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean
+++ b/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean
@@ -58,4 +58,4 @@ Hint (n : ℕ) (hn : odd n) (h : ∀ (x : ℕ), (odd x) → even (x + 1)) : even
 "`∀ (x : ℕ), (odd x) → even (x + 1)` ist eigentlich das gleiche wie
 `(x : ℕ) → `"
 
-Tactics ring intro unfold
+NewTactics ring intro unfold
diff --git a/server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean b/server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean
index 84c8044..129c126 100644
--- a/server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean
+++ b/server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean
@@ -22,4 +22,4 @@ Statement : ∃ (f : ℕ → ℕ), ∀ (x : ℕ), f x = 0 := by
 
 Conclusion ""
 
-Tactics use simp
+NewTactics use simp
diff --git a/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean b/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean
index 31c3006..52d5908 100644
--- a/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean
@@ -39,6 +39,6 @@ Ring zu lösen, funktioniert aber auch auf `ℕ`, auch wenn dieses kein Ring ist
 (erst `ℤ` ist ein Ring).
 "
 
-Tactics ring
+NewTactics ring
 
 #eval 4 / 6
diff --git a/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean b/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean
index 22ee139..9e8f068 100644
--- a/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean
@@ -67,4 +67,4 @@ Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : d = b) (h₃
 
 Conclusion "Übrigens, mit `rw [h₁, ←h₂]` könnte man mehrere `rw` zusammenfassen."
 
-Tactics assumption rw
+NewTactics assumption rw
diff --git a/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean b/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean
index 2395208..2320b54 100644
--- a/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean
@@ -37,4 +37,4 @@ Hint (a : ℕ) (b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : a + a ^ 2 = a + 1
 Conclusion "Übrigens, mit `rw [h] at *` kann man im weiteren `h` in **allen** Annahmen und
 dem Goal umschreiben."
 
-Tactics assumption rw
+NewTactics assumption rw
diff --git a/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean b/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean
index 42460c2..3d1f19d 100644
--- a/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean
@@ -30,4 +30,4 @@ Hint (y : ℕ) : (2 * y + 1) ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y =>
 
 Conclusion ""
 
-Tactics ring rw
+NewTactics ring rw
diff --git a/server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean b/server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean
index 73a940f..32ecad3 100644
--- a/server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean
@@ -28,4 +28,4 @@ Conclusion
 aufzurufen, deshalb brauchst du das nur noch selten.
 "
 
-Tactics rfl
+NewTactics rfl
diff --git a/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean b/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean
index 8bbcd67..9ae29ce 100644
--- a/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean
@@ -67,5 +67,5 @@ Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : n ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 =>
 Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : (x + x) ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 =>
 "Die Taktik `ring` löst solche Gleichungen."
 
-Tactics unfold rcases use rw ring
-Lemmas Even Odd
+NewTactics unfold rcases use rw ring
+NewLemmas Even Odd
diff --git a/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean b/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean
index 9d6af52..5e1b812 100644
--- a/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean
@@ -50,4 +50,4 @@ Hint (n : ℕ) (hn : Odd n) (h : ∀ (x : ℕ), (Odd x) → Even (x + 1)) : Even
 Conclusion "Für-alle-Statements, Implikationen und Lemmas/Theoreme verhalten sich alle
 praktisch gleich. Mehr dazu später."
 
-Tactics ring intro unfold
+NewTactics ring intro unfold
diff --git a/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean b/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean
index 306dd9e..24f03a5 100644
--- a/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean
@@ -62,6 +62,6 @@ Hint (n : ℕ) : n + n = 2 * n => "Recap: `ring` löst Gleichungen in `ℕ`."
 
 Conclusion ""
 
-Tactics push_neg intro use rw unfold ring
+NewTactics push_neg intro use rw unfold ring
 
-Lemmas Even Odd not_even not_odd not_exists not_forall
+NewLemmas Even Odd not_even not_odd not_exists not_forall
diff --git a/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean b/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean
index 0ba22c4..00f7730 100644
--- a/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean
@@ -50,6 +50,6 @@ Statement
 
 Conclusion ""
 
-Tactics push_neg intro use rw unfold ring
+NewTactics push_neg intro use rw unfold ring
 
-Lemmas Even Odd not_even not_odd not_exists not_forall
+NewLemmas Even Odd not_even not_odd not_exists not_forall
diff --git a/server/testgame/TestGame/Levels/Prime/L01_Prime.lean b/server/testgame/TestGame/Levels/Prime/L01_Prime.lean
index b6a177b..2361ca8 100644
--- a/server/testgame/TestGame/Levels/Prime/L01_Prime.lean
+++ b/server/testgame/TestGame/Levels/Prime/L01_Prime.lean
@@ -36,6 +36,6 @@ example : True := by
 
 Conclusion ""
 
-Tactics
+NewTactics
 
-Lemmas
+NewLemmas
diff --git a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean
index 5824a91..4c09230 100644
--- a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean
@@ -48,4 +48,4 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop): ¬((¬B ∨ ¬ C) ∨ (A → B)) 
 
 Conclusion ""
 
-Tactics tauto
+NewTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
index 2171491..614490b 100644
--- a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
@@ -27,4 +27,5 @@ HiddenHint : 42 = 42 =>
 
 Conclusion "Bravo! PS: `rfl` steht für \"reflexivity\"."
 
-Tactics rfl
+NewTactics rfl
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
index 21fb31f..754aae9 100644
--- a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
@@ -32,4 +32,5 @@ HiddenHint (n : ℕ) (h : 1 < n) : 1 < n =>
 
 Conclusion ""
 
-Tactics assumption
+NewTactics assumption
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean
index bb038f2..a8ff296 100644
--- a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean
@@ -27,4 +27,5 @@ HiddenHint (A : Prop) (hA : A) : A =>
 
 Conclusion ""
 
-Tactics assumption
+NewTactics assumption
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L04_True.lean b/server/testgame/TestGame/Levels/Proposition/L04_True.lean
index bbbac31..352ce3e 100644
--- a/server/testgame/TestGame/Levels/Proposition/L04_True.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L04_True.lean
@@ -33,4 +33,5 @@ True := by
 
 Conclusion ""
 
-Tactics trivial
+NewTactics trivial
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
index 0aaf9df..1030b90 100644
--- a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
@@ -21,4 +21,5 @@ Statement
 
 Conclusion ""
 
-Tactics trivial
+NewTactics trivial
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L06_False.lean b/server/testgame/TestGame/Levels/Proposition/L06_False.lean
index 990f282..b81feb4 100644
--- a/server/testgame/TestGame/Levels/Proposition/L06_False.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L06_False.lean
@@ -27,4 +27,5 @@ HiddenHint (A : Prop) (h : False) : A =>
 "Wenn man einen Beweis von `False` hat, kann man mit `contradiction` das Goal beweisen,
 unabhängig davon, was das Goal ist."
 
-Tactics contradiction
+NewTactics contradiction
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean
index 286dbc1..d2d6309 100644
--- a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean
@@ -26,4 +26,5 @@ Conclusion
 "
 "
 
-Tactics contradiction
+NewTactics contradiction
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean
index e2ee09f..dca804b 100644
--- a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean
@@ -29,4 +29,5 @@ Conclusion
 "
 "
 
-Tactics contradiction
+NewTactics contradiction
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L09_And.lean b/server/testgame/TestGame/Levels/Proposition/L09_And.lean
index f33a175..9aa3f37 100644
--- a/server/testgame/TestGame/Levels/Proposition/L09_And.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L09_And.lean
@@ -32,7 +32,8 @@ HiddenHint (A : Prop) (B : Prop) (hA : A) (hB : B) : A ∧ B =>
 HiddenHint (A : Prop) (hA : A) : A =>
   "Du hast einen Beweis dafür in den *Annahmen*."
 
-Tactics constructor assumption
+NewTactics constructor assumption
+DisabledTactics tauto
 
 -- Statement
 --     "Zeige $(A \\land (A \\Rightarrow B)) \\iff (A \\land B)$."
diff --git a/server/testgame/TestGame/Levels/Proposition/L10_And.lean b/server/testgame/TestGame/Levels/Proposition/L10_And.lean
index fe85f6a..6579ff7 100644
--- a/server/testgame/TestGame/Levels/Proposition/L10_And.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L10_And.lean
@@ -33,7 +33,8 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ (B ∧ C)) : B =>
 HiddenHint (A : Prop) (hA : A) : A =>
   "Du hast einen Beweis dafür in den *Annahmen*."
 
-Tactics constructor assumption
+NewTactics constructor assumption
+DisabledTactics tauto
 
 -- Statement
 --     "Zeige $(A \\land (A \\Rightarrow B)) \\iff (A \\land B)$."
diff --git a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean
index 62d5147..deeb72e 100644
--- a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean
@@ -30,4 +30,5 @@ HiddenHint (A : Prop) (B : Prop) (hA : A) : A ∨ (¬ B) =>
 Hint (A : Prop) (B : Prop) (hA : A) : ¬ B =>
 "Sackgasse. Probier's nochmals."
 
-Tactics left right assumption
+NewTactics left right assumption
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean
index 984d6a6..272dc84 100644
--- a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean
@@ -44,4 +44,5 @@ HiddenHint (A : Prop) (B : Prop) (h : A ∨ (A ∧ B)) : A =>
 Hint (A : Prop) (B : Prop) (h : A ∧ B) : A =>
 "Jetzt noch das UND in den Annahmen mit `rcases h with ⟨h₁, h₂⟩` zerlegen."
 
-Tactics assumption rcases
+NewTactics assumption rcases
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
index b05193a..00f1f86 100644
--- a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
@@ -122,4 +122,5 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ C) =>
 HiddenHint (A : Prop) (B : Prop) : A ∨ B =>
 "`left` oder `right`?"
 
-Tactics left right assumption constructor rcases rfl contradiction trivial
+NewTactics left right assumption constructor rcases rfl contradiction trivial
+DisabledTactics tauto
diff --git a/server/testgame/TestGame/Levels/SetFunction/L01_xxx.lean b/server/testgame/TestGame/Levels/SetFunction/L01_xxx.lean
index 56fa09b..b2bf693 100644
--- a/server/testgame/TestGame/Levels/SetFunction/L01_xxx.lean
+++ b/server/testgame/TestGame/Levels/SetFunction/L01_xxx.lean
@@ -21,4 +21,4 @@ Statement
     : True := by
   trivial
 
-Tactics rw
+NewTactics rw
diff --git a/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean b/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean
index eb240e9..90ff1f8 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean
@@ -39,4 +39,4 @@ Statement mem_univ
   trivial
   -- tauto
 
-Tactics tauto trivial
+NewTactics tauto trivial
diff --git a/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
index 483a8d3..eac4906 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
@@ -39,7 +39,7 @@ Statement subset_empty_iff
   intro h hA
   apply mem_univ -- or `trivial`.
 
-Tactics intro trivial apply
+NewTactics intro trivial apply
 -- blocked: tauto simp
 
 end MySet
diff --git a/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean b/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
index 1307805..3aeaf5c 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
@@ -54,8 +54,8 @@ Statement subset_empty_iff
   rcases a with ⟨h₁, h₂⟩
   assumption
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
 
 end MySet
diff --git a/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean b/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean
index 40260ab..c9b9908 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean
@@ -45,8 +45,8 @@ Statement eq_empty_iff_forall_not_mem
   rw [←subset_empty_iff]
   rfl -- This is quite a miracle :)
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
 
 end MySet
diff --git a/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean b/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean
index 55585e8..88e28b0 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean
@@ -30,6 +30,6 @@ Statement nonempty_iff_ne_empty
   push_neg
   rfl
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean b/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean
index 9bd7bf9..5a7a792 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean
@@ -26,6 +26,6 @@ Statement
 "" (A B : Set ℕ) : (A ∪ ∅) ∩ B = A ∩ (univ ∩ B) := by
   simp
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean b/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean
index 918313d..af7deeb 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean
@@ -30,6 +30,6 @@ Statement
   rw [←union_diff_distrib]
   rw [univ_union]
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean b/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean
index bef711c..b48d09b 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean
@@ -30,6 +30,6 @@ Statement
   rw [←not_mem_compl_iff]
   exact h4
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L10_Morgan.lean b/server/testgame/TestGame/Levels/SetTheory/L10_Morgan.lean
index 556d3c5..e61fcd3 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L10_Morgan.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L10_Morgan.lean
@@ -22,7 +22,7 @@ man die de-Morganschen Regeln einfach selber beweisen könnten.
 
 
 Die meisten Aufgaben über Mengen sind eine Kombination von `rw` und `simp_rw` verschiedenster
-Lemmas in `import Mathlib.Data.Set`.
+NewLemmas in `import Mathlib.Data.Set`.
 
 Die Taktik `simp_rw` funktioniert ähnlich wie `rw`, aber sie versucht jedes Lemma so oft
 wie möglich anzuwenden. Wir kennen also 4 etwas verwandte Optionen um Lemmas und Theoreme zu
@@ -52,7 +52,7 @@ Statement
   rw [diff_eq_compl_inter]
   rw [inter_comm]
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
 -- TODOs
 -- Lemmas compl_union compl_inter mem_compl_iff
diff --git a/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean b/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean
index dfae8fd..652584a 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean
@@ -33,6 +33,6 @@ Statement
   rw [Set.mem_diff]
   exact hx
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean b/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean
index 2501949..6b03d1b 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean
@@ -32,6 +32,6 @@ Statement
     ({4, 9} : Set ℕ) = Set.insert 4 {9} := by
   rfl
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L13_Insert.lean b/server/testgame/TestGame/Levels/SetTheory/L13_Insert.lean
index dde8c82..daf6062 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L13_Insert.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L13_Insert.lean
@@ -35,5 +35,5 @@ Statement
   simp_rw [mem_insert_iff, mem_singleton_iff] at *
   tauto
 
-Tactics simp_rw intro tauto rw
+NewTactics simp_rw intro tauto rw
 --Lemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean b/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean
index 68974a9..bc6e273 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean
@@ -32,6 +32,6 @@ Statement
   use 1
   ring
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean b/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean
index b0e2484..768f341 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean
@@ -37,6 +37,6 @@ Statement
   assumption
 
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean b/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean
index 8fe48f8..20ff5b7 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean
@@ -36,6 +36,6 @@ Statement
   ring
 
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean b/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean
index e3449fd..0887e21 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean
@@ -34,6 +34,6 @@ Statement
   ring
 
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean b/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean
index 110e17b..e98dd28 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean
@@ -28,6 +28,6 @@ Statement
     { x ∈ (S : Set ℤ) | 0 ≤ x} ⊆ S := by
   library_search
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean b/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean
index 65e8e32..2824f96 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean
@@ -23,6 +23,6 @@ Statement
   use 1
   ring
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean b/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean
index a081429..dfd5380 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean
@@ -22,6 +22,6 @@ open Set
 Statement
 "" : True := sorry
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean b/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean
index e4c74d3..7c384ad 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean
@@ -23,6 +23,6 @@ Statement
   use 1
   ring
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/T01_Set.lean b/server/testgame/TestGame/Levels/SetTheory/T01_Set.lean
index a63620d..9b6e875 100644
--- a/server/testgame/TestGame/Levels/SetTheory/T01_Set.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/T01_Set.lean
@@ -54,8 +54,7 @@ Statement
   rw [←Set.union_diff_distrib]
   rw [Set.univ_union]
 
-Tactics rw
-
+NewTactics rw
 
 example : 4 ∈ (univ : Set ℕ) := by
   trivial
diff --git a/server/testgame/TestGame/Levels/StatementTest.lean b/server/testgame/TestGame/Levels/StatementTest.lean
index 3ec654a..a9d47e1 100644
--- a/server/testgame/TestGame/Levels/StatementTest.lean
+++ b/server/testgame/TestGame/Levels/StatementTest.lean
@@ -35,4 +35,4 @@ lemma asdf (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c
 
 Conclusion ""
 
-Tactics assumption
+NewTactics assumption
diff --git a/server/testgame/TestGame/TacticDocs.lean b/server/testgame/TestGame/TacticDocs.lean
index fd33f0d..488aa67 100644
--- a/server/testgame/TestGame/TacticDocs.lean
+++ b/server/testgame/TestGame/TacticDocs.lean
@@ -258,5 +258,3 @@ Prove:
 
 TacticDoc intro
 "Useful to introduce stuff"
-
-TacticSet basics := rfl induction_on intro rewrite