Method paintHeader

MiniZincIDE/codeeditor.cpp:666–684

}

void CodeEditor::paintHeader(QPaintEvent *event)
{
    QPainter painter(editorHeader);
    QFont lineNoFont = font();
    QFontMetrics fm(lineNoFont);
    int origFontHeight = fm.height();
    lineNoFont.setPointSizeF(lineNoFont.pointSizeF()*0.8);
    QFontMetrics fm2(lineNoFont);
    int heightDiff = (origFontHeight-fm2.height());
    painter.setFont(lineNoFont);


    painter.fillRect(event->rect(), theme.backgroundColor.get(darkMode));
    int baseX = debugInfo->geometry().x();
    painter.setPen(theme.textColor.get(darkMode));
    painter.drawText(baseX, heightDiff/2, DEBUG_TAB_SIZE, debugInfoOffset(), Qt::AlignCenter, "Cons");
    painter.drawText(baseX + DEBUG_TAB_SIZE, heightDiff/2, DEBUG_TAB_SIZE, debugInfoOffset(), Qt::AlignCenter, "Vars");
    painter.drawText(baseX + DEBUG_TAB_SIZE*2, heightDiff/2, DEBUG_TAB_SIZE, debugInfoOffset(), Qt::AlignCenter, "Time");
}

void CodeEditor::setEditorFont(QFont& font)
{