# HG changeset patch
# User wenzelm
# Date 1398694627 -7200
# Node ID 59f70b89e5fdb6d56deff13487af966c4cb39b45
# Parent  2d39c313f39e72b4987a6a8f3d89463df750eb04
improved syslog performance -- avoid denial-of-service e.g. with threads_trace = 5 and active Syslog dockable;

diff -r 2d39c313f39e -r 59f70b89e5fd src/Pure/PIDE/session.scala
--- 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 =>
diff -r 2d39c313f39e -r 59f70b89e5fd src/Tools/jEdit/src/plugin.scala
--- 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 =>
diff -r 2d39c313f39e -r 59f70b89e5fd src/Tools/jEdit/src/syslog_dockable.scala
--- 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()