BoxTranslator const & boxtranslator()
{
- static BoxTranslator translator = initBoxtranslator();
+ static BoxTranslator const translator = initBoxtranslator();
return translator;
}
BoxTranslatorLoc const & boxtranslator_loc()
{
- static BoxTranslatorLoc translator = initBoxtranslatorLoc();
+ static BoxTranslatorLoc const translator = initBoxtranslatorLoc();
return translator;
}
os << "\\begin{framed}%\n";
break;
case Boxed:
- if (width_string.empty()) {
- os << "\\framebox";
+ if (!width_string.empty()) {
if (!params_.inner_box) {
+ os << "\\framebox";
// Special widths, see usrguide sec. 3.5
// FIXME UNICODE
if (params_.special != "none") {
<< ']';
if (params_.hor_pos != 'c')
os << "[" << params_.hor_pos << "]";
- }
+ } else
+ os << "\\fbox";
} else
os << "\\fbox";
os << "{";