src/Tools/jEdit/src/syslog_dockable.scala
author wenzelm
Mon, 28 Apr 2014 16:17:07 +0200
changeset 56775 59f70b89e5fd
parent 56715 52125652e82a
child 57612 990ffb84489b
permissions -rw-r--r--
improved syslog performance -- avoid denial-of-service e.g. with threads_trace = 5 and active Syslog dockable;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/syslog_dockable.scala
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
     3
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
     4
Dockable window for syslog.
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
     5
*/
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
     6
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
     8
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
     9
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    10
import isabelle._
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    11
56775
59f70b89e5fd improved syslog performance -- avoid denial-of-service e.g. with threads_trace = 5 and active Syslog dockable;
wenzelm
parents: 56715
diff changeset
    12
import scala.swing.{TextArea, ScrollPane}
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    13
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    14
import org.gjt.sp.jedit.View
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    15
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    16
49559
wenzelm
parents: 48021
diff changeset
    17
class Syslog_Dockable(view: View, position: String) extends Dockable(view, position)
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    18
{
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    19
  /* GUI components */
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    20
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    21
  private val syslog = new TextArea()
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    22
56775
59f70b89e5fd improved syslog performance -- avoid denial-of-service e.g. with threads_trace = 5 and active Syslog dockable;
wenzelm
parents: 56715
diff changeset
    23
  private def syslog_delay = Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay"))
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    24
  {
56775
59f70b89e5fd improved syslog performance -- avoid denial-of-service e.g. with threads_trace = 5 and active Syslog dockable;
wenzelm
parents: 56715
diff changeset
    25
    val text = PIDE.session.syslog_content()
53177
dcac8d837b9c more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents: 50205
diff changeset
    26
    if (text != syslog.text) syslog.text = text
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    27
  }
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    28
56775
59f70b89e5fd improved syslog performance -- avoid denial-of-service e.g. with threads_trace = 5 and active Syslog dockable;
wenzelm
parents: 56715
diff changeset
    29
  set_content(new ScrollPane(syslog))
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    30
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    31
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    32
  /* main */
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    33
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    34
  private val main =
56775
59f70b89e5fd improved syslog performance -- avoid denial-of-service e.g. with threads_trace = 5 and active Syslog dockable;
wenzelm
parents: 56715
diff changeset
    35
    Session.Consumer[Prover.Output](getClass.getName) { case _ => syslog_delay.invoke() }
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    36
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    37
  override def init()
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    38
  {
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    39
    PIDE.session.syslog_messages += main
56775
59f70b89e5fd improved syslog performance -- avoid denial-of-service e.g. with threads_trace = 5 and active Syslog dockable;
wenzelm
parents: 56715
diff changeset
    40
    syslog_delay.invoke()
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    41
  }
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    42
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    43
  override def exit()
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    44
  {
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    45
    PIDE.session.syslog_messages -= main
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    46
  }
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    47
}