duplicate symbol

1 files changed, 8 insertions, 3 deletions

diff --git a/index.html b/index.html
index b71536e..b227cc0 100644
--- a/index.html
+++ b/index.html
@@ -322,6 +322,11 @@
                 if (firstTick !== -1 && lastTick !== -1 && lastTick > firstTick) {
                     name = line.substring(0, firstTick).trim()
                     if (!this.defs.has(name)) this.defs.add(name)
+                    else if (name !== 'Ω' && name !== 'me') {
+                        console.log('[warn] duplicate symbol', name)
+                        warnings.innerHTML += `Duplicate symbol ${name}!<br>`
+                        warnings.style.display = 'block'
+                    }
                     code = line.substring(firstTick + 1, lastTick)
 
                     let remainder = line.substring(lastTick + 1).trim()
@@ -396,7 +401,7 @@
                 }
                 warnings.innerHTML += msg.replace(/\n/g, '<br>')
                 console.warn('undefined symbols:', missing)
-            } else {
+            } else if (warnings.innerHTML.length === 0) {
                 warnings.style.display = 'none'
             }
         }
@@ -416,8 +421,8 @@
                 parser.tokenize()
                 const html = parser.render().replace(/{{dict_size}}/g, `<b>${parser.defs.size - 1}</b>`)
 
-                // store first 4kb of website in local storage
-                document.getElementById('content').innerHTML = html
+                // store first 32kb of website in local storage
+                content.innerHTML = html
                 try {
                     localStorage.setItem('rendered', html.substring(0, 32768))
                 } catch (err) {