author | wenzelm |
Wed, 14 Mar 2012 15:09:33 +0100 | |
changeset 46918 | 1752164d916b |
parent 46774 | 38f113b052b1 |
child 50205 | 788c8263e634 |
permissions | -rw-r--r-- |
43282
5d294220ca43
moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents:
39588
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/protocol_dockable.scala |
36760 | 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 |
||
43520
cec9b95fa35d
explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents:
43282
diff
changeset
|
12 |
import java.lang.System |
cec9b95fa35d
explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents:
43282
diff
changeset
|
13 |
|
34772 | 14 |
import scala.actors.Actor._ |
37067 | 15 |
import scala.swing.{TextArea, ScrollPane} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
16 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
17 |
import org.gjt.sp.jedit.View |
34424 | 18 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
19 |
|
37067 | 20 |
class Protocol_Dockable(view: View, position: String) extends Dockable(view, position) |
34760 | 21 |
{ |
37067 | 22 |
private val text_area = new TextArea |
23 |
set_content(new ScrollPane(text_area)) |
|
34772 | 24 |
|
25 |
||
37067 | 26 |
/* main actor */ |
34671 | 27 |
|
37067 | 28 |
private val main_actor = actor { |
34772 | 29 |
loop { |
30 |
react { |
|
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43520
diff
changeset
|
31 |
case input: Isabelle_Process.Input => |
46918
1752164d916b
prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents:
46774
diff
changeset
|
32 |
Swing_Thread.later { text_area.append(input.toString + "\n") } |
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43520
diff
changeset
|
33 |
|
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46120
diff
changeset
|
34 |
case output: Isabelle_Process.Output => |
46918
1752164d916b
prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents:
46774
diff
changeset
|
35 |
Swing_Thread.later { text_area.append(output.message.toString + "\n") } |
34772 | 36 |
|
37067 | 37 |
case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad) |
34772 | 38 |
} |
39 |
} |
|
40 |
} |
|
41 |
||
46774 | 42 |
override def init() { Isabelle.session.all_messages += main_actor } |
43 |
override def exit() { Isabelle.session.all_messages -= main_actor } |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
44 |
} |