diff options
| -rw-r--r-- | lib/js/urweb.js | 26 |
1 files changed, 15 insertions, 11 deletions
diff --git a/lib/js/urweb.js b/lib/js/urweb.js index 8bb3dbe5..b599393b 100644 --- a/lib/js/urweb.js +++ b/lib/js/urweb.js @@ -636,21 +636,25 @@ function cr(n) { return closures[n]; } -function flattenAcc(a, cls, tr) { - if (tr.cat1 != null) { - flattenAcc(a, cls, tr.cat1); - flattenAcc(a, cls, tr.cat2); - } else if (tr.closure != null) { - var cl = newClosure(tr.closure); - cls.v = cons(cl, cls.v); - a.push("cr(", cl.toString(), ")"); - } else - a.push(tr); +function flattenAcc(a, cls, trs) { + while (trs) { + var tr = trs.data; + trs = trs.next; + + if (tr.cat1 != null) { + trs = cons(tr.cat1, cons(tr.cat2, trs)); + } else if (tr.closure != null) { + var cl = newClosure(tr.closure); + cls.v = cons(cl, cls.v); + a.push("cr(", cl.toString(), ")"); + } else + a.push(tr); + } } function flatten(cls, tr) { var a = []; - flattenAcc(a, cls, tr); + flattenAcc(a, cls, cons(tr, null)); return a.join(""); } |