From 5a839505144befc9881916b0b4f653bc2a819679 Mon Sep 17 00:00:00 2001 From: yhirose Date: Fri, 10 Jun 2022 17:34:19 -0400 Subject: [PATCH] Fix #212 --- docs/index.js | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/docs/index.js b/docs/index.js index d85b46c..63f84ab 100644 --- a/docs/index.js +++ b/docs/index.js @@ -152,6 +152,18 @@ $('#auto-refresh').on('change', () => { }); $('#parse').on('click', parse); +// Resize editors to fit their parents +function resizeEditorsToParent() { + code.resize(); + code.renderer.updateFull(); + codeAst.resize(); + codeAst.renderer.updateFull(); + codeAstOptimized.resize(); + codeAstOptimized.renderer.updateFull(); + codeProfile.resize(); + codeProfile.renderer.updateFull(); +} + // Show windows function setupToolWindow(lsKeyName, buttonSel, codeSel) { let show = localStorage.getItem(lsKeyName) === 'true'; @@ -162,6 +174,7 @@ function setupToolWindow(lsKeyName, buttonSel, codeSel) { show = !show; localStorage.setItem(lsKeyName, show); $(codeSel).css({ 'display': show ? 'block' : 'none' }); + resizeEditorsToParent(); }); } setupToolWindow('show-ast', '#show-ast', '#code-ast');