- /*
- parsed = xml.getElementsByTagName("parsed")[0];
- len = parseInt(parsed.getAttribute("length"));
- // len0 = unlocked.innerHTML.length;
- unescaped = unlocked.innerHTML.html_to_matita();
- parsedtxt = parsed.childNodes[0].wholeText;
- //parsedtxt = unescaped.substr(0,len);
- unparsedtxt = unescaped.substr(len);
- lockedbackup += parsedtxt;
- locked.innerHTML = lockedbackup; //.matita_to_html();
- unlocked.innerHTML = unparsedtxt.matita_to_html();
- // len1 = unlocked.innerHTML.length;
- len2 = parsedtxt.length;
- metasenv = xml.getElementsByTagName("meta");
- // populate_goalarray(metasenv);
- statements = listcons(len2,statements);
- unlocked.scrollIntoView(true);
- // la populate non andrebbe fatta a ogni passo
- */