changes

1 files changed, 99 insertions, 20 deletions

diff --git a/index.html b/index.html
index aca73cb..73a47ab 100644
--- a/index.html
+++ b/index.html
@@ -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