Matitaweb: Fixes a bug which prevented Mozilla from displaying long goals

[helm.git] / matitaB / matita / html / matitaweb.js

diff --git a/matitaB/matita/html/matitaweb.js b/matitaB/matita/html/matitaweb.js
index d367b6bb3019a02590894f09c4e3d455a2ca4eb8..20d0fec43dbcf9557da473af7fae857413b3d60e 100644 (file)
--- a/matitaB/matita/html/matitaweb.js
+++ b/matitaB/matita/html/matitaweb.js
@@ -211,10 +211,10 @@ function lookup_tex(texmacro)
 function strip_tags(tagname,classname) 
 {
     var tags = unlocked.getElementsByTagName(tagname);
-    var tlen = tags.length; // preserving the value from removeChild operations
     if (is_defined(classname)) {
        tags = filterByClass(tags,classname);
     }
+    var tlen = tags.length; // preserving the value from removeChild operations
     for (i = 0; i < tlen; i++) {
         var children = tags[i].childNodes;
         for (j = 0; j < children.length; j++) {
@@ -420,8 +420,9 @@ function populate_goalarray(menv)
       var tmp_goallist = "";
       for (i = 0; i < menv.length; i++) {
         metano = menv[i].getAttribute("number");
-       metaname = menv[i].childNodes[0].childNodes[0].data;
-       goal = menv[i].childNodes[1].childNodes[0].data;
+       // item 0 = <metaname>, item 1 = <goal>
+       metaname = menv[i].childNodes[0].childNodes[0].wholeText;
+       goal = menv[i].childNodes[1].childNodes[0].wholeText;
         debug ("found meta n. " + metano);
         debug ("found goal\nBEGIN" + goal + "\nEND");
         goalarray[metano] = goal;