From e77db1f4c5029f23528c76136d0b6ec6dc18a5ee Mon Sep 17 00:00:00 2001 From: rm-dr <96270320+rm-dr@users.noreply.github.com> Date: Sat, 1 Nov 2025 11:18:34 -0700 Subject: [PATCH] Font size --- webui/src/components/Editor.tsx | 14 ++++++- webui/src/components/Playground.tsx | 23 ++++++++++++ webui/src/components/Terminal.tsx | 17 +++++++-- webui/src/components/ui/Slider.tsx | 49 +++++++++++++++++++++++++ webui/src/styles/Slider.module.css | 57 +++++++++++++++++++++++++++++ 5 files changed, 155 insertions(+), 5 deletions(-) create mode 100644 webui/src/components/ui/Slider.tsx create mode 100644 webui/src/styles/Slider.module.css diff --git a/webui/src/components/Editor.tsx b/webui/src/components/Editor.tsx index 1399b96..2566079 100644 --- a/webui/src/components/Editor.tsx +++ b/webui/src/components/Editor.tsx @@ -47,10 +47,11 @@ interface EditorProps { initialValue?: string; onChange?: (editor: any, changes: any) => void; onReady?: (editor: any) => void; + fontSize?: number; } export const Editor = forwardRef(function Editor( - { initialValue = "", onChange, onReady }, + { initialValue = "", onChange, onReady, fontSize = 14 }, ref ) { const textareaRef = useRef(null); @@ -113,6 +114,17 @@ export const Editor = forwardRef(function Editor( }; }, []); // DO NOT FILL ARRAY + // Update font size when it changes + useEffect(() => { + if (editorRef.current) { + const wrapper = editorRef.current.getWrapperElement(); + if (wrapper) { + wrapper.style.fontSize = `${fontSize}px`; + editorRef.current.refresh(); + } + } + }, [fontSize]); + return (