privatedef syslog_delay =
Delay.first(PIDE.session.update_delay, gui = true) { val text = PIDE.session.syslog.content() if (text != syslog.text) syslog.text = text
}
set_content(new ScrollPane(syslog))
/* main */
privateval main =
Session.Consumer[Prover.Output](getClass.getName) { case _ => syslog_delay.invoke() }
overridedef init(): Unit = {
PIDE.session.syslog_messages += main
syslog_delay.invoke()
}
overridedef exit(): Unit = {
PIDE.session.syslog_messages -= main
}
}
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.