author | wenzelm |
Mon, 28 Apr 2014 16:17:07 +0200 | |
changeset 56775 | 59f70b89e5fd |
parent 56715 | 52125652e82a |
child 57612 | 990ffb84489b |
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._ |
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 | 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 |
} |