diff --git a/edit/codemirror-editing-hooks.js b/edit/codemirror-editing-hooks.js index 358aca88..e5914dc2 100644 --- a/edit/codemirror-editing-hooks.js +++ b/edit/codemirror-editing-hooks.js @@ -537,7 +537,7 @@ onDOMscriptReady('/codemirror.js').then(() => { 'xq-dark', 'xq-light', 'yeti', - 'zenburn' + 'zenburn', /* populate-theme-end */ ]; localStorage.codeMirrorThemes = themes.join(' '); diff --git a/tools/update-codemirror-themes.js b/tools/update-codemirror-themes.js index c5debd48..b6a887d0 100644 --- a/tools/update-codemirror-themes.js +++ b/tools/update-codemirror-themes.js @@ -15,11 +15,13 @@ async function getThemes() { } function replaceThemes(content, themes) { - const list = JSON.stringify(themes, null, 8).replace(/"/g, '\''); + const lineFeed = content.includes('\r\n') ? '\r\n' : '\n'; return content.replace( - /\/\*\s*populate-theme-start\s*\*\/[\s\S]+\/\*\s*populate-theme-end\s*\*\//, - // strip off square brackets & first 8 spaces - `/* populate-theme-start */\n${list.substring(2, list.length - 2)}\n /* populate-theme-end */` + /(\x20+)(\/\*\s*populate-theme-start\s*\*\/)[\s\S]+?(\/\*\s*populate-theme-end\s*\*\/)/, + (_, indent, intro, outro) => + indent + intro + lineFeed + + themes.map(_ => `${indent}'${_}',`).join(lineFeed) + lineFeed + + indent + outro ); }