| 24 |
var lineEl = document.getElementById (idPrefix + 'line-' + line); |
var lineEl = document.getElementById (idPrefix + 'line-' + line); |
| 25 |
if (lineEl) { |
if (lineEl) { |
| 26 |
lineText = lineEl.innerHTML |
lineText = lineEl.innerHTML |
| 27 |
|
.replace (/<var>U\+([0-9A-F]{4})<\/var>/g, function (s) { |
| 28 |
|
return String.fromCharCode (parseInt (s, 16)); |
| 29 |
|
}) |
| 30 |
.replace (/</g, '<') |
.replace (/</g, '<') |
| 31 |
.replace (/>/g, '>') |
.replace (/>/g, '>') |
| 32 |
.replace (/ /g, '\u00A0') |
.replace (/ /g, '\u00A0') |