author | wenzelm |
Mon, 29 Jul 2013 14:37:59 +0200 | |
changeset 52766 | 36c3c051b355 |
parent 50205 | 788c8263e634 |
child 55618 | 995162143ef4 |
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/raw_output_dockable.scala |
37065
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
3 |
|
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
4 |
Dockable window for raw process output (stdout). |
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
5 |
*/ |
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
6 |
|
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
8 |
|
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
9 |
|
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
10 |
import isabelle._ |
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
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 |
|
37065
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
14 |
import scala.actors.Actor._ |
37067 | 15 |
import scala.swing.{TextArea, ScrollPane} |
37065
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
16 |
|
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
17 |
import org.gjt.sp.jedit.View |
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
18 |
|
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
19 |
|
49559 | 20 |
class Raw_Output_Dockable(view: View, position: String) extends Dockable(view, position) |
37065
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
21 |
{ |
37067 | 22 |
private val text_area = new TextArea |
23 |
set_content(new ScrollPane(text_area)) |
|
37065
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
24 |
|
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
25 |
|
37067 | 26 |
/* main actor */ |
37065
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
27 |
|
37067 | 28 |
private val main_actor = actor { |
37065
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
29 |
loop { |
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
30 |
react { |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
45633
diff
changeset
|
31 |
case output: Isabelle_Process.Output => |
52766
36c3c051b355
show displaced messages (e.g. from protocol thread) as raw output;
wenzelm
parents:
50205
diff
changeset
|
32 |
Swing_Thread.later { |
36c3c051b355
show displaced messages (e.g. from protocol thread) as raw output;
wenzelm
parents:
50205
diff
changeset
|
33 |
text_area.append(XML.content(output.message)) |
36c3c051b355
show displaced messages (e.g. from protocol thread) as raw output;
wenzelm
parents:
50205
diff
changeset
|
34 |
if (!output.is_stdout && !output.is_stderr) text_area.append("\n") |
36c3c051b355
show displaced messages (e.g. from protocol thread) as raw output;
wenzelm
parents:
50205
diff
changeset
|
35 |
} |
37065
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
36 |
|
37067 | 37 |
case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad) |
37065
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
38 |
} |
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
39 |
} |
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
40 |
} |
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
41 |
|
50205 | 42 |
override def init() { PIDE.session.raw_output_messages += main_actor } |
43 |
override def exit() { PIDE.session.raw_output_messages -= main_actor } |
|
37065
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
diff
changeset
|
44 |
} |