44 namespace Gecode {
namespace Gist {
48 :
public std::basic_ostream<char, std::char_traits<char> > {
51 :
public std::basic_streambuf<char, std::char_traits<char> > {
56 QTextBlockFormat bf = editor->textCursor().blockFormat();
57 bf.setBottomMargin(0);
58 editor->textCursor().setBlockFormat(bf);
59 editor->append(buffer);
62 virtual int overflow(
int v = std::char_traits<char>::eof()) {
70 Buf(QTextEdit* e) : editor(e) {}
76 : std::basic_ostream<char, std::char_traits<char> >(&_buf),
86 : QMainWindow(parent) {
94 QString fontFamily(
"Courier");
95 font.setFamily(fontFamily);
96 font.setFixedPitch(
true);
97 font.setPointSize(12);
100 editor =
new QTextEdit;
101 editor->setFont(font);
102 editor->setReadOnly(
true);
103 editor->setLineWrapMode(QTextEdit::FixedColumnWidth);
104 editor->setLineWrapColumnOrWidth(80);
107 QAction* clearText =
new QAction(
"Clear",
this);
108 clearText->setShortcut(QKeySequence(
"Ctrl+K"));
109 this->addAction(clearText);
110 connect(clearText, SIGNAL(triggered()), editor,
113 QAction* closeWindow =
new QAction(
"Close window",
this);
114 closeWindow->setShortcut(QKeySequence(
"Ctrl+W"));
115 this->addAction(closeWindow);
116 connect(closeWindow, SIGNAL(triggered()),
this,
119 QToolBar* t = addToolBar(
"Tools");
120 t->setFloatable(
false);
121 t->setMovable(
false);
122 t->addAction(clearText);
124 stayOnTop =
new QAction(
"Stay on top",
this);
125 stayOnTop->setCheckable(
true);
126 t->addAction(stayOnTop);
127 connect(stayOnTop, SIGNAL(changed()),
this,
131 setCentralWidget(editor);
132 setWindowTitle(QString((std::string(
"Gist Console: ") + name).c_str()));
134 setAttribute(Qt::WA_QuitOnClose,
false);
135 setAttribute(Qt::WA_DeleteOnClose,
false);
155 QTextBlockFormat bf = editor->textCursor().blockFormat();
156 bf.setBottomMargin(0);
157 editor->textCursor().setBlockFormat(bf);
158 editor->insertHtml(s);
159 editor->ensureCursorVisible();
164 if (stayOnTop->isChecked()) {
165 setWindowFlags(windowFlags() | Qt::WindowStaysOnTopHint);
167 setWindowFlags(windowFlags() & ~Qt::WindowStaysOnTopHint);