diff options
Diffstat (limited to 'index.html')
| -rw-r--r-- | index.html | 119 |
1 files changed, 99 insertions, 20 deletions
@@ -12,6 +12,7 @@ <meta charset='UTF-8'> <title>tempo</title> <link rel="prefetch" href="/tempo.md" as="fetch"> + <link rel="prefetch" href="/symbols.txt" as="fetch"> <link rel="stylesheet" href="styles3.css"> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link rel="shortcut icon" href="bell.png"> @@ -28,7 +29,7 @@ } </script> <div id="themeButton" style="display: none"> - <button id="themeToggle">🌙</button> + <button id="themeToggle">🌙</button> </div> <script> @@ -52,15 +53,16 @@ </script> <noscript> - hello.<br> - your browser does not support javascript, it seems.<br> - this means i cannot render the markdown as pretty-printed html for you.<br> - instead, you can read the markdown raw at <a href="tempo.md">this page</a>.<br> - have a great day! :) + hello.<br> + your browser does not support javascript, it seems.<br> + this means i cannot render the markdown as pretty-printed html for you.<br> + instead, you can read the markdown raw at <a href="tempo.md">this page</a>.<br> + have a great day! :) - <br><br><br><br><br> + <br><br><br><br><br> </noscript> + <div id='warnings'></div> <div id='content'></div> <div> tempo is licensed under creative-commons. @@ -100,7 +102,7 @@ chunk = chunk.replace(/\*\*(.*?)\*\*/g, '<b>$1</b>') chunk = chunk.replace(/__(.*?)__/g, '<u>$1</u>') chunk = chunk.replace(/\*(.*?)\*/g, '<i>$1</i>') - chunk = chunk.replace(/\[\[(.*?)\]\]/g, '<span style="user-select:none">🔎 </span><b>“$1”</b>') + chunk = chunk.replace(/\[\[(.*?)\]\]/g, '<span style="user-select:none">🔎 </span><b>"$1"</b>') html += chunk } else { html += `<code>${escapeHTML(parts[i])}</code>` @@ -109,6 +111,46 @@ return html } + async function loadSymbols() { + try { + let response = await fetch('symbols.txt') + if (response.status !== 200) response = await fetch('symbols.txt.html') + if (response.status !== 200) { + console.log('symbols.txt not found, skipping symbol replacement') + return {} + } + + const text = await response.text() + const symbols = {} + + for (const line of text.split('\n')) { + const trimmed = line.trim() + if (!trimmed) continue + + const parts = trimmed.split(/\s+/) + if (parts.length >= 2) { + const symbol = parts[0] + const name = parts.slice(1).join(' ') + symbols[name] = symbol + } + } + + return symbols + } catch (err) { + console.warn('failed to load symbols.txt:', err) + return {} + } + } + + function applySymbols(text, symbols) { + let result = text + for (const [name, symbol] of Object.entries(symbols)) { + const pattern = new RegExp(`\\\\${name.replace(/[.*+?^${}()|[\]\\]/g, '\\$&')}\\\\`, 'g') + result = result.replace(pattern, symbol) + } + return result + } + class TempoParser { constructor(rawText) { this.lines = rawText.replace(/\r\n/g, '\n').replace(/\r/g, '\n').split('\n') @@ -266,25 +308,62 @@ const deftext = escapeHTML(code) return `<block> - <header> - <div class='header-left'> - <span>def</span> - <span class='def-name'>${escapeHTML(name)}</span> - ${deftext.length === 0 ? `` : `<code>${escapeHTML(code)}</code>`} - </div> - ${eng ? `<span class='eng-text'>[${escapeHTML(eng)}]</span>` : ''} - </header> - <desc>${descHtml}</desc> - </block>` + <header> + <div class='header-left'> + <span>def</span> + <span class='def-name'>${escapeHTML(name)}</span> + ${deftext.length === 0 ? `` : `<code>${escapeHTML(code)}</code>`} + </div> + ${eng ? `<span class='eng-text'>[${escapeHTML(eng)}]</span>` : ''} + </header> + <desc>${descHtml}</desc> + </block>` + } + } + + function validateSymbols(text, symbols) { + const usagePattern = /\\([^\\\s]+)\\/g + const usedSymbols = new Set() + let match + + while ((match = usagePattern.exec(text)) !== null) { + usedSymbols.add(match[1]) + } + + const definedSymbols = new Set() + const defPattern = /^def\s+(\S+)/gm + + while ((match = defPattern.exec(text)) !== null) { + console.log('defined:', match[1]) + definedSymbols.add(match[1].replace(/^\\/g, '').replace(/\\$/g, '')) + } + + const missing = [] + for (const name of usedSymbols) { + if (definedSymbols.has(name)) continue + + const symbol = symbols[name] + if (symbol && definedSymbols.has(symbol)) continue + + missing.push(name) + } + + if (missing.length > 0) { + const msg = `undefined symbols detected:\n${missing.map(s => ` • (${symbols[s]}) ${s}`).join('\n')}` + warnings.innerHTML += msg.replace(/\n/g, '<br>') + console.warn('undefined symbols:', missing) } } async function loadMarkdown() { try { + const symbols = await loadSymbols() let response = await fetch('tempo.md') if (response.status !== 200) response = await fetch('tempo.md.html') - const text = await response.text() + let text = await response.text() + validateSymbols(text, symbols) + text = applySymbols(text, symbols) const parser = new TempoParser(text) parser.tokenize() @@ -356,4 +435,4 @@ </script> </body> -</html> +</html>
\ No newline at end of file |