# HG changeset patch
# User wenzelm
# Date 1330790370 -3600
# Node ID 06a9b24c4a36e3f0bbb95678bbbe3244b681c374
# Parent  44c28a33c461f8b1894a06fa0bf07e79f54c99a9
explicit syslog_limit reduces danger of low-level message flooding;
tuned;

diff -r 44c28a33c461 -r 06a9b24c4a36 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Mar 03 14:04:49 2012 +0100
+++ b/src/Pure/System/session.scala	Sat Mar 03 16:59:30 2012 +0100
@@ -12,6 +12,7 @@
 import java.util.{Timer, TimerTask}
 
 import scala.collection.mutable
+import scala.collection.immutable.Queue
 import scala.actors.TIMEOUT
 import scala.actors.Actor._
 
@@ -37,7 +38,7 @@
 
 class Session(thy_load: Thy_Load = new Thy_Load)
 {
-  /* real time parameters */  // FIXME properties or settings (!?)
+  /* tuning parameters */  // FIXME properties or settings (!?)
 
   val message_delay = Time.seconds(0.01)  // prover messages
   val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
@@ -46,6 +47,7 @@
   val load_delay = Time.seconds(0.5)  // file load operations (new buffers etc.)
   val prune_delay = Time.seconds(60.0)  // prune history -- delete old versions
   val prune_size = 0  // size of retained history
+  val syslog_limit = 100
 
 
   /* pervasive event buses */
@@ -119,8 +121,8 @@
   @volatile private var syntax = Outer_Syntax.init()
   def current_syntax(): Outer_Syntax = syntax
 
-  @volatile private var reverse_syslog = List[XML.Elem]()
-  def syslog(): String = cat_lines(reverse_syslog.reverse.map(msg => XML.content(msg).mkString))
+  private val syslog = Volatile(Queue.empty[XML.Elem])
+  def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
 
   @volatile private var _phase: Session.Phase = Session.Inactive
   private def phase_=(new_phase: Session.Phase)
@@ -191,7 +193,14 @@
       def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
         buffer += msg
         msg match {
-          case result: Isabelle_Process.Result if result.is_raw => flush()
+          case result: Isabelle_Process.Result =>
+            if (result.is_syslog)
+              syslog >> (queue =>
+                {
+                  val queue1 = queue.enqueue(result.message)
+                  if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
+                })
+            if (result.is_raw) flush()
           case _ =>
         }
       }
@@ -404,11 +413,8 @@
           syntax += name
 
         case _ =>
-          if (result.is_syslog) {
-            reverse_syslog ::= result.message
-            if (result.is_exit && phase == Session.Startup) phase = Session.Failed
-            else if (result.is_exit) phase = Session.Inactive
-          }
+          if (result.is_exit && phase == Session.Startup) phase = Session.Failed
+          else if (result.is_exit) phase = Session.Inactive
           else if (result.is_stdout) { }
           else bad_result(result)
       }
diff -r 44c28a33c461 -r 06a9b24c4a36 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sat Mar 03 14:04:49 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Mar 03 16:59:30 2012 +0100
@@ -387,7 +387,7 @@
           phase match {
             case Session.Failed =>
               Swing_Thread.now {
-                val text = new scala.swing.TextArea(Isabelle.session.syslog())
+                val text = new scala.swing.TextArea(Isabelle.session.current_syslog())
                 text.editable = false
                 Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
               }
diff -r 44c28a33c461 -r 06a9b24c4a36 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sat Mar 03 14:04:49 2012 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Mar 03 16:59:30 2012 +0100
@@ -43,7 +43,7 @@
   status.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
   status.selection.intervalMode = ListView.IntervalMode.Single
 
-  private val syslog = new TextArea(Isabelle.session.syslog())
+  private val syslog = new TextArea(Isabelle.session.current_syslog())
 
   private val tabs = new TabbedPane {
     pages += new TabbedPane.Page("README", Component.wrap(readme))
@@ -176,10 +176,8 @@
         case result: Isabelle_Process.Result =>
           if (result.is_syslog)
             Swing_Thread.now {
-              val text = Isabelle.session.syslog()
-              if (text != syslog.text) {
-                syslog.text = text
-              }
+              val text = Isabelle.session.current_syslog()
+              if (text != syslog.text) syslog.text = text
             }
 
         case phase: Session.Phase =>