From 3dc8d37790f7d8cdebee60abfb8b9d8e43b5d9f2 Mon Sep 17 00:00:00 2001 From: Glenn Rice Date: Tue, 8 Oct 2024 15:41:29 -0500 Subject: [PATCH] Fix language selection on page refresh on the test page. --- public/editor.js | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/public/editor.js b/public/editor.js index 157ec9b..9ef062d 100644 --- a/public/editor.js +++ b/public/editor.js @@ -4,7 +4,11 @@ const codeMirrorElt = document.querySelector('.pg-codemirror-editor'); if (codeMirrorElt instanceof HTMLElement) { const sourceInput = document.getElementsByName('editor-source')[0]; - const pgEditor = new PGCodeMirrorEditor.View(codeMirrorElt, { source: sourceInput.value }); + const languageSelector = document.getElementById('select-language'); + const pgEditor = new PGCodeMirrorEditor.View(codeMirrorElt, { + source: sourceInput.value, + language: languageSelector?.value ?? 'pg' + }); document.getElementById('load-file')?.addEventListener('click', () => { const file = document.getElementsByName('problem-file')[0]?.files?.[0]; @@ -18,7 +22,6 @@ if (codeMirrorElt instanceof HTMLElement) { } }); - const languageSelector = document.getElementById('select-language'); languageSelector?.addEventListener('change', () => { pgEditor.setLanguage(languageSelector.value); });