| author | wenzelm |
| Mon, 11 Jan 2010 20:51:58 +0100 | |
| changeset 34870 | d0057d9777ce |
| parent 34835 | d785f72ef388 |
| child 34874 | e596a0b71f3c |
| permissions | -rw-r--r-- |
| wenzelm@34411 | 1 |
/* |
| wenzelm@34768 | 2 |
* Dockable window with result message output |
| wenzelm@34411 | 3 |
* |
| wenzelm@34768 | 4 |
* @author Makarius |
| wenzelm@34411 | 5 |
*/ |
| wenzelm@34411 | 6 |
|
| wenzelm@34321 | 7 |
package isabelle.jedit |
| wenzelm@34321 | 8 |
|
| wenzelm@34763 | 9 |
|
| wenzelm@34794 | 10 |
import isabelle.proofdocument.{Command, HTML_Panel, Session}
|
| wenzelm@34321 | 11 |
|
| wenzelm@34771 | 12 |
import scala.actors.Actor._ |
| wenzelm@34763 | 13 |
|
| wenzelm@34771 | 14 |
import javax.swing.JPanel |
| wenzelm@34771 | 15 |
import java.awt.{BorderLayout, Dimension}
|
| wenzelm@34751 | 16 |
|
| wenzelm@34321 | 17 |
import org.gjt.sp.jedit.View |
| wenzelm@34427 | 18 |
import org.gjt.sp.jedit.gui.DockableWindowManager |
| wenzelm@34427 | 19 |
|
| wenzelm@34748 | 20 |
|
| wenzelm@34321 | 21 |
|
| wenzelm@34794 | 22 |
class Output_Dockable(view: View, position: String) extends JPanel(new BorderLayout) |
| wenzelm@34763 | 23 |
{
|
| wenzelm@34427 | 24 |
if (position == DockableWindowManager.FLOATING) |
| wenzelm@34771 | 25 |
setPreferredSize(new Dimension(500, 250)) |
| wenzelm@34774 | 26 |
|
| wenzelm@34778 | 27 |
private val html_panel = |
| wenzelm@34778 | 28 |
new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"), null)
|
| wenzelm@34771 | 29 |
add(html_panel, BorderLayout.CENTER) |
| wenzelm@34748 | 30 |
|
| wenzelm@34771 | 31 |
|
| wenzelm@34771 | 32 |
/* actor wiring */ |
| wenzelm@34771 | 33 |
|
| wenzelm@34776 | 34 |
private val output_actor = actor {
|
| wenzelm@34771 | 35 |
loop {
|
| wenzelm@34771 | 36 |
react {
|
| wenzelm@34771 | 37 |
case cmd: Command => |
| wenzelm@34792 | 38 |
Swing_Thread.now { Document_Model(view.getBuffer) } match {
|
| wenzelm@34780 | 39 |
case None => |
| wenzelm@34787 | 40 |
case Some(model) => |
| wenzelm@34870 | 41 |
val body = model.recent_document.current_state(cmd).map(_.results) getOrElse Nil |
| wenzelm@34780 | 42 |
html_panel.render(body) |
| wenzelm@34780 | 43 |
} |
| wenzelm@34794 | 44 |
|
| wenzelm@34794 | 45 |
case Session.Global_Settings => |
| wenzelm@34794 | 46 |
html_panel.init(Isabelle.Int_Property("font-size"))
|
| wenzelm@34771 | 47 |
|
| wenzelm@34776 | 48 |
case bad => System.err.println("output_actor: ignoring bad message " + bad)
|
| wenzelm@34771 | 49 |
} |
| wenzelm@34771 | 50 |
} |
| wenzelm@34771 | 51 |
} |
| wenzelm@34771 | 52 |
|
| wenzelm@34780 | 53 |
override def addNotify() |
| wenzelm@34780 | 54 |
{
|
| wenzelm@34771 | 55 |
super.addNotify() |
| wenzelm@34780 | 56 |
Isabelle.session.results += output_actor |
| wenzelm@34794 | 57 |
Isabelle.session.global_settings += output_actor |
| wenzelm@34771 | 58 |
} |
| wenzelm@34771 | 59 |
|
| wenzelm@34780 | 60 |
override def removeNotify() |
| wenzelm@34780 | 61 |
{
|
| wenzelm@34780 | 62 |
Isabelle.session.results -= output_actor |
| wenzelm@34794 | 63 |
Isabelle.session.global_settings -= output_actor |
| wenzelm@34771 | 64 |
super.removeNotify() |
| wenzelm@34771 | 65 |
} |
| wenzelm@34321 | 66 |
} |