1.1 --- a/src/Tools/jEdit/plugin/dockables.xml	Tue Dec 08 21:48:12 2009 +0100
     1.2 +++ b/src/Tools/jEdit/plugin/dockables.xml	Tue Dec 08 21:49:30 2009 +0100
     1.3 @@ -3,12 +3,12 @@
     1.4  
     1.5  <DOCKABLES>
     1.6  	<DOCKABLE NAME="isabelle-results" MOVABLE="TRUE">
     1.7 -		new isabelle.jedit.Results_Dockable(view, position).peer();
     1.8 +		new isabelle.jedit.Results_Dockable(view, position);
     1.9  	</DOCKABLE>
    1.10  	<DOCKABLE NAME="isabelle-raw-output" MOVABLE="TRUE">
    1.11  		new isabelle.jedit.Raw_Output_Dockable(view, position);
    1.12  	</DOCKABLE>
    1.13  	<DOCKABLE NAME="isabelle-history" MOVABLE="TRUE">
    1.14 -		new isabelle.jedit.History_Dockable(view, position).peer();
    1.15 +		new isabelle.jedit.History_Dockable(view, position).peer ();
    1.16  	</DOCKABLE>
    1.17  </DOCKABLES>
    1.18 \ No newline at end of file

     2.1 --- a/src/Tools/jEdit/src/jedit/results_dockable.scala	Tue Dec 08 21:48:12 2009 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit/results_dockable.scala	Tue Dec 08 21:49:30 2009 +0100
     2.3 @@ -7,36 +7,69 @@
     2.4  package isabelle.jedit
     2.5  
     2.6  
     2.7 -import isabelle.proofdocument.HTML_Panel
     2.8 +import isabelle.proofdocument.{Command, HTML_Panel}
     2.9  
    2.10  import scala.io.Source
    2.11 -import scala.swing.{BorderPanel, Component}
    2.12 +import scala.actors.Actor._
    2.13  
    2.14 -import java.awt.Dimension
    2.15 +import javax.swing.JPanel
    2.16 +import java.awt.{BorderLayout, Dimension}
    2.17  
    2.18  import org.gjt.sp.jedit.View
    2.19  import org.gjt.sp.jedit.gui.DockableWindowManager
    2.20  
    2.21  
    2.22  
    2.23 -class Results_Dockable(view: View, position: String) extends BorderPanel
    2.24 +class Results_Dockable(view: View, position: String) extends JPanel
    2.25  {
    2.26    // outer panel
    2.27  
    2.28    if (position == DockableWindowManager.FLOATING)
    2.29 -    preferredSize = new Dimension(500, 250)
    2.30 +    setPreferredSize(new Dimension(500, 250))
    2.31 +  setLayout(new BorderLayout)
    2.32  
    2.33  
    2.34    // HTML panel
    2.35  
    2.36 -  val html_panel = new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"))
    2.37 -  add(Component.wrap(html_panel), BorderPanel.Position.Center)
    2.38 +  private val html_panel = new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"))
    2.39 +  add(html_panel, BorderLayout.CENTER)
    2.40  
    2.41 -  Isabelle.plugin.state_update += (cmd => {
    2.42 -    val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
    2.43 -    val body =
    2.44 -      if (cmd == null) Nil  // FIXME ??
    2.45 -      else cmd.results(theory_view.current_document)
    2.46 -    html_panel.render(body)
    2.47 -  })
    2.48 +
    2.49 +  /* actor wiring */
    2.50 +
    2.51 +  private val results_actor = actor {
    2.52 +    loop {
    2.53 +      react {
    2.54 +        case cmd: Command =>
    2.55 +          val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
    2.56 +          val body =
    2.57 +            if (cmd == null) Nil  // FIXME ??
    2.58 +            else cmd.results(theory_view.current_document)
    2.59 +          html_panel.render(body)
    2.60 +          
    2.61 +        case bad => System.err.println("prover: ignoring bad message " + bad)
    2.62 +      }
    2.63 +    }
    2.64 +  }
    2.65 +
    2.66 +  private val properties_actor = actor {
    2.67 +    loop {
    2.68 +      react {
    2.69 +        case _: Unit => html_panel.init(Isabelle.Int_Property("font-size"))
    2.70 +        case bad => System.err.println("prover: ignoring bad message " + bad)
    2.71 +      }
    2.72 +    }
    2.73 +  }
    2.74 +
    2.75 +  override def addNotify() {
    2.76 +    super.addNotify()
    2.77 +    Isabelle.plugin.state_update += results_actor
    2.78 +    Isabelle.plugin.properties_changed += properties_actor
    2.79 +  }
    2.80 +
    2.81 +  override def removeNotify() {
    2.82 +    Isabelle.plugin.state_update -= results_actor
    2.83 +    Isabelle.plugin.properties_changed -= properties_actor
    2.84 +    super.removeNotify()
    2.85 +  }
    2.86  }