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') |