8 |
8 |
9 |
9 |
10 import isabelle._ |
10 import isabelle._ |
11 |
11 |
12 import scala.actors.Actor._ |
12 import scala.actors.Actor._ |
13 |
13 import scala.swing.{TextArea, ScrollPane} |
14 import java.awt.{Dimension, Graphics, BorderLayout} |
|
15 import javax.swing.{JPanel, JTextArea, JScrollPane} |
|
16 |
14 |
17 import org.gjt.sp.jedit.View |
15 import org.gjt.sp.jedit.View |
18 import org.gjt.sp.jedit.gui.DockableWindowManager |
|
19 |
16 |
20 |
17 |
21 class Raw_Output_Dockable(view: View, position: String) extends JPanel(new BorderLayout) |
18 class Raw_Output_Dockable(view: View, position: String) |
|
19 extends Dockable(view: View, position: String) |
22 { |
20 { |
23 if (position == DockableWindowManager.FLOATING) |
21 private val text_area = new TextArea |
24 setPreferredSize(new Dimension(500, 250)) |
22 set_content(new ScrollPane(text_area)) |
25 |
|
26 private val text_area = new JTextArea |
|
27 add(new JScrollPane(text_area), BorderLayout.CENTER) |
|
28 |
23 |
29 |
24 |
30 /* actor wiring */ |
25 /* main actor */ |
31 |
26 |
32 private val raw_output_actor = actor { |
27 private val main_actor = actor { |
33 loop { |
28 loop { |
34 react { |
29 react { |
35 case result: Isabelle_Process.Result => |
30 case result: Isabelle_Process.Result => |
36 Swing_Thread.now { text_area.append(XML.content(result.message).mkString) } |
31 Swing_Thread.now { text_area.append(XML.content(result.message).mkString) } |
37 |
32 |
38 case bad => System.err.println("raw_output_actor: ignoring bad message " + bad) |
33 case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad) |
39 } |
34 } |
40 } |
35 } |
41 } |
36 } |
42 |
37 |
43 override def addNotify() |
38 override def init() { Isabelle.session.raw_output += main_actor } |
44 { |
39 override def exit() { Isabelle.session.raw_output -= main_actor } |
45 super.addNotify() |
|
46 Isabelle.session.raw_output += raw_output_actor |
|
47 } |
|
48 |
|
49 override def removeNotify() |
|
50 { |
|
51 Isabelle.session.raw_output -= raw_output_actor |
|
52 super.removeNotify() |
|
53 } |
|
54 } |
40 } |