--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Wed May 19 18:05:34 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Wed May 19 21:18:02 2010 +0200
@@ -11,6 +11,9 @@
import scala.actors.Actor._
+import scala.swing.{FlowPanel, Button, ToggleButton}
+import scala.swing.event.ButtonClicked
+
import javax.swing.JPanel
import java.awt.{BorderLayout, Dimension}
@@ -24,17 +27,45 @@
if (position == DockableWindowManager.FLOATING)
setPreferredSize(new Dimension(500, 250))
+ val controls = new FlowPanel(FlowPanel.Alignment.Right)()
+ add(controls.peer, BorderLayout.NORTH)
+
val html_panel = new HTML_Panel(Isabelle.system, Isabelle.font_size(), null)
add(html_panel, BorderLayout.CENTER)
+ /* controls */
+
+ private def handle_update()
+ {
+ Swing_Thread.now {
+ Document_Model(view.getBuffer) match {
+ case Some(model) =>
+ model.recent_document.command_at(view.getTextArea.getCaretPosition) match {
+ case Some((cmd, _)) => output_actor ! cmd
+ case None =>
+ }
+ case None =>
+ }
+ }
+ }
+
+ private val update = new Button("Update") {
+ reactions += { case ButtonClicked(_) => handle_update() }
+ }
+
+ private val freeze = new ToggleButton("Freeze")
+
+
/* actor wiring */
private val output_actor = actor {
loop {
react {
case cmd: Command =>
- Swing_Thread.now { Document_Model(view.getBuffer) } match {
+ Swing_Thread.now {
+ if (freeze.selected) None else Document_Model(view.getBuffer)
+ } match {
case None =>
case Some(model) =>
val body = model.recent_document.current_state(cmd).map(_.results) getOrElse Nil
@@ -42,7 +73,7 @@
}
case Session.Global_Settings => html_panel.init(Isabelle.font_size())
-
+
case bad => System.err.println("output_actor: ignoring bad message " + bad)
}
}
@@ -61,4 +92,10 @@
Isabelle.session.global_settings -= output_actor
super.removeNotify()
}
+
+
+ /* init controls */
+
+ controls.contents ++= List(update, freeze)
+ handle_update()
}