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 d86c908..45ef83c 100644
--- a/client/src/components/infoview/CommandLine.tsx
+++ b/client/src/components/infoview/CommandLine.tsx
@@ -8,30 +8,108 @@ 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)
 
   const inputRef = useRef()
 
+  // 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: commandLineInput + "\n",
+      forceMoveMarkers: false
+    }]);
+    editor.setPosition(pos)
+    setProcessing(true)
+  }, [commandLineInput, editor])
+
   useEffect(() => {
-    const editor = monaco.editor.create(inputRef.current!, {
+    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)) {
+        setCommandLineInput("")
+        editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
+      }
+    }
+  }, []);
+
+  useEffect(() => {
+    const myEditor = monaco.editor.create(inputRef.current!, {
+      value: commandLineInput,
+      language: "lean4cmd",
       quickSuggestions: false,
       lightbulb: {
         enabled: true
@@ -46,30 +124,51 @@ export function CommandLine() {
       lineNumbers: 'off',
       glyphMargin: false,
       folding: false,
-      // Undocumented see https://github.com/Microsoft/vscode/issues/30795#issuecomment-410998882
       lineDecorationsWidth: 0,
       lineNumbersMinChars: 0,
       'semanticHighlighting.enabled': true,
       overviewRulerLanes: 0,
       hideCursorInOverviewRuler: true,
       scrollbar: {
-          vertical: 'hidden'
+        vertical: 'hidden',
+        horizontalScrollbarSize: 3
       },
       overviewRulerBorder: false,
       theme: 'vs-code-theme-converted',
       contextmenu: false
     })
 
-    const t = editor.getModel().onDidChangeContent((e) => {
-      const value = editor.getValue()
+    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) {
-        editor.setValue(newValue)
+        oneLineEditor.setValue(newValue)
       }
     })
+    return () => { l.dispose() }
+  }, [oneLineEditor, setCommandLineInput])
 
-    return () => {t.dispose(); editor.dispose()}
-  }, [])
+  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(() => {
@@ -78,7 +177,7 @@ export function CommandLine() {
       if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") {
         editor.executeEdits("command-line", [{
           range: monaco.Selection.fromPositions(endPos, endPos),
-          text: "\n",
+          text: commandLineInput + "\n",
           forceMoveMarkers: false
         }]);
       }
@@ -86,38 +185,27 @@ export function CommandLine() {
     }
   }, [commandLineMode])
 
-  // Run the command
   const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
     ev.preventDefault()
-    const pos = editor.getPosition()
-    editor.executeEdits("command-line", [{
-      range: monaco.Selection.fromPositions(
-        pos,
-        editor.getModel().getFullModelRange().getEndPosition()
-      ),
-      text: commandInput.current!.value + "\n",
-      forceMoveMarkers: false
-    }]);
-    editor.setPosition(pos)
-    setProcessing(true)
+    runCommand()
   }
 
-  // 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 = "";
-        editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
-      }
-    }
-  }, []);
-
   return <div className="command-line">
       <form onSubmit={handleSubmit}>
-        <div ref={inputRef} className="command-line-input" />
-        {/* <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/infoview.css b/client/src/components/infoview/infoview.css
index 174d4f1..e91bc49 100644
--- a/client/src/components/infoview/infoview.css
+++ b/client/src/components/infoview/infoview.css
@@ -52,8 +52,21 @@
   display: block;
 }
 
-.command-line .command-line-input{
+.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 */
 /***************************************/