diff options
Diffstat (limited to 'index.html')
| -rw-r--r-- | index.html | 11 |
1 files changed, 8 insertions, 3 deletions
@@ -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) { |