src/Pure/PIDE/session.scala
changeset 56775 59f70b89e5fd
parent 56772 725a192f8081
child 56782 433cf57550fa
     1.1 --- a/src/Pure/PIDE/session.scala	Mon Apr 28 15:29:09 2014 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Mon Apr 28 16:17:07 2014 +0200
     1.3 @@ -75,6 +75,27 @@
     1.4    //}}}
     1.5  
     1.6  
     1.7 +  /* syslog */
     1.8 +
     1.9 +  private[Session] class Syslog(limit: Int)
    1.10 +  {
    1.11 +    private var queue = Queue.empty[XML.Elem]
    1.12 +    private var length = 0
    1.13 +
    1.14 +    def += (msg: XML.Elem): Unit = synchronized {
    1.15 +      queue = queue.enqueue(msg)
    1.16 +      length += 1
    1.17 +      if (length > limit) queue = queue.dequeue._2
    1.18 +    }
    1.19 +
    1.20 +    def content: String = synchronized {
    1.21 +      cat_lines(queue.iterator.map(XML.content)) +
    1.22 +      (if (length > limit) "\n(A total of " + length + " messages...)" else "")
    1.23 +    }
    1.24 +  }
    1.25 +
    1.26 +
    1.27 +
    1.28    /* protocol handlers */
    1.29  
    1.30    abstract class Protocol_Handler
    1.31 @@ -207,8 +228,8 @@
    1.32  
    1.33    /* global state */
    1.34  
    1.35 -  private val syslog = Synchronized(Queue.empty[XML.Elem])
    1.36 -  def current_syslog(): String = cat_lines(syslog.value.iterator.map(XML.content))
    1.37 +  private val syslog = new Session.Syslog(syslog_limit)
    1.38 +  def syslog_content(): String = syslog.content
    1.39  
    1.40    @volatile private var _phase: Session.Phase = Session.Inactive
    1.41    private def phase_=(new_phase: Session.Phase)
    1.42 @@ -476,16 +497,15 @@
    1.43          //{{{
    1.44          arg match {
    1.45            case output: Prover.Output =>
    1.46 -            if (output.is_stdout || output.is_stderr) raw_output_messages.post(output)
    1.47 +            if (output.is_stdout || output.is_stderr)
    1.48 +              raw_output_messages.post(output)
    1.49              else handle_output(output)
    1.50 +
    1.51              if (output.is_syslog) {
    1.52 -              syslog.change(queue =>
    1.53 -                {
    1.54 -                  val queue1 = queue.enqueue(output.message)
    1.55 -                  if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
    1.56 -                })
    1.57 +              syslog += output.message
    1.58                syslog_messages.post(output)
    1.59              }
    1.60 +
    1.61              all_messages.post(output)
    1.62  
    1.63            case input: Prover.Input =>