some&all + symbol shortcuts

1 files changed, 17 insertions, 11 deletions

diff --git a/index.html b/index.html
index 2e5e31b..18442fb 100644
--- a/index.html
+++ b/index.html
@@ -151,6 +151,7 @@
 
                 const text = await response.text()
                 const symbols = {}
+                const symbolAliases = {}
 
                 for (const line of text.split('\n')) {
                     const trimmed = line.trim()
@@ -161,13 +162,15 @@
                         const symbol = parts[0]
                         const name = parts.slice(1).join(' ')
                         symbols[name] = symbol
+                        if (!symbolAliases[symbol]) symbolAliases[symbol] = []
+                        symbolAliases[symbol].push(name)
                     }
                 }
 
-                return symbols
+                return { symbols, symbolAliases }
             } catch (err) {
                 console.warn('failed to load symbols.txt:', err)
-                return {}
+                return { symbols: {}, symbolAliases: {} }
             }
         }
 
@@ -285,7 +288,7 @@
 
             render() {
                 let html = ''
-                
+
                 let tocItems = []
                 for (const token of this.tokens) {
                     if (token.type === 'definition') {
@@ -298,9 +301,9 @@
                         } else {
                             name = line
                         }
-                        
+
                         const actualName = token.description.split('\n')[0].replace(/:/g, '')
-                        
+
                         if (this.reverseSymbols[name]) {
                             tocItems.push({
                                 symbol: name,
@@ -420,7 +423,7 @@
             }
         }
 
-        function validateSymbols(text, symbols) {
+        function validateSymbols(text, symbols, symbolAliases) {
             const definedSymbols = new Set()
             const missing = new Map()
             const lines = text.replace(/\r\n/g, '\n').replace(/\r/g, '\n').split('\n')
@@ -447,11 +450,14 @@
                 while ((match = usagePattern.exec(line)) !== null) {
                     const name = match[1]
                     if (definedSymbols.has(name)) continue
-                    if (symbols[name] && definedSymbols.has(symbols[name])) continue
 
-                    if (!missing.has(name)) {
-                        missing.set(name, [])
+                    const sym = symbols[name]
+                    if (sym) {
+                        const aliases = symbolAliases[sym] || []
+                        if (aliases.some(alias => definedSymbols.has(alias))) continue
                     }
+
+                    if (!missing.has(name)) missing.set(name, [])
                     missing.get(name).push(lineNumber)
                 }
             })
@@ -472,12 +478,12 @@
 
         async function loadMarkdown() {
             try {
-                const symbols = await loadSymbols()
+                const { symbols, symbolAliases } = await loadSymbols()
                 let response = await fetch('tempo.md')
                 if (response.status !== 200) response = await fetch('tempo.md.html')
 
                 let text = await response.text()
-                validateSymbols(text, symbols)
+                validateSymbols(text, symbols, symbolAliases)
                 text = text.replace(/((^|\n)<!> *)/g, (e) => e.replace(/<!> */g, ''))
                 text = applySymbols(text, symbols)