author | wenzelm |
Thu, 23 Sep 2010 20:34:05 +0200 | |
changeset 39631 | cad7a5b7f641 |
parent 39588 | 507fcf86e1e0 |
permissions | -rw-r--r-- |
36760 | 1 |
/* Title: Tools/jEdit/src/jedit/protocol_dockable.scala |
2 |
Author: Makarius |
|
3 |
||
37067 | 4 |
Dockable window for protocol messages. |
36760 | 5 |
*/ |
34408 | 6 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
8 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
9 |
|
36015 | 10 |
import isabelle._ |
11 |
||
34772 | 12 |
import scala.actors.Actor._ |
37067 | 13 |
import scala.swing.{TextArea, ScrollPane} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
14 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
15 |
import org.gjt.sp.jedit.View |
34424 | 16 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
17 |
|
37067 | 18 |
class Protocol_Dockable(view: View, position: String) extends Dockable(view, position) |
34760 | 19 |
{ |
37067 | 20 |
private val text_area = new TextArea |
21 |
set_content(new ScrollPane(text_area)) |
|
34772 | 22 |
|
23 |
||
37067 | 24 |
/* main actor */ |
34671 | 25 |
|
37067 | 26 |
private val main_actor = actor { |
34772 | 27 |
loop { |
28 |
react { |
|
29 |
case result: Isabelle_Process.Result => |
|
36987 | 30 |
Swing_Thread.now { text_area.append(result.message.toString + "\n") } |
34772 | 31 |
|
37067 | 32 |
case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad) |
34772 | 33 |
} |
34 |
} |
|
35 |
} |
|
36 |
||
39588 | 37 |
override def init() { Isabelle.session.raw_messages += main_actor } |
38 |
override def exit() { Isabelle.session.raw_messages -= main_actor } |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
39 |
} |