improved syslog performance -- avoid denial-of-service e.g. with threads_trace = 5 and active Syslog dockable;
--- a/src/Pure/PIDE/session.scala Mon Apr 28 15:29:09 2014 +0200
+++ b/src/Pure/PIDE/session.scala Mon Apr 28 16:17:07 2014 +0200
@@ -75,6 +75,27 @@
//}}}
+ /* syslog */
+
+ private[Session] class Syslog(limit: Int)
+ {
+ private var queue = Queue.empty[XML.Elem]
+ private var length = 0
+
+ def += (msg: XML.Elem): Unit = synchronized {
+ queue = queue.enqueue(msg)
+ length += 1
+ if (length > limit) queue = queue.dequeue._2
+ }
+
+ def content: String = synchronized {
+ cat_lines(queue.iterator.map(XML.content)) +
+ (if (length > limit) "\n(A total of " + length + " messages...)" else "")
+ }
+ }
+
+
+
/* protocol handlers */
abstract class Protocol_Handler
@@ -207,8 +228,8 @@
/* global state */
- private val syslog = Synchronized(Queue.empty[XML.Elem])
- def current_syslog(): String = cat_lines(syslog.value.iterator.map(XML.content))
+ private val syslog = new Session.Syslog(syslog_limit)
+ def syslog_content(): String = syslog.content
@volatile private var _phase: Session.Phase = Session.Inactive
private def phase_=(new_phase: Session.Phase)
@@ -476,16 +497,15 @@
//{{{
arg match {
case output: Prover.Output =>
- if (output.is_stdout || output.is_stderr) raw_output_messages.post(output)
+ if (output.is_stdout || output.is_stderr)
+ raw_output_messages.post(output)
else handle_output(output)
+
if (output.is_syslog) {
- syslog.change(queue =>
- {
- val queue1 = queue.enqueue(output.message)
- if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
- })
+ syslog += output.message
syslog_messages.post(output)
}
+
all_messages.post(output)
case input: Prover.Input =>
--- a/src/Tools/jEdit/src/plugin.scala Mon Apr 28 15:29:09 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Mon Apr 28 16:17:07 2014 +0200
@@ -249,7 +249,7 @@
case Session.Inactive | Session.Failed =>
Swing_Thread.later {
GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
- "Isabelle Syslog", GUI.scrollable_text(PIDE.session.current_syslog()))
+ "Isabelle Syslog", GUI.scrollable_text(PIDE.session.syslog_content()))
}
case Session.Ready =>
--- a/src/Tools/jEdit/src/syslog_dockable.scala Mon Apr 28 15:29:09 2014 +0200
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Mon Apr 28 16:17:07 2014 +0200
@@ -9,7 +9,7 @@
import isabelle._
-import scala.swing.TextArea
+import scala.swing.{TextArea, ScrollPane}
import org.gjt.sp.jedit.View
@@ -20,29 +20,24 @@
private val syslog = new TextArea()
- private def update_syslog()
+ private def syslog_delay = Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay"))
{
- Swing_Thread.require {}
-
- val text = PIDE.session.current_syslog()
+ val text = PIDE.session.syslog_content()
if (text != syslog.text) syslog.text = text
}
- set_content(syslog)
+ set_content(new ScrollPane(syslog))
/* main */
private val main =
- Session.Consumer[Prover.Output](getClass.getName) {
- case output =>
- if (output.is_syslog) Swing_Thread.later { update_syslog() }
- }
+ Session.Consumer[Prover.Output](getClass.getName) { case _ => syslog_delay.invoke() }
override def init()
{
PIDE.session.syslog_messages += main
- update_syslog()
+ syslog_delay.invoke()
}
override def exit()