equal
deleted
inserted
replaced
7 package isabelle.jedit |
7 package isabelle.jedit |
8 |
8 |
9 |
9 |
10 import isabelle._ |
10 import isabelle._ |
11 |
11 |
12 import scala.actors.Actor._ |
|
13 import scala.swing.{TextArea, ScrollPane} |
12 import scala.swing.{TextArea, ScrollPane} |
14 |
13 |
15 import org.gjt.sp.jedit.View |
14 import org.gjt.sp.jedit.View |
16 |
15 |
17 |
16 |
19 { |
18 { |
20 private val text_area = new TextArea |
19 private val text_area = new TextArea |
21 set_content(new ScrollPane(text_area)) |
20 set_content(new ScrollPane(text_area)) |
22 |
21 |
23 |
22 |
24 /* main actor */ |
23 /* main */ |
25 |
24 |
26 private val main_actor = actor { |
25 private val main = |
27 loop { |
26 Session.Consumer[Prover.Output](getClass.getName) { |
28 react { |
27 case output: Prover.Output => |
29 case output: Prover.Output => |
28 Swing_Thread.later { |
30 Swing_Thread.later { |
29 text_area.append(XML.content(output.message)) |
31 text_area.append(XML.content(output.message)) |
30 if (!output.is_stdout && !output.is_stderr) text_area.append("\n") |
32 if (!output.is_stdout && !output.is_stderr) text_area.append("\n") |
31 } |
33 } |
32 } |
34 |
33 |
35 case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad) |
34 override def init() { PIDE.session.raw_output_messages += main } |
36 } |
35 override def exit() { PIDE.session.raw_output_messages -= main } |
37 } |
|
38 } |
|
39 |
|
40 override def init() { PIDE.session.raw_output_messages += main_actor } |
|
41 override def exit() { PIDE.session.raw_output_messages -= main_actor } |
|
42 } |
36 } |