# HG changeset patch # User wenzelm # Date 1440409085 -7200 # Node ID 39f67bb4e609bcc6c372a1442054ff54779a3c97 # Parent 018b0c996b543b614ba255f1ed4643694ec332ef maintain per-thread focus context; tuned signature; diff -r 018b0c996b54 -r 39f67bb4e609 src/Pure/Tools/debugger.scala --- a/src/Pure/Tools/debugger.scala Mon Aug 24 00:20:20 2015 +0200 +++ b/src/Pure/Tools/debugger.scala Mon Aug 24 11:38:05 2015 +0200 @@ -28,12 +28,13 @@ Some(debug_states(index - 1)) else None - def debug_state_index: Option[Int] = + def debug_index: Option[Int] = if (stack_state.isDefined) Some(index - 1) else if (debug_states.nonEmpty) Some(0) else None def debug_state: Option[Debug_State] = stack_state orElse thread_state + def debug_position: Option[Position.T] = debug_state.map(_.pos) override def toString: String = stack_state match { @@ -50,8 +51,8 @@ active: Int = 0, // active views break: Boolean = false, // break at next possible breakpoint active_breakpoints: Set[Long] = Set.empty, // explicit breakpoint state - focus: Option[Position.T] = None, // position of active GUI component threads: Map[String, List[Debug_State]] = Map.empty, // thread name ~> stack of debug states + focus: Map[String, Context] = Map.empty, // thread name ~> focus output: Map[String, Command.Results] = Map.empty) // thread name ~> output messages { def set_session(new_session: Session): State = @@ -71,16 +72,15 @@ (active_breakpoints1(breakpoint), copy(active_breakpoints = active_breakpoints1)) } - def set_focus(new_focus: Option[Position.T]): State = - copy(focus = new_focus) - def get_thread(thread_name: String): List[Debug_State] = threads.getOrElse(thread_name, Nil) def update_thread(thread_name: String, debug_states: List[Debug_State]): State = - if (debug_states.isEmpty) copy(threads = threads - thread_name) + if (debug_states.isEmpty) copy(threads = threads - thread_name, focus = focus - thread_name) else copy(threads = threads + (thread_name -> debug_states)) + def set_focus(c: Context): State = copy(focus = focus + (c.thread_name -> c)) + def get_output(thread_name: String): Command.Results = output.getOrElse(thread_name, Command.Results.empty) @@ -222,16 +222,15 @@ }) } - def focus(): Option[Position.T] = global_state.value.focus + def threads(): Map[String, List[Debug_State]] = global_state.value.threads - def set_focus(focus: Option[Position.T]) + def focus(): List[Context] = global_state.value.focus.toList.map(_._2) + def set_focus(c: Context) { - global_state.change(_.set_focus(focus)) + global_state.change(_.set_focus(c)) delay_update.invoke() } - def threads(): Map[String, List[Debug_State]] = global_state.value.threads - def output(): Map[String, Command.Results] = global_state.value.output def input(thread_name: String, msg: String*): Unit = @@ -251,7 +250,7 @@ def eval(c: Context, SML: Boolean, context: String, expression: String) { global_state.change(state => { - input(c.thread_name, "eval", c.debug_state_index.getOrElse(0).toString, + input(c.thread_name, "eval", c.debug_index.getOrElse(0).toString, SML.toString, Symbol.encode(context), Symbol.encode(expression)) state.clear_output(c.thread_name) }) @@ -260,10 +259,10 @@ def print_vals(c: Context, SML: Boolean, context: String) { - require(c.debug_state_index.isDefined) + require(c.debug_index.isDefined) global_state.change(state => { - input(c.thread_name, "print_vals", c.debug_state_index.getOrElse(0).toString, + input(c.thread_name, "print_vals", c.debug_index.getOrElse(0).toString, SML.toString, Symbol.encode(context)) state.clear_output(c.thread_name) }) diff -r 018b0c996b54 -r 39f67bb4e609 src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Mon Aug 24 00:20:20 2015 +0200 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Mon Aug 24 11:38:05 2015 +0200 @@ -141,12 +141,6 @@ def thread_selection(): Option[String] = tree_selection().map(_.thread_name) - def focus_selection(): Option[Position.T] = - for { - c <- tree_selection() - d <- c.debug_state - } yield d.pos - private def update_tree(threads: List[Debugger.Context]) { require(threads.forall(_.index == 0)) @@ -199,7 +193,7 @@ tree.addTreeSelectionListener( new TreeSelectionListener { override def valueChanged(e: TreeSelectionEvent) { - update_focus(focus_selection()) + update_focus() update_vals() } }) @@ -209,7 +203,7 @@ { val click = tree.getPathForLocation(e.getX, e.getY) if (click != null && e.getClickCount == 1) - update_focus(focus_selection()) + update_focus() } }) @@ -292,7 +286,7 @@ context_field.addCurrentToHistory() expression_field.addCurrentToHistory() tree_selection() match { - case Some(c) if c.debug_state_index.isDefined => + case Some(c) if c.debug_index.isDefined => Debugger.eval(c, sml_button.selected, context_field.getText, expression_field.getText) case _ => } @@ -319,16 +313,21 @@ override def focusOnDefaultComponent { eval_button.requestFocus } addFocusListener(new FocusAdapter { - override def focusGained(e: FocusEvent) { update_focus(focus_selection()) } - override def focusLost(e: FocusEvent) { update_focus(None) } + override def focusGained(e: FocusEvent) { update_focus() } }) - private def update_focus(focus: Option[Position.T]) + private def update_focus() { - Debugger.set_focus(focus) - if (focus.isDefined) - PIDE.editor.hyperlink_position(false, current_snapshot, focus.get).foreach(_.follow(view)) - view.getTextArea.repaint() + for (c <- tree_selection()) { + Debugger.set_focus(c) + for { + pos <- c.debug_position + link <- PIDE.editor.hyperlink_position(false, current_snapshot, pos) + } { + link.follow(view) + view.getTextArea.repaint() + } + } } @@ -370,7 +369,6 @@ PIDE.session.global_options -= main PIDE.session.debugger_updates -= main delay_resize.revoke() - update_focus(None) Debugger.exit() jEdit.propertiesChanged() } diff -r 018b0c996b54 -r 39f67bb4e609 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Mon Aug 24 00:20:20 2015 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Aug 24 11:38:05 2015 +0200 @@ -352,10 +352,16 @@ private def caret_color(rendering: Rendering, offset: Text.Offset): Color = { if (text_area.isCaretVisible) text_area.getPainter.getCaretColor - else - if (Debugger.focus().exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _))) + else { + val debug_positions = + for { + c <- Debugger.focus() + pos <- c.debug_position + } yield pos + if (debug_positions.exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _))) rendering.caret_debugger_color else rendering.caret_invisible_color + } } private def paint_chunk_list(rendering: Rendering,