1.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Wed May 19 18:05:34 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Wed May 19 21:18:02 2010 +0200
     1.3 @@ -11,6 +11,9 @@
     1.4  
     1.5  import scala.actors.Actor._
     1.6  
     1.7 +import scala.swing.{FlowPanel, Button, ToggleButton}
     1.8 +import scala.swing.event.ButtonClicked
     1.9 +
    1.10  import javax.swing.JPanel
    1.11  import java.awt.{BorderLayout, Dimension}
    1.12  
    1.13 @@ -24,17 +27,45 @@
    1.14    if (position == DockableWindowManager.FLOATING)
    1.15      setPreferredSize(new Dimension(500, 250))
    1.16  
    1.17 +  val controls = new FlowPanel(FlowPanel.Alignment.Right)()
    1.18 +  add(controls.peer, BorderLayout.NORTH)
    1.19 +
    1.20    val html_panel = new HTML_Panel(Isabelle.system, Isabelle.font_size(), null)
    1.21    add(html_panel, BorderLayout.CENTER)
    1.22  
    1.23  
    1.24 +  /* controls */
    1.25 +
    1.26 +  private def handle_update()
    1.27 +  {
    1.28 +    Swing_Thread.now {
    1.29 +      Document_Model(view.getBuffer) match {
    1.30 +        case Some(model) =>
    1.31 +          model.recent_document.command_at(view.getTextArea.getCaretPosition) match {
    1.32 +            case Some((cmd, _)) => output_actor ! cmd
    1.33 +            case None =>
    1.34 +          }
    1.35 +        case None =>
    1.36 +      }
    1.37 +    }
    1.38 +  }
    1.39 +
    1.40 +  private val update = new Button("Update") {
    1.41 +    reactions += { case ButtonClicked(_) => handle_update() }
    1.42 +  }
    1.43 +
    1.44 +  private val freeze = new ToggleButton("Freeze")
    1.45 +
    1.46 +
    1.47    /* actor wiring */
    1.48  
    1.49    private val output_actor = actor {
    1.50      loop {
    1.51        react {
    1.52          case cmd: Command =>
    1.53 -          Swing_Thread.now { Document_Model(view.getBuffer) } match {
    1.54 +          Swing_Thread.now {
    1.55 +            if (freeze.selected) None else Document_Model(view.getBuffer)
    1.56 +          } match {
    1.57              case None =>
    1.58              case Some(model) =>
    1.59                val body = model.recent_document.current_state(cmd).map(_.results) getOrElse Nil
    1.60 @@ -42,7 +73,7 @@
    1.61            }
    1.62  
    1.63          case Session.Global_Settings => html_panel.init(Isabelle.font_size())
    1.64 -          
    1.65 +
    1.66          case bad => System.err.println("output_actor: ignoring bad message " + bad)
    1.67        }
    1.68      }
    1.69 @@ -61,4 +92,10 @@
    1.70      Isabelle.session.global_settings -= output_actor
    1.71      super.removeNotify()
    1.72    }
    1.73 +
    1.74 +
    1.75 +  /* init controls */
    1.76 +
    1.77 +  controls.contents ++= List(update, freeze)
    1.78 +  handle_update()
    1.79  }