merged
authorwenzelm
Thu May 27 13:13:30 2010 +0200 (2010-05-27)
changeset 3714256e1b6976d0e
parent 37141 8d231d3efcde
parent 37132 10ef4da1c314
child 37143 2a5182751151
child 37150 73e738371c90
merged
     1.1 --- a/src/Pure/PIDE/command.scala	Thu May 27 08:02:02 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu May 27 13:13:30 2010 +0200
     1.3 @@ -13,6 +13,9 @@
     1.4  import scala.collection.mutable
     1.5  
     1.6  
     1.7 +case class Command_Set(set: Set[Command])
     1.8 +
     1.9 +
    1.10  object Command
    1.11  {
    1.12    object Status extends Enumeration
    1.13 @@ -29,10 +32,10 @@
    1.14      command_id: Option[String], offset: Option[Int])
    1.15  }
    1.16  
    1.17 -
    1.18  class Command(
    1.19      val id: Isar_Document.Command_ID,
    1.20 -    val span: Thy_Syntax.Span)
    1.21 +    val span: Thy_Syntax.Span,
    1.22 +    val static_parent: Option[Command] = None)
    1.23    extends Session.Entity
    1.24  {
    1.25    /* classification */
    1.26 @@ -42,7 +45,9 @@
    1.27    def is_malformed: Boolean = !is_command && !is_ignored
    1.28  
    1.29    def name: String = if (is_command) span.head.content else ""
    1.30 -  override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
    1.31 +  override def toString =
    1.32 +    if (is_command) name + "(" + id + ")"
    1.33 +    else if (is_ignored) "<ignored>" else "<malformed>"
    1.34  
    1.35  
    1.36    /* source text */
    1.37 @@ -59,15 +64,17 @@
    1.38    @volatile protected var state = new State(this)
    1.39    def current_state: State = state
    1.40  
    1.41 -  private case class Consume(session: Session, message: XML.Tree)
    1.42 +  private case class Consume(message: XML.Tree, forward: Command => Unit)
    1.43    private case object Assign
    1.44  
    1.45    private val accumulator = actor {
    1.46      var assigned = false
    1.47      loop {
    1.48        react {
    1.49 -        case Consume(session: Session, message: XML.Tree) if !assigned =>
    1.50 -          state = state.+(session, message)
    1.51 +        case Consume(message, forward) if !assigned =>
    1.52 +          val old_state = state
    1.53 +          state = old_state + message
    1.54 +          if (!(state eq old_state)) forward(static_parent getOrElse this)
    1.55  
    1.56          case Assign =>
    1.57            assigned = true  // single assignment
    1.58 @@ -78,11 +85,14 @@
    1.59      }
    1.60    }
    1.61  
    1.62 -  def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
    1.63 +  def consume(message: XML.Tree, forward: Command => Unit)
    1.64 +  {
    1.65 +    accumulator ! Consume(message, forward)
    1.66 +  }
    1.67  
    1.68    def assign_state(state_id: Isar_Document.State_ID): Command =
    1.69    {
    1.70 -    val cmd = new Command(state_id, span)
    1.71 +    val cmd = new Command(state_id, span, Some(this))
    1.72      accumulator !? Assign
    1.73      cmd.state = current_state
    1.74      cmd
     2.1 --- a/src/Pure/PIDE/state.scala	Thu May 27 08:02:02 2010 +0200
     2.2 +++ b/src/Pure/PIDE/state.scala	Thu May 27 13:13:30 2010 +0200
     2.3 @@ -70,50 +70,45 @@
     2.4  
     2.5    /* message dispatch */
     2.6  
     2.7 -  def + (session: Session, message: XML.Tree): State =
     2.8 -  {
     2.9 -    val changed: State =
    2.10 -      message match {
    2.11 -        case XML.Elem(Markup.STATUS, _, elems) =>
    2.12 -          (this /: elems)((state, elem) =>
    2.13 -            elem match {
    2.14 -              case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
    2.15 -              case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
    2.16 -              case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
    2.17 -              case XML.Elem(kind, atts, body) =>
    2.18 -                atts match {
    2.19 -                  case Position.Range(begin, end) =>
    2.20 -                    if (kind == Markup.ML_TYPING) {
    2.21 -                      val info = Pretty.string_of(body, margin = 40)
    2.22 -                      state.add_markup(
    2.23 -                        command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
    2.24 +  def + (message: XML.Tree): State =
    2.25 +    message match {
    2.26 +      case XML.Elem(Markup.STATUS, _, elems) =>
    2.27 +        (this /: elems)((state, elem) =>
    2.28 +          elem match {
    2.29 +            case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
    2.30 +            case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
    2.31 +            case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
    2.32 +            case XML.Elem(kind, atts, body) =>
    2.33 +              atts match {
    2.34 +                case Position.Range(begin, end) =>
    2.35 +                  if (kind == Markup.ML_TYPING) {
    2.36 +                    val info = Pretty.string_of(body, margin = 40)
    2.37 +                    state.add_markup(
    2.38 +                      command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
    2.39 +                  }
    2.40 +                  else if (kind == Markup.ML_REF) {
    2.41 +                    body match {
    2.42 +                      case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
    2.43 +                        state.add_markup(command.markup_node(
    2.44 +                          begin - 1, end - 1,
    2.45 +                          Command.RefInfo(
    2.46 +                            Position.get_file(atts),
    2.47 +                            Position.get_line(atts),
    2.48 +                            Position.get_id(atts),
    2.49 +                            Position.get_offset(atts))))
    2.50 +                      case _ => state
    2.51                      }
    2.52 -                    else if (kind == Markup.ML_REF) {
    2.53 -                      body match {
    2.54 -                        case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
    2.55 -                          state.add_markup(command.markup_node(
    2.56 -                            begin - 1, end - 1,
    2.57 -                            Command.RefInfo(
    2.58 -                              Position.get_file(atts),
    2.59 -                              Position.get_line(atts),
    2.60 -                              Position.get_id(atts),
    2.61 -                              Position.get_offset(atts))))
    2.62 -                        case _ => state
    2.63 -                      }
    2.64 -                    }
    2.65 -                    else {
    2.66 -                      state.add_markup(
    2.67 -                        command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind)))
    2.68 -                    }
    2.69 -                  case _ => state
    2.70 -                }
    2.71 -              case _ =>
    2.72 -                System.err.println("ignored status report: " + elem)
    2.73 -                state
    2.74 -            })
    2.75 -        case _ => add_result(message)
    2.76 -      }
    2.77 -    if (!(this eq changed)) session.command_change.event(command)
    2.78 -    changed
    2.79 -  }
    2.80 +                  }
    2.81 +                  else {
    2.82 +                    state.add_markup(
    2.83 +                      command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind)))
    2.84 +                  }
    2.85 +                case _ => state
    2.86 +              }
    2.87 +            case _ =>
    2.88 +              System.err.println("ignored status report: " + elem)
    2.89 +              state
    2.90 +          })
    2.91 +      case _ => add_result(message)
    2.92 +    }
    2.93  }
     3.1 --- a/src/Pure/System/isabelle_process.scala	Thu May 27 08:02:02 2010 +0200
     3.2 +++ b/src/Pure/System/isabelle_process.scala	Thu May 27 13:13:30 2010 +0200
     3.3 @@ -161,7 +161,7 @@
     3.4      if (proc == 0) error("Cannot kill Isabelle: no process")
     3.5      else {
     3.6        try_close()
     3.7 -      Thread.sleep(500)
     3.8 +      Thread.sleep(500)  // FIXME property!?
     3.9        put_result(Kind.SIGNAL, "KILL")
    3.10        proc.destroy
    3.11        proc = null
    3.12 @@ -391,7 +391,7 @@
    3.13      new Thread("isabelle: exit") {
    3.14        override def run() = {
    3.15          val rc = proc.waitFor()
    3.16 -        Thread.sleep(300)
    3.17 +        Thread.sleep(300)  // FIXME property!?
    3.18          put_result(Kind.SYSTEM, "Exit thread terminated")
    3.19          put_result(Kind.EXIT, rc.toString)
    3.20          rm_fifo()
     4.1 --- a/src/Pure/System/isabelle_system.scala	Thu May 27 08:02:02 2010 +0200
     4.2 +++ b/src/Pure/System/isabelle_system.scala	Thu May 27 13:13:30 2010 +0200
     4.3 @@ -215,12 +215,12 @@
     4.4                catch { case _: IOException => None }
     4.5              if (pid.isDefined) {
     4.6                var running = true
     4.7 -              var count = 10
     4.8 +              var count = 10   // FIXME property!?
     4.9                while (running && count > 0) {
    4.10                  if (execute(true, "kill", "-INT", "-" + pid.get).waitFor != 0)
    4.11                    running = false
    4.12                  else {
    4.13 -                  Thread.sleep(100)
    4.14 +                  Thread.sleep(100)   // FIXME property!?
    4.15                    if (!strict) count -= 1
    4.16                  }
    4.17                }
     5.1 --- a/src/Pure/System/session.scala	Thu May 27 08:02:02 2010 +0200
     5.2 +++ b/src/Pure/System/session.scala	Thu May 27 13:13:30 2010 +0200
     5.3 @@ -25,7 +25,7 @@
     5.4    trait Entity
     5.5    {
     5.6      val id: Entity_ID
     5.7 -    def consume(session: Session, message: XML.Tree): Unit
     5.8 +    def consume(message: XML.Tree, forward: Command => Unit): Unit
     5.9    }
    5.10  }
    5.11  
    5.12 @@ -37,9 +37,7 @@
    5.13    val global_settings = new Event_Bus[Session.Global_Settings.type]
    5.14    val raw_results = new Event_Bus[Isabelle_Process.Result]
    5.15    val raw_output = new Event_Bus[Isabelle_Process.Result]
    5.16 -  val results = new Event_Bus[Command]
    5.17 -
    5.18 -  val command_change = new Event_Bus[Command]
    5.19 +  val commands_changed = new Event_Bus[Command_Set]
    5.20  
    5.21  
    5.22    /* unique ids */
    5.23 @@ -66,7 +64,7 @@
    5.24    private case object Stop
    5.25    private case class Begin_Document(path: String)
    5.26  
    5.27 -  private val session_actor = actor {
    5.28 +  private lazy val session_actor = actor {
    5.29  
    5.30      var prover: Isabelle_Process with Isar_Document = null
    5.31  
    5.32 @@ -118,7 +116,7 @@
    5.33            case None => None
    5.34            case Some(id) => lookup_entity(id)
    5.35          }
    5.36 -      if (target.isDefined) target.get.consume(this, result.message)
    5.37 +      if (target.isDefined) target.get.consume(result.message, indicate_command_change)
    5.38        else if (result.kind == Isabelle_Process.Kind.STATUS) {
    5.39          // global status message
    5.40          result.body match {
    5.41 @@ -239,6 +237,52 @@
    5.42    }
    5.43  
    5.44  
    5.45 +
    5.46 +  /** buffered command changes -- delay_first discipline **/
    5.47 +
    5.48 +  private lazy val command_change_buffer = actor {
    5.49 +    import scala.compat.Platform.currentTime
    5.50 +
    5.51 +    var changed: Set[Command] = Set()
    5.52 +    var flush_time: Option[Long] = None
    5.53 +
    5.54 +    def flush_timeout: Long =
    5.55 +      flush_time match {
    5.56 +        case None => 5000L
    5.57 +        case Some(time) => (time - currentTime) max 0
    5.58 +      }
    5.59 +
    5.60 +    def flush()
    5.61 +    {
    5.62 +      if (!changed.isEmpty) commands_changed.event(Command_Set(changed))
    5.63 +      changed = Set()
    5.64 +      flush_time = None
    5.65 +    }
    5.66 +
    5.67 +    def invoke()
    5.68 +    {
    5.69 +      val now = currentTime
    5.70 +      flush_time match {
    5.71 +        case None => flush_time = Some(now + 100)   // FIXME output_delay property
    5.72 +        case Some(time) => if (now >= time) flush()
    5.73 +      }
    5.74 +    }
    5.75 +
    5.76 +    loop {
    5.77 +      reactWithin(flush_timeout) {
    5.78 +        case command: Command => changed += command; invoke()
    5.79 +        case TIMEOUT => flush()
    5.80 +        case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
    5.81 +      }
    5.82 +    }
    5.83 +  }
    5.84 +
    5.85 +  def indicate_command_change(command: Command)
    5.86 +  {
    5.87 +    command_change_buffer ! command
    5.88 +  }
    5.89 +
    5.90 +
    5.91    /* main methods */
    5.92  
    5.93    def start(timeout: Int, args: List[String]): Option[String] =
     6.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Thu May 27 08:02:02 2010 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Thu May 27 13:13:30 2010 +0200
     6.3 @@ -95,7 +95,7 @@
     6.4  
     6.5    private val edits_buffer = new mutable.ListBuffer[Text_Edit]   // owned by Swing thread
     6.6  
     6.7 -  private val edits_delay = Swing_Thread.delay_last(300) {
     6.8 +  private val edits_delay = Swing_Thread.delay_last(300) {  // FIXME input_delay property
     6.9      if (!edits_buffer.isEmpty) {
    6.10        val new_change = current_change().edit(session, edits_buffer.toList)
    6.11        edits_buffer.clear
     7.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Thu May 27 08:02:02 2010 +0200
     7.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Thu May 27 13:13:30 2010 +0200
     7.3 @@ -69,7 +69,7 @@
     7.4  }
     7.5  
     7.6  
     7.7 -class Document_View(model: Document_Model, text_area: TextArea)
     7.8 +class Document_View(val model: Document_Model, text_area: TextArea)
     7.9  {
    7.10    private val session = model.session
    7.11  
    7.12 @@ -79,38 +79,22 @@
    7.13    @volatile private var document = model.recent_document()
    7.14  
    7.15  
    7.16 -  /* buffer of changed commands -- owned by Swing thread */
    7.17 -
    7.18 -  @volatile private var changed_commands: Set[Command] = Set()
    7.19 +  /* commands_changed_actor */
    7.20  
    7.21 -  private val changed_delay = Swing_Thread.delay_first(100) {
    7.22 -    if (!changed_commands.isEmpty) {
    7.23 -      document = model.recent_document()
    7.24 -      for (cmd <- changed_commands if document.commands.contains(cmd)) { // FIXME cover doc states as well!!?
    7.25 -        update_syntax(cmd)
    7.26 -        invalidate_line(cmd)
    7.27 -        overview.repaint()
    7.28 -      }
    7.29 -      changed_commands = Set()
    7.30 -    }
    7.31 -  }
    7.32 -
    7.33 -
    7.34 -  /* command change actor */
    7.35 -
    7.36 -  private case object Exit
    7.37 -
    7.38 -  private val command_change_actor = actor {
    7.39 +  private val commands_changed_actor = actor {
    7.40      loop {
    7.41        react {
    7.42 -        case command: Command =>  // FIXME rough filtering according to document family!?
    7.43 +        case Command_Set(changed) =>
    7.44            Swing_Thread.now {
    7.45 -            changed_commands += command
    7.46 -            changed_delay()
    7.47 +            document = model.recent_document()
    7.48 +            // FIXME cover doc states as well!!?
    7.49 +            for (command <- changed if document.commands.contains(command)) {
    7.50 +              update_syntax(command)
    7.51 +              invalidate_line(command)
    7.52 +              overview.repaint()
    7.53 +            }
    7.54            }
    7.55  
    7.56 -        case Exit => reply(()); exit()
    7.57 -
    7.58          case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
    7.59        }
    7.60      }
    7.61 @@ -153,24 +137,23 @@
    7.62    }
    7.63  
    7.64  
    7.65 -  /* caret_listener */
    7.66 +  /* caret handling */
    7.67  
    7.68 -  private var _selected_command: Command = null
    7.69 -  private def selected_command = _selected_command
    7.70 -  private def selected_command_=(cmd: Command)
    7.71 -  {
    7.72 -    _selected_command = cmd
    7.73 -    session.results.event(cmd)
    7.74 -  }
    7.75 +  def selected_command: Option[Command] =
    7.76 +    document.command_at(text_area.getCaretPosition) match {
    7.77 +      case Some((command, _)) => Some(command)
    7.78 +      case None => None
    7.79 +    }
    7.80  
    7.81    private val caret_listener = new CaretListener
    7.82    {
    7.83 +    private var last_selected_command: Option[Command] = None
    7.84      override def caretUpdate(e: CaretEvent)
    7.85      {
    7.86 -      document.command_at(e.getDot) match {
    7.87 -        case Some((command, command_start)) if (selected_command != command) =>
    7.88 -          selected_command = command
    7.89 -        case _ =>
    7.90 +      val selected = selected_command
    7.91 +      if (selected != last_selected_command) {
    7.92 +        last_selected_command = selected
    7.93 +        if (selected.isDefined) session.indicate_command_change(selected.get)
    7.94        }
    7.95      }
    7.96    }
    7.97 @@ -179,6 +162,7 @@
    7.98    /* (re)painting */
    7.99  
   7.100    private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() }
   7.101 +  // FIXME update_delay property
   7.102  
   7.103    private def update_syntax(cmd: Command)
   7.104    {
   7.105 @@ -192,9 +176,6 @@
   7.106    {
   7.107      val (start, stop) = model.lines_of_command(document, cmd)
   7.108      text_area.invalidateLineRange(start, stop)
   7.109 -
   7.110 -    if (selected_command == cmd)
   7.111 -      session.results.event(cmd)
   7.112    }
   7.113  
   7.114    private def invalidate_all() =
   7.115 @@ -289,13 +270,12 @@
   7.116        addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
   7.117      text_area.addCaretListener(caret_listener)
   7.118      text_area.addLeftOfScrollBar(overview)
   7.119 -    session.command_change += command_change_actor
   7.120 +    session.commands_changed += commands_changed_actor
   7.121    }
   7.122  
   7.123    private def deactivate()
   7.124    {
   7.125 -    session.command_change -= command_change_actor
   7.126 -    command_change_actor !? Exit
   7.127 +    session.commands_changed -= commands_changed_actor
   7.128      text_area.removeLeftOfScrollBar(overview)
   7.129      text_area.removeCaretListener(caret_listener)
   7.130      text_area.getPainter.removeExtension(text_area_extension)
     8.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 27 08:02:02 2010 +0200
     8.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 27 13:13:30 2010 +0200
     8.3 @@ -22,74 +22,61 @@
     8.4  
     8.5  class Output_Dockable(view: View, position: String) extends Dockable(view, position)
     8.6  {
     8.7 +  Swing_Thread.assert()
     8.8 +
     8.9    val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()))
    8.10    add(html_panel, BorderLayout.CENTER)
    8.11  
    8.12  
    8.13 -  /* controls */
    8.14 -
    8.15 -  private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
    8.16 -  zoom.tooltip = "Zoom factor for basic font size"
    8.17 -
    8.18 -  private val update = new Button("Update") {
    8.19 -    reactions += { case ButtonClicked(_) => handle_update() }
    8.20 -  }
    8.21 -  update.tooltip =
    8.22 -    "<html>Update display according to the<br>state of command at caret position</html>"
    8.23 -
    8.24 -  private val tracing = new CheckBox("Tracing") {
    8.25 -    reactions += { case ButtonClicked(_) => handle_update() }
    8.26 -  }
    8.27 -  tracing.tooltip =
    8.28 -    "<html>Indicate output of tracing messages<br>(also needs to be enabled on the prover side)</html>"
    8.29 +  /* component state -- owned by Swing thread */
    8.30  
    8.31 -  private val debug = new CheckBox("Debug") {
    8.32 -    reactions += { case ButtonClicked(_) => handle_update() }
    8.33 -  }
    8.34 -  debug.tooltip =
    8.35 -    "<html>Indicate output of debug messages<br>(also needs to be enabled on the prover side)</html>"
    8.36 +  private var zoom_factor = 100
    8.37 +  private var show_debug = false
    8.38 +  private var show_tracing = false
    8.39 +  private var follow_caret = true
    8.40 +  private var current_command: Option[Command] = None
    8.41  
    8.42 -  private val follow = new CheckBox("Follow")
    8.43 -  follow.selected = true
    8.44 -  follow.tooltip =
    8.45 -    "<html>Indicate automatic update following<br>caret movement or state changes</html>"
    8.46  
    8.47 -  private def filtered_results(document: Document, cmd: Command): List[XML.Tree] =
    8.48 +  private def handle_resize()
    8.49    {
    8.50 -    val show_tracing = tracing.selected
    8.51 -    val show_debug = debug.selected
    8.52 -    document.current_state(cmd).results filter {
    8.53 -      case XML.Elem(Markup.TRACING, _, _) => show_tracing
    8.54 -      case XML.Elem(Markup.DEBUG, _, _) => show_debug
    8.55 -      case _ => true
    8.56 +    Swing_Thread.now {
    8.57 +      html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100))
    8.58      }
    8.59    }
    8.60  
    8.61 -  private case class Render(body: List[XML.Tree])
    8.62 +  private def handle_caret()
    8.63 +  {
    8.64 +    Swing_Thread.now {
    8.65 +      Document_View(view.getTextArea) match {
    8.66 +        case Some(doc_view) => current_command = doc_view.selected_command
    8.67 +        case None =>
    8.68 +      }
    8.69 +    }
    8.70 +  }
    8.71  
    8.72 -  private def handle_update()
    8.73 +  private def handle_update(restriction: Option[Set[Command]] = None)
    8.74    {
    8.75      Swing_Thread.now {
    8.76 -      Document_Model(view.getBuffer) match {
    8.77 -        case Some(model) =>
    8.78 -          val document = model.recent_document
    8.79 -          document.command_at(view.getTextArea.getCaretPosition) match {
    8.80 -            case Some((cmd, _)) =>
    8.81 -              main_actor ! Render(filtered_results(document, cmd))
    8.82 -            case None =>
    8.83 +      if (follow_caret) handle_caret()
    8.84 +      Document_View(view.getTextArea) match {
    8.85 +        case Some(doc_view) =>
    8.86 +          current_command match {
    8.87 +            case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
    8.88 +              val document = doc_view.model.recent_document
    8.89 +              val filtered_results =
    8.90 +                document.current_state(cmd).results filter {
    8.91 +                  case XML.Elem(Markup.TRACING, _, _) => show_tracing
    8.92 +                  case XML.Elem(Markup.DEBUG, _, _) => show_debug
    8.93 +                  case _ => true
    8.94 +                }
    8.95 +              html_panel.render(filtered_results)
    8.96 +            case _ =>
    8.97            }
    8.98          case None =>
    8.99        }
   8.100      }
   8.101    }
   8.102  
   8.103 -  private var zoom_factor = 100
   8.104 -
   8.105 -  private def handle_resize() =
   8.106 -    Swing_Thread.now {
   8.107 -      html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100))
   8.108 -    }
   8.109 -
   8.110  
   8.111    /* main actor */
   8.112  
   8.113 @@ -97,17 +84,7 @@
   8.114      loop {
   8.115        react {
   8.116          case Session.Global_Settings => handle_resize()
   8.117 -        case Render(body) => html_panel.render(body)
   8.118 -
   8.119 -        case cmd: Command =>
   8.120 -          Swing_Thread.now {
   8.121 -            if (follow.selected) Document_Model(view.getBuffer) else None
   8.122 -          } match {
   8.123 -            case None =>
   8.124 -            case Some(model) =>
   8.125 -              html_panel.render(filtered_results(model.recent_document, cmd))
   8.126 -          }
   8.127 -
   8.128 +        case Command_Set(changed) => handle_update(Some(changed))
   8.129          case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
   8.130        }
   8.131      }
   8.132 @@ -115,13 +92,13 @@
   8.133  
   8.134    override def init()
   8.135    {
   8.136 -    Isabelle.session.results += main_actor
   8.137 +    Isabelle.session.commands_changed += main_actor
   8.138      Isabelle.session.global_settings += main_actor
   8.139    }
   8.140  
   8.141    override def exit()
   8.142    {
   8.143 -    Isabelle.session.results -= main_actor
   8.144 +    Isabelle.session.commands_changed -= main_actor
   8.145      Isabelle.session.global_settings -= main_actor
   8.146    }
   8.147  
   8.148 @@ -129,14 +106,42 @@
   8.149    /* resize */
   8.150  
   8.151    addComponentListener(new ComponentAdapter {
   8.152 -    val delay = Swing_Thread.delay_last(500) { handle_resize() }
   8.153 +    val delay = Swing_Thread.delay_last(500) { handle_resize() }  // FIXME update_delay property
   8.154      override def componentResized(e: ComponentEvent) { delay() }
   8.155    })
   8.156  
   8.157  
   8.158 -  /* init controls */
   8.159 +  /* controls */
   8.160 +
   8.161 +  private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
   8.162 +  zoom.tooltip = "Zoom factor for basic font size"
   8.163 +
   8.164 +  private val debug = new CheckBox("Debug") {
   8.165 +    reactions += { case ButtonClicked(_) => show_debug = this.selected; handle_update() }
   8.166 +  }
   8.167 +  debug.selected = show_debug
   8.168 +  debug.tooltip =
   8.169 +    "<html>Indicate output of debug messages<br>(also needs to be enabled on the prover side)</html>"
   8.170  
   8.171 -  val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, update, debug, tracing, follow)
   8.172 +  private val tracing = new CheckBox("Tracing") {
   8.173 +    reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
   8.174 +  }
   8.175 +  tracing.selected = show_tracing
   8.176 +  tracing.tooltip =
   8.177 +    "<html>Indicate output of tracing messages<br>(also needs to be enabled on the prover side)</html>"
   8.178 +
   8.179 +  private val auto_update = new CheckBox("Auto update") {
   8.180 +    reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
   8.181 +  }
   8.182 +  auto_update.selected = follow_caret
   8.183 +  auto_update.tooltip = "<html>Indicate automatic update following cursor movement</html>"
   8.184 +
   8.185 +  private val update = new Button("Update") {
   8.186 +    reactions += { case ButtonClicked(_) => handle_caret(); handle_update() }
   8.187 +  }
   8.188 +  update.tooltip = "<html>Update display according to the command at cursor position</html>"
   8.189 +
   8.190 +  val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update)
   8.191    add(controls.peer, BorderLayout.NORTH)
   8.192  
   8.193    handle_update()