fix remeasure font. #24

leanprover-community · May 14, 2024 · f3c128d · f3c128d
1 parent f7ee513
commit f3c128d
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/client/src/Editor.tsx b/client/src/Editor.tsx
@@ -33,6 +33,13 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme:
   const [dragging, setDragging] = useState<boolean | null>(false)
   const [restartMessage, setRestartMessage] = useState<boolean | null>(false)
 
+  useEffect(() => {
+    console.log('Font is ready, rescaling editor.')
+    document.fonts.ready.then(function () {
+      monaco.editor.remeasureFonts()
+    })
+  }, [editor])
+
   useEffect(() => {
     if (['lightPlus', 'custom'].includes(theme)) {
       monaco.editor.setTheme(theme)