equal
deleted
inserted
replaced
1 /* Title: Tools/jEdit/src/jedit/protocol_dockable.scala |
|
2 Author: Makarius |
|
3 |
|
4 Dockable window for protocol messages. |
|
5 */ |
|
6 |
|
7 package isabelle.jedit |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import scala.actors.Actor._ |
|
13 import scala.swing.{TextArea, ScrollPane} |
|
14 |
|
15 import org.gjt.sp.jedit.View |
|
16 |
|
17 |
|
18 class Protocol_Dockable(view: View, position: String) extends Dockable(view, position) |
|
19 { |
|
20 private val text_area = new TextArea |
|
21 set_content(new ScrollPane(text_area)) |
|
22 |
|
23 |
|
24 /* main actor */ |
|
25 |
|
26 private val main_actor = actor { |
|
27 loop { |
|
28 react { |
|
29 case result: Isabelle_Process.Result => |
|
30 Swing_Thread.now { text_area.append(result.message.toString + "\n") } |
|
31 |
|
32 case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad) |
|
33 } |
|
34 } |
|
35 } |
|
36 |
|
37 override def init() { Isabelle.session.raw_messages += main_actor } |
|
38 override def exit() { Isabelle.session.raw_messages -= main_actor } |
|
39 } |
|