author | wenzelm |
Sun, 13 Dec 2020 16:35:37 +0100 | |
changeset 72900 | c9813630cca4 |
parent 71704 | b9a5eb0f3b43 |
child 73340 | 0ffcad1f6130 |
permissions | -rw-r--r-- |
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 | 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 | 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 |
} |