minibar: adapt to changed bracket structure in linearization output

This commit is contained in:
hallgren
2013-11-06 16:45:24 +00:00
parent f9d044d294
commit 72a58a8114
2 changed files with 31 additions and 12 deletions

View File

@@ -207,7 +207,7 @@ Translations.prototype.show_translations=function(translationResults) {
trans.appendChild(wrap("pre",text(errs[i].msg)))
}
if(options.show_brackets)
trans.appendChild(div_class("brackets",draw_brackets(bra)));
trans.appendChild(div_class("brackets",draw_bracketss(bra)));
}
}
@@ -291,3 +291,9 @@ function draw_brackets(b) {
title:(b.fun||"_")+":"+b.cat+" "+b.fid+":"+b.index},
b.children.map(draw_brackets))
}
function draw_bracketss(bs) {
return Array.isArray(bs)
? bs.map(draw_brackets) //with gf>3.5, in some cases
: draw_brackets(b) // with gf<=3.5
}