From f23556739f070a1aa5578e1464cc26f8868a3d78 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Tue, 22 Feb 2022 12:40:14 +0800 Subject: [PATCH] refactor: clean up javascript code --- DocGen4/Output.lean | 19 ++- DocGen4/Output/Base.lean | 2 + DocGen4/Output/Find.lean | 2 +- DocGen4/Output/Template.lean | 4 +- static/declaration-data.js | 127 +++++++++++++++++++ static/find/find.js | 30 +++-- static/how-about.js | 35 +++++ static/mathjax-config.js | 45 ++++--- static/nav.js | 239 ++++------------------------------- static/search.js | 157 ++++++++++++++--------- static/site-root.js | 3 + static/tactic.js | 61 +++++++++ 12 files changed, 414 insertions(+), 310 deletions(-) create mode 100644 static/declaration-data.js create mode 100644 static/how-about.js create mode 100644 static/tactic.js diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index dcf51d0..82d3a26 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -82,18 +82,23 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do let json := Json.arr declList - FS.writeFile (basePath / "searchable_data.bmp") json.compress FS.writeFile (basePath / "index.html") indexHtml.toString - FS.writeFile (basePath / "style.css") styleCss FS.writeFile (basePath / "404.html") notFoundHtml.toString + FS.writeFile (basePath / "find" / "index.html") findHtml.toString + + FS.writeFile (basePath / "style.css") styleCss + + let declarationDataPath := basePath / "declaration-data.bmp" + FS.writeFile declarationDataPath json.compress + FS.writeFile (basePath / "declaration-data.timestamp") <| toString (←declarationDataPath.metadata).modified.sec + + FS.writeFile (basePath / "site-root.js") (siteRootJs.replace "{siteRoot}" config.root) + FS.writeFile (basePath / "declaration-data.js") declarationDataCenterJs FS.writeFile (basePath / "nav.js") navJs + FS.writeFile (basePath / "find" / "find.js") findJs + FS.writeFile (basePath / "how-about.js") howAboutJs FS.writeFile (basePath / "search.js") searchJs FS.writeFile (basePath / "mathjax-config.js") mathjaxConfigJs - FS.writeFile (basePath / "site-root.js") (siteRootJs.replace "{siteRoot}" config.root) - - FS.writeFile (basePath / "find" / "index.html") findHtml.toString - FS.writeFile (basePath / "find" / "find.js") findJs - for (module, content) in result.moduleInfo.toArray do let moduleHtml := ReaderT.run (moduleToHtml content) config diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 0188511..20443f8 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -48,7 +48,9 @@ def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath := section Static def styleCss : String := include_str "./static/style.css" def siteRootJs : String := include_str "./static/site-root.js" + def declarationDataCenterJs : String := include_str "./static/declaration-data.js" def navJs : String := include_str "./static/nav.js" + def howAboutJs : String := include_str "./static/how-about.js" def searchJs : String := include_str "./static/search.js" def findJs : String := include_str "./static/find/find.js" def mathjaxConfigJs : String := include_str "./static/mathjax-config.js" diff --git a/DocGen4/Output/Find.lean b/DocGen4/Output/Find.lean index 60e56ac..95bbd8e 100644 --- a/DocGen4/Output/Find.lean +++ b/DocGen4/Output/Find.lean @@ -10,7 +10,7 @@ def find : HtmlM Html := do pure - + diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index d4f358f..05390fe 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -24,13 +24,15 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do - + + + diff --git a/static/declaration-data.js b/static/declaration-data.js new file mode 100644 index 0000000..ec72aa8 --- /dev/null +++ b/static/declaration-data.js @@ -0,0 +1,127 @@ +/** + * This module is a wrapper that facilitates manipulating the declaration data. + * + * Please see {@link DeclarationDataCenter} for more information. + */ + +import { SITE_ROOT } from "./site-root.js"; + +/** + * The DeclarationDataCenter is used for declaration searching. + * + * For usage, see the {@link init} and {@link search} methods. + */ +export class DeclarationDataCenter { + /** + * The declaration data. Users should not interact directly with this field. + * + * *NOTE:* This is not made private to support legacy browsers. + */ + declarationData = []; + + /** + * Used to implement the singleton, in case we need to fetch data mutiple times in the same page. + */ + static singleton = null; + + /** + * Construct a DeclarationDataCenter with given data. + * + * Please use {@link DeclarationDataCenter.init} instead, which automates the data fetching process. + * @param {*} declarationData + */ + constructor(declarationData) { + this.declarationData = declarationData; + } + + /** + * The actual constructor of DeclarationDataCenter + * @returns {Promise} + */ + static async init() { + if (!DeclarationDataCenter.singleton) { + const dataUrl = new URL( + `${SITE_ROOT}declaration-data.bmp`, + window.location + ); + const response = await fetch(dataUrl); + const json = await response.json(); + const data = json.map(({ name, description, link, source }) => [ + name, + name.toLowerCase(), + description.toLowerCase(), + link, + source, + ]); + DeclarationDataCenter.singleton = new DeclarationDataCenter(data); + } + return DeclarationDataCenter.singleton; + } + + /** + * Search for a declaration. + * @returns {Array} + */ + search(pattern, strict = false) { + if (!pattern) { + return []; + } + // TODO: implement strict + return getMatches(this.declarationData, pattern); + } +} + +function isSeparater(char) { + return char === "." || char === "_"; +} + +function matchCaseSensitive( + declName, + lowerDeclName, + pattern +) { + let i = 0, + j = 0, + err = 0, + lastMatch = 0; + while (i < declName.length && j < pattern.length) { + if ( + pattern[j] === declName[i] || + pattern[j] === lowerDeclName[i] + ) { + err += (isSeparater(pattern[j]) ? 0.125 : 1) * (i - lastMatch); + if (pattern[j] !== declName[i]) err += 0.5; + lastMatch = i + 1; + j++; + } else if (isSeparater(declName[i])) { + err += 0.125 * (i + 1 - lastMatch); + lastMatch = i + 1; + } + i++; + } + err += 0.125 * (declName.length - lastMatch); + if (j === pattern.length) { + return err; + } +} + +function getMatches(declarations, pattern, maxResults = 30) { + const lowerPats = pattern.toLowerCase().split(/\s/g); + const patNoSpaces = pattern.replace(/\s/g, ""); + const results = []; + for (const [decl, lowerDecl, lowerDoc, link, source] of declarations) { + let err = matchCaseSensitive(decl, lowerDecl, patNoSpaces); + // match all words as substrings of docstring + if ( + !(err < 3) && + pattern.length > 3 && + lowerPats.every((l) => lowerDoc.indexOf(l) != -1) + ) { + err = 3; + } + if (err !== undefined) { + results.push({ decl, err, link, source }); + } + } + return results.sort(({ err: a }, { err: b }) => a - b).slice(0, maxResults); +} diff --git a/static/find/find.js b/static/find/find.js index 480f725..7fcb9ec 100644 --- a/static/find/find.js +++ b/static/find/find.js @@ -1,22 +1,28 @@ -import { SITE_ROOT } from "../site-root.js"; -import { declSearch } from "../search.js"; +/** + * This module is used for the `/find` endpoint. + */ -async function findRedirect(query, isSource) { - return declSearch(query).then((results) => { - window.location.replace(isSource? results[0].source : results[0].link); - }).catch(() => { +import { SITE_ROOT } from "../site-root.js"; +import { DeclarationDataCenter } from "../declaration-data.js"; + +async function findRedirect(pattern, isSource) { + const dataCenter = await DeclarationDataCenter.init(); + try { + let results = dataCenter.search(pattern); + window.location.replace(isSource ? results[0].source : results[0].link); + } catch { window.location.replace(`${SITE_ROOT}404.html`); - }); + } } -let splits = window.location.href.split("#"); +let hash = window.location.hash.split("#"); -if (splits.length < 2) { +if (hash.length == 0) { window.location.replace(`${SITE_ROOT}/404.html`); } -if (splits[1].endsWith("/src")) { - findRedirect(splits[1].replace("/src", ""), true); +if (hash[1].endsWith("/src")) { + findRedirect(hash.replace("/src", ""), true); } else { - findRedirect(splits[1], false); + findRedirect(hash, false); } diff --git a/static/how-about.js b/static/how-about.js new file mode 100644 index 0000000..421f6e4 --- /dev/null +++ b/static/how-about.js @@ -0,0 +1,35 @@ +/** + * This module implements the `howabout` functionality in the 404 page. + */ + +import { DeclarationDataCenter } from "./declaration-data.js"; + +const HOW_ABOUT = document.querySelector("#howabout"); + +if (HOW_ABOUT) { + HOW_ABOUT.innerText = "Please wait a second. I'll try to help you."; + + HOW_ABOUT.parentNode + .insertBefore(document.createElement("pre"), HOW_ABOUT) + .appendChild(document.createElement("code")).innerText = + window.location.href.replace(/[/]/g, "/\u200b"); + + // TODO: add how about functionality for similar page as well. + const pattern = window.location.hash.replace("#", ""); + + DeclarationDataCenter.init().then((dataCenter) => { + let results = dataCenter.search(pattern); + if (results.length > 0) { + HOW_ABOUT.innerText = "How about one of these instead:"; + const ul = HOW_ABOUT.appendChild(document.createElement("ul")); + for (const { decl, link } of results) { + const li = ul.appendChild(document.createElement("li")); + const a = li.appendChild(document.createElement("a")); + a.href = link; + a.appendChild(document.createElement("code")).innerText = decl; + } + } else { + HOW_ABOUT.innerText = "Sorry, I cannot find any similar declarations. Check the link or use the module navigation to find what you want :P"; + } + }); +} diff --git a/static/mathjax-config.js b/static/mathjax-config.js index 9e470bc..076dbf6 100644 --- a/static/mathjax-config.js +++ b/static/mathjax-config.js @@ -1,26 +1,41 @@ /* - * This file is for configing MathJax behavior. - * Seehttps://docs.mathjax.org/en/latest/web/configuration.html - */ - -/** + * This file is for configing MathJax behavior. + * See https://docs.mathjax.org/en/latest/web/configuration.html + * * This configuration is copied from old doc-gen3 * https://github.com/leanprover-community/doc-gen */ MathJax = { tex: { - inlineMath: [['$', '$']], - displayMath: [['$$', '$$']] + inlineMath: [["$", "$"]], + displayMath: [["$$", "$$"]], }, options: { skipHtmlTags: [ - 'script', 'noscript', 'style', 'textarea', 'pre', - 'code', 'annotation', 'annotation-xml', - 'decl', 'decl_meta', 'attributes', 'decl_args', 'decl_header', 'decl_name', - 'decl_type', 'equation', 'equations', 'structure_field', 'structure_fields', - 'constructor', 'constructors', 'instances' + "script", + "noscript", + "style", + "textarea", + "pre", + "code", + "annotation", + "annotation-xml", + "decl", + "decl_meta", + "attributes", + "decl_args", + "decl_header", + "decl_name", + "decl_type", + "equation", + "equations", + "structure_field", + "structure_fields", + "constructor", + "constructors", + "instances", ], - ignoreHtmlClass: 'tex2jax_ignore', - processHtmlClass: 'tex2jax_process', + ignoreHtmlClass: "tex2jax_ignore", + processHtmlClass: "tex2jax_process", }, -}; \ No newline at end of file +}; diff --git a/static/nav.js b/static/nav.js index 3889da3..ff8404e 100644 --- a/static/nav.js +++ b/static/nav.js @@ -1,232 +1,43 @@ -import { declSearch } from "./search.js"; - -// Persistent expansion cookie for the file tree -// --------------------------------------------- +/** + * This module is used to implement persistent navbar expansion. + */ +// The variable to store the expansion information. let expanded = {}; -for (const e of (sessionStorage.getItem('expanded') || '').split(',')) { - if (e !== '') { + +// Load expansion information from sessionStorage. +for (const e of (sessionStorage.getItem("expanded") || "").split(",")) { + if (e !== "") { expanded[e] = true; } } +/** + * Save expansion information to sessionStorage. + */ function saveExpanded() { - sessionStorage.setItem("expanded", - Object.getOwnPropertyNames(expanded).filter((e) => expanded[e]).join(",")); + sessionStorage.setItem( + "expanded", + Object.getOwnPropertyNames(expanded) + .filter((e) => expanded[e]) + .join(",") + ); } -for (const elem of document.getElementsByClassName('nav_sect')) { - const id = elem.getAttribute('data-path'); +// save expansion information when user change the expansion. +for (const elem of document.getElementsByClassName("nav_sect")) { + const id = elem.getAttribute("data-path"); if (!id) continue; if (expanded[id]) { elem.open = true; } - elem.addEventListener('toggle', () => { + elem.addEventListener("toggle", () => { expanded[id] = elem.open; saveExpanded(); }); } -for (const currentFileLink of document.getElementsByClassName('visible')) { - currentFileLink.scrollIntoView({block: 'center'}); -} - - - - - - -// Tactic list tag filter -// ---------------------- - -function filterSelectionClass(tagNames, classname) { - if (tagNames.length == 0) { - for (const elem of document.getElementsByClassName(classname)) { - elem.classList.remove("hide"); - } - } else { - // Add the "show" class (display:block) to the filtered elements, and remove the "show" class from the elements that are not selected - for (const elem of document.getElementsByClassName(classname)) { - elem.classList.add("hide"); - for (const tagName of tagNames) { - if (elem.classList.contains(tagName)) { - elem.classList.remove("hide"); - } - } - } - } - } - - function filterSelection(c) { - filterSelectionClass(c, "tactic"); - filterSelectionClass(c, "taclink"); - } - -var filterBoxes = document.getElementsByClassName("tagfilter"); - -function updateDisplay() { - filterSelection(getSelectValues()); -} - -function getSelectValues() { - var result = []; - - for (const opt of filterBoxes) { - - if (opt.checked) { - result.push(opt.value); - } - } - return result; - } - -function setSelectVal(val) { - for (const opt of filterBoxes) { - opt.checked = val; - } -} - -updateDisplay(); - -for (const opt of filterBoxes) { - opt.addEventListener('change', updateDisplay); -} - -const tse = document.getElementById("tagfilter-selectall") -if (tse != null) { - tse.addEventListener('change', function() { - setSelectVal(this.checked); - updateDisplay(); - }); -} - - - - - - -// Simple declaration search -// ------------------------- - -const srId = 'search_results'; -document.getElementById('search_form') - .appendChild(document.createElement('div')) - .id = srId; - -function handleSearchCursorUpDown(down) { - const sel = document.querySelector(`#${srId} .selected`); - const sr = document.getElementById(srId); - if (sel) { - sel.classList.remove('selected'); - const toSelect = down ? - sel.nextSibling || sr.firstChild: - sel.previousSibling || sr.lastChild; - toSelect && toSelect.classList.add('selected'); - } else { - const toSelect = down ? sr.firstChild : sr.lastChild; - toSelect && toSelect.classList.add('selected'); - } -} - -function handleSearchEnter() { - const sel = document.querySelector(`#${srId} .selected`) - || document.getElementById(srId).firstChild; - sel.click(); -} - -const searchInput = document.querySelector('#search_form input[name=q]'); - -searchInput.addEventListener('keydown', (ev) => { - switch (ev.key) { - case 'Down': - case 'ArrowDown': - ev.preventDefault(); - handleSearchCursorUpDown(true); - break; - case 'Up': - case 'ArrowUp': - ev.preventDefault(); - handleSearchCursorUpDown(false); - break; - case 'Enter': - ev.preventDefault(); - handleSearchEnter(); - break; - } -}); - -searchInput.addEventListener('input', async (ev) => { - const text = ev.target.value; - - if (!text) { - const sr = document.getElementById(srId); - sr.removeAttribute('state'); - sr.replaceWith(sr.cloneNode(false)); - return; - } - - document.getElementById(srId).setAttribute('state', 'loading'); - - const result = await declSearch(text); - if (ev.target.value != text) return; - - const oldSR = document.getElementById('search_results'); - const sr = oldSR.cloneNode(false); - for (const {decl, link} of result) { - const d = sr.appendChild(document.createElement('a')); - d.innerText = decl; - d.title = decl; - d.href = link; - } - sr.setAttribute('state', 'done'); - oldSR.replaceWith(sr); -}); - - - - - - -// 404 page goodies -// ---------------- - -const howabout = document.getElementById('howabout'); -if (howabout) { - howabout.innerText = "Please wait a second. I'll try to help you."; - - howabout.parentNode - .insertBefore(document.createElement('pre'), howabout) - .appendChild(document.createElement('code')) - .innerText = window.location.href.replace(/[/]/g, '/\u200b'); - - const query = window.location.href.match(/[/]([^/]+)(?:\.html|[/])?$/)[1]; - declSearch(query).then((results) => { - howabout.innerText = 'How about one of these instead:'; - const ul = howabout.appendChild(document.createElement('ul')); - for (const {decl, link} of results) { - const li = ul.appendChild(document.createElement('li')); - const a = li.appendChild(document.createElement('a')); - a.href = link; - a.appendChild(document.createElement('code')).innerText = decl; - } - }); -} - - - - - - -// Rewrite GitHub links -// -------------------- - -for (const elem of document.getElementsByClassName('gh_link')) { - const a = elem.firstElementChild; - // commit is set in add_commit.js - for (const [prefix, replacement] of commit) { - if (a.href.startsWith(prefix)) { - a.href = a.href.replace(prefix, replacement); - break; - } - } -} +// Scroll to center. +for (const currentFileLink of document.getElementsByClassName("visible")) { + currentFileLink.scrollIntoView({ block: "center" }); +} \ No newline at end of file diff --git a/static/search.js b/static/search.js index 3449036..a6a72ea 100644 --- a/static/search.js +++ b/static/search.js @@ -1,67 +1,104 @@ -import { SITE_ROOT } from "./site-root.js"; +/** + * This module is used to handle user's interaction with the search form. + */ -function isSep(c) { - return c === '.' || c === '_'; -} +import { DeclarationDataCenter } from "./declaration-data.js"; -function matchCaseSensitive(declName, lowerDeclName, pat) { - let i = 0, j = 0, err = 0, lastMatch = 0 - while (i < declName.length && j < pat.length) { - if (pat[j] === declName[i] || pat[j] === lowerDeclName[i]) { - err += (isSep(pat[j]) ? 0.125 : 1) * (i - lastMatch); - if (pat[j] !== declName[i]) err += 0.5; - lastMatch = i + 1; - j++; - } else if (isSep(declName[i])) { - err += 0.125 * (i + 1 - lastMatch); - lastMatch = i + 1; - } - i++; - } - err += 0.125 * (declName.length - lastMatch); - if (j === pat.length) { - return err; - } -} -export function loadDecls(searchableDataCnt) { - return searchableDataCnt.map(({name, description, link, source}) => [name, name.toLowerCase(), description.toLowerCase(), link, source]); -} +const SEARCH_FORM = document.querySelector("#search_form"); +const SEARCH_INPUT = SEARCH_FORM.querySelector("input[name=q]"); -export function getMatches(decls, pat, maxResults = 30) { - const lowerPats = pat.toLowerCase().split(/\s/g); - const patNoSpaces = pat.replace(/\s/g, ''); - const results = []; - for (const [decl, lowerDecl, lowerDoc, link, source] of decls) { - let err = matchCaseSensitive(decl, lowerDecl, patNoSpaces); +// Create an `div#search_results` to hold all search results. +let sr = document.createElement("div"); +sr.id = "search_results"; +SEARCH_FORM.appendChild(sr); - // match all words as substrings of docstring - if (!(err < 3) && pat.length > 3 && lowerPats.every(l => lowerDoc.indexOf(l) != -1)) { - err = 3; - } - - if (err !== undefined) { - results.push({decl, err, link, source}); - } - } - return results.sort(({err: a}, {err: b}) => a - b).slice(0, maxResults); -} - -const declURL = new URL(`${SITE_ROOT}searchable_data.bmp`, window.location); - -export const getDecls = (() => { - let decls; - return () => { - if (!decls) decls = new Promise((resolve, reject) => { - const req = new XMLHttpRequest(); - req.responseType = 'json'; - req.addEventListener('load', () => resolve(loadDecls(req.response))); - req.addEventListener('error', () => reject()); - req.open('GET', declURL); - req.send(); - }) - return decls; +/** + * Attach `selected` class to the the selected search result. + */ +function handleSearchCursorUpDown(down) { + const sel = sr.querySelector(`.selected`); + if (sel) { + sel.classList.remove("selected"); + const toSelect = down + ? sel.nextSibling || sr.firstChild + : sel.previousSibling || sr.lastChild; + toSelect && toSelect.classList.add("selected"); + } else { + const toSelect = down ? sr.firstChild : sr.lastChild; + toSelect && toSelect.classList.add("selected"); } -})() +} -export const declSearch = async (q) => getMatches(await getDecls(), q); \ No newline at end of file +/** + * Perform search (when enter is pressed). + */ +function handleSearchEnter() { + const sel = + sr.querySelector(`.selected`) || + sr.firstChild; + sel.click(); +} + +/** + * Allow user to navigate search results with up/down arrow keys, and choose with enter. + */ +SEARCH_INPUT.addEventListener("keydown", (ev) => { + switch (ev.key) { + case "Down": + case "ArrowDown": + ev.preventDefault(); + handleSearchCursorUpDown(true); + break; + case "Up": + case "ArrowUp": + ev.preventDefault(); + handleSearchCursorUpDown(false); + break; + case "Enter": + ev.preventDefault(); + handleSearchEnter(); + break; + } +}); + +/** + * Remove all children of a DOM node. + */ +function removeAllChildren(node) { + while (node.firstChild) { + node.removeChild(node.lastChild); + } +} + +/** + * Search autocompletion. + */ +SEARCH_INPUT.addEventListener("input", async (ev) => { + const text = ev.target.value; + + // If no input clear all. + if (!text) { + sr.removeAttribute("state"); + removeAllChildren(sr); + return; + } + + // searching + sr.setAttribute("state", "loading"); + const dataCenter = await DeclarationDataCenter.init(); + const result = dataCenter.search(text); + + // in case user has updated the input. + if (ev.target.value != text) return; + + // update search results + removeAllChildren(sr); + for (const { decl, link } of result) { + const d = sr.appendChild(document.createElement("a")); + d.innerText = decl; + d.title = decl; + d.href = link; + } + sr.setAttribute("state", "done"); +}); diff --git a/static/site-root.js b/static/site-root.js index 0663d6b..3dd39a3 100644 --- a/static/site-root.js +++ b/static/site-root.js @@ -1 +1,4 @@ +/** + * Get the site root, {siteRoot} is to be replaced by doc-gen4. + */ export const SITE_ROOT = "{siteRoot}"; \ No newline at end of file diff --git a/static/tactic.js b/static/tactic.js new file mode 100644 index 0000000..e40c4ec --- /dev/null +++ b/static/tactic.js @@ -0,0 +1,61 @@ +// TODO: The tactic part seem to be unimplemented now. + +function filterSelectionClass(tagNames, classname) { + if (tagNames.length == 0) { + for (const elem of document.getElementsByClassName(classname)) { + elem.classList.remove("hide"); + } + } else { + // Add the "show" class (display:block) to the filtered elements, and remove the "show" class from the elements that are not selected + for (const elem of document.getElementsByClassName(classname)) { + elem.classList.add("hide"); + for (const tagName of tagNames) { + if (elem.classList.contains(tagName)) { + elem.classList.remove("hide"); + } + } + } + } +} + +function filterSelection(c) { + filterSelectionClass(c, "tactic"); + filterSelectionClass(c, "taclink"); +} + +var filterBoxes = document.getElementsByClassName("tagfilter"); + +function updateDisplay() { + filterSelection(getSelectValues()); +} + +function getSelectValues() { + var result = []; + + for (const opt of filterBoxes) { + if (opt.checked) { + result.push(opt.value); + } + } + return result; +} + +function setSelectVal(val) { + for (const opt of filterBoxes) { + opt.checked = val; + } +} + +updateDisplay(); + +for (const opt of filterBoxes) { + opt.addEventListener("change", updateDisplay); +} + +const tse = document.getElementById("tagfilter-selectall"); +if (tse != null) { + tse.addEventListener("change", function () { + setSelectVal(this.checked); + updateDisplay(); + }); +}