# HG changeset patch
# User wenzelm
# Date 1274296682 -7200
# Node ID fd641bc8522204fa5b28998276c6f242dd452bfb
# Parent  8af34e1609680eb205c4a8b7e6db13479e09f74c
basic controls to freeze/update prover results;

diff -r 8af34e160968 -r fd641bc85222 src/Tools/jEdit/src/jedit/output_dockable.scala
--- 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()
 }