# 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() }