From efb879c50ce861785fe1c5ea9ce3446a3dd2b63b Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Mon, 24 Jul 2023 13:25:50 +0200 Subject: [PATCH] trim later --- client/src/components/infoview/command_line.tsx | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/client/src/components/infoview/command_line.tsx b/client/src/components/infoview/command_line.tsx index 84a85da..c93a1ec 100644 --- a/client/src/components/infoview/command_line.tsx +++ b/client/src/components/infoview/command_line.tsx @@ -183,7 +183,7 @@ export function CommandLine({proofPanelRef}: {proofPanelRef: React.MutableRefObj proofPanelRef.current?.lastElementChild?.scrollIntoView() }) }) - }, [commandLineInput, editor, rpcSess, uri, model, proofPanelRef]) + }, [editor, rpcSess, uri, model, proofPanelRef]) // Run the command const runCommand = React.useCallback(() => { @@ -200,7 +200,7 @@ export function CommandLine({proofPanelRef}: {proofPanelRef: React.MutableRefObj pos, editor.getModel().getFullModelRange().getEndPosition() ), - text: commandLineInput + "\n", + text: commandLineInput.trim() + "\n", forceMoveMarkers: false }]) } @@ -277,7 +277,7 @@ export function CommandLine({proofPanelRef}: {proofPanelRef: React.MutableRefObj // Ensure that our one-line editor can only have a single line const l = oneLineEditor.getModel().onDidChangeContent((e) => { const value = oneLineEditor.getValue() - setCommandLineInput(value.trim()) + setCommandLineInput(value) const newValue = value.replace(/[\n\r]/g, '') if (value != newValue) { oneLineEditor.setValue(newValue)