follow debugger focus;
authorwenzelm
Mon Aug 10 14:14:49 2015 +0200 (2015-08-10)
changeset 60875ee23c1d21ac3
parent 60874 7865e03a7fc1
child 60876 52edced9cce5
follow debugger focus;
src/Pure/Tools/debugger.scala
src/Tools/jEdit/src/debugger_dockable.scala
     1.1 --- a/src/Pure/Tools/debugger.scala	Mon Aug 10 14:13:49 2015 +0200
     1.2 +++ b/src/Pure/Tools/debugger.scala	Mon Aug 10 14:14:49 2015 +0200
     1.3 @@ -17,12 +17,16 @@
     1.4  
     1.5    sealed case class State(
     1.6      session: Session = new Session(Resources.empty),
     1.7 +    focus: Option[Position.T] = None,  // position of active GUI component
     1.8      threads: Map[String, List[Debug_State]] = Map.empty,  // thread name ~> stack of debug states
     1.9      output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
    1.10    {
    1.11      def set_session(new_session: Session): State =
    1.12        copy(session = new_session)
    1.13  
    1.14 +    def set_focus(new_focus: Option[Position.T]): State =
    1.15 +      copy(focus = new_focus)
    1.16 +
    1.17      def get_thread(thread_name: String): List[Debug_State] =
    1.18        threads.getOrElse(thread_name, Nil)
    1.19  
    1.20 @@ -120,6 +124,9 @@
    1.21      current_state().session.protocol_command("Debugger.init")
    1.22    }
    1.23  
    1.24 +  def focus(new_focus: Option[Position.T]): Boolean =
    1.25 +    global_state.change_result(state => (state.focus != new_focus, state.set_focus(new_focus)))
    1.26 +
    1.27    def cancel(thread_name: String): Unit =
    1.28      current_state().session.protocol_command("Debugger.cancel", thread_name)
    1.29  
     2.1 --- a/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 14:13:49 2015 +0200
     2.2 +++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 14:14:49 2015 +0200
     2.3 @@ -10,7 +10,8 @@
     2.4  import isabelle._
     2.5  
     2.6  import java.awt.{BorderLayout, Dimension}
     2.7 -import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, MouseEvent, MouseAdapter}
     2.8 +import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, MouseEvent, MouseAdapter,
     2.9 +  FocusAdapter, FocusEvent}
    2.10  import javax.swing.{JTree, JScrollPane}
    2.11  import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel}
    2.12  import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
    2.13 @@ -18,7 +19,7 @@
    2.14  import scala.swing.{Button, Label, Component, SplitPane, Orientation, CheckBox}
    2.15  import scala.swing.event.ButtonClicked
    2.16  
    2.17 -import org.gjt.sp.jedit.View
    2.18 +import org.gjt.sp.jedit.{jEdit, View}
    2.19  
    2.20  
    2.21  object Debugger_Dockable
    2.22 @@ -117,6 +118,14 @@
    2.23  
    2.24    def thread_selection(): Option[String] = tree_selection().map(sel => sel._1.thread_name)
    2.25  
    2.26 +  def focus_selection(): Option[Position.T] =
    2.27 +    tree_selection() match {
    2.28 +      case Some((t, opt_index)) =>
    2.29 +        val i = opt_index getOrElse 0
    2.30 +        if (i < t.debug_states.length) Some(t.debug_states(i).pos) else None
    2.31 +      case _ => None
    2.32 +    }
    2.33 +
    2.34    private def update_tree(thread_entries: List[Debugger_Dockable.Thread_Entry])
    2.35    {
    2.36      val old_thread_selection = thread_selection()
    2.37 @@ -149,10 +158,10 @@
    2.38      tree.revalidate()
    2.39    }
    2.40  
    2.41 -  private def action(node: DefaultMutableTreeNode)
    2.42 -  {
    2.43 -    handle_update()
    2.44 -  }
    2.45 +  tree.addTreeSelectionListener(
    2.46 +    new TreeSelectionListener {
    2.47 +      override def valueChanged(e: TreeSelectionEvent) { update_focus(focus_selection()) }
    2.48 +    })
    2.49  
    2.50    tree.addMouseListener(new MouseAdapter {
    2.51      override def mouseClicked(e: MouseEvent)
    2.52 @@ -161,7 +170,7 @@
    2.53        if (click != null && e.getClickCount == 1) {
    2.54          (click.getLastPathComponent, tree.getLastSelectedPathComponent) match {
    2.55            case (node: DefaultMutableTreeNode, node1: DefaultMutableTreeNode) if node == node1 =>
    2.56 -            action(node)
    2.57 +            handle_update()
    2.58            case _ =>
    2.59          }
    2.60        }
    2.61 @@ -212,7 +221,6 @@
    2.62        tooltip = "Evaluate ML expression within optional context"
    2.63        reactions += { case ButtonClicked(_) => eval_expression() }
    2.64      }
    2.65 -  override def focusOnDefaultComponent { eval_button.requestFocus }
    2.66  
    2.67    private def eval_expression()
    2.68    {
    2.69 @@ -270,6 +278,22 @@
    2.70    add(controls.peer, BorderLayout.NORTH)
    2.71  
    2.72  
    2.73 +  /* focus */
    2.74 +
    2.75 +  override def focusOnDefaultComponent { eval_button.requestFocus }
    2.76 +
    2.77 +  addFocusListener(new FocusAdapter {
    2.78 +    override def focusGained(e: FocusEvent) { update_focus(focus_selection()) }
    2.79 +    override def focusLost(e: FocusEvent) { update_focus(None) }
    2.80 +  })
    2.81 +
    2.82 +  private def update_focus(focus: Option[Position.T])
    2.83 +  {
    2.84 +    if (Debugger.focus(focus) && focus.isDefined)
    2.85 +      PIDE.editor.hyperlink_position(current_snapshot, focus.get).foreach(_.follow(view))
    2.86 +  }
    2.87 +
    2.88 +
    2.89    /* main panel */
    2.90  
    2.91    val main_panel = new SplitPane(Orientation.Vertical) {
    2.92 @@ -309,6 +333,7 @@
    2.93      PIDE.session.global_options -= main
    2.94      PIDE.session.debugger_updates -= main
    2.95      delay_resize.revoke()
    2.96 +    update_focus(None)
    2.97    }
    2.98  
    2.99