src/Tools/jEdit/src/syslog_dockable.scala
author wenzelm
Sun, 13 Dec 2020 16:35:37 +0100
changeset 72900 c9813630cca4
parent 71704 b9a5eb0f3b43
child 73340 0ffcad1f6130
permissions -rw-r--r--
clarified signature: more explicit types;
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._
66591
6efa351190d0 more robust: provide docking framework via base plugin;
wenzelm
parents: 57612
diff changeset
    11
import isabelle.jedit_base.Dockable
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    12
56775
59f70b89e5fd improved syslog performance -- avoid denial-of-service e.g. with threads_trace = 5 and active Syslog dockable;
wenzelm
parents: 56715
diff changeset
    13
import scala.swing.{TextArea, ScrollPane}
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    14
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    15
import org.gjt.sp.jedit.View
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    16
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    17
49559
wenzelm
parents: 48021
diff changeset
    18
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
    19
{
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    20
  /* GUI components */
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    21
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    22
  private val syslog = new TextArea()
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    23
71704
b9a5eb0f3b43 clarified modules;
wenzelm
parents: 66591
diff changeset
    24
  private def syslog_delay = Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true)
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    25
  {
56775
59f70b89e5fd improved syslog performance -- avoid denial-of-service e.g. with threads_trace = 5 and active Syslog dockable;
wenzelm
parents: 56715
diff changeset
    26
    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
    27
    if (text != syslog.text) syslog.text = text
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    28
  }
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    29
56775
59f70b89e5fd improved syslog performance -- avoid denial-of-service e.g. with threads_trace = 5 and active Syslog dockable;
wenzelm
parents: 56715
diff changeset
    30
  set_content(new ScrollPane(syslog))
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    31
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    32
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    33
  /* main */
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    34
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    35
  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
    36
    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
    37
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    38
  override def init()
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    39
  {
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    40
    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
    41
    syslog_delay.invoke()
48021
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
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    44
  override def exit()
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    45
  {
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    46
    PIDE.session.syslog_messages -= main
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    47
  }
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents:
diff changeset
    48
}