# HG changeset patch
# User wenzelm
# Date 1274344280 -7200
# Node ID aaa7cac3e54aa9a13e3b5a26eb0345d595646c7c
# Parent  fd641bc8522204fa5b28998276c6f242dd452bfb
inverted "Freeze" to "Follow", which is the default;
update unconditionally;

diff -r fd641bc85222 -r aaa7cac3e54a src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Wed May 19 21:18:02 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 10:31:20 2010 +0200
@@ -36,13 +36,17 @@
 
   /* controls */
 
+  private case class Render(body: List[XML.Tree])
+
   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
+          val document = model.recent_document
+          document.command_at(view.getTextArea.getCaretPosition) match {
+            case Some((cmd, _)) =>
+              output_actor ! Render(document.current_state(cmd).map(_.results) getOrElse Nil)
             case None =>
           }
         case None =>
@@ -54,7 +58,8 @@
     reactions += { case ButtonClicked(_) => handle_update() }
   }
 
-  private val freeze = new ToggleButton("Freeze")
+  val follow = new ToggleButton("Follow")
+  follow.selected = true
 
 
   /* actor wiring */
@@ -62,9 +67,13 @@
   private val output_actor = actor {
     loop {
       react {
+        case Session.Global_Settings => html_panel.init(Isabelle.font_size())
+
+        case Render(body) => html_panel.render(body)
+
         case cmd: Command =>
           Swing_Thread.now {
-            if (freeze.selected) None else Document_Model(view.getBuffer)
+            if (follow.selected) Document_Model(view.getBuffer) else None
           } match {
             case None =>
             case Some(model) =>
@@ -72,8 +81,6 @@
               html_panel.render(body)
           }
 
-        case Session.Global_Settings => html_panel.init(Isabelle.font_size())
-
         case bad => System.err.println("output_actor: ignoring bad message " + bad)
       }
     }
@@ -96,6 +103,6 @@
 
   /* init controls */
 
-  controls.contents ++= List(update, freeze)
+  controls.contents ++= List(update, follow)
   handle_update()
 }