# HG changeset patch # User wenzelm # Date 1440444257 -7200 # Node ID 0be2726382d9a34c23ea7d63b06746e663da87cd # Parent 6890d5875bc7d09ac52a3c6bc10f0c4ec96e9115# Parent 7ce030f14aa935281fd6ecb857dcd870a688be29 merged diff -r 6890d5875bc7 -r 0be2726382d9 src/Pure/Tools/debugger.scala --- a/src/Pure/Tools/debugger.scala Mon Aug 24 16:25:40 2015 +0200 +++ b/src/Pure/Tools/debugger.scala Mon Aug 24 21:24:17 2015 +0200 @@ -7,6 +7,9 @@ package isabelle +import scala.collection.immutable.SortedMap + + object Debugger { /* context */ @@ -28,12 +31,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 { @@ -45,13 +49,15 @@ /* global state */ + type Threads = SortedMap[String, List[Debug_State]] + sealed case class State( session: Session = new Session(Resources.empty), // implicit session 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 + threads: Threads = SortedMap.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,15 +77,24 @@ (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) - else copy(threads = threads + (thread_name -> debug_states)) + { + val threads1 = + if (debug_states.nonEmpty) threads + (thread_name -> debug_states) + else threads - thread_name + val focus1 = + focus.get(thread_name) match { + case Some(c) if debug_states.nonEmpty => + focus + (thread_name -> Context(thread_name, debug_states)) + case _ => focus - thread_name + } + copy(threads = threads1, focus = focus1) + } + + 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,18 +237,29 @@ }) } - def focus(): Option[Position.T] = global_state.value.focus + def status(focus: Option[Context]): (Threads, List[XML.Tree]) = + { + val state = global_state.value + val output = + focus match { + case None => Nil + case Some(c) => + (for { + (thread_name, results) <- state.output + if thread_name == c.thread_name + (_, tree) <- results.iterator + } yield tree).toList + } + (state.threads, output) + } - 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 = global_state.value.session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*) @@ -251,7 +277,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 +286,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 6890d5875bc7 -r 0be2726382d9 src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Mon Aug 24 16:25:40 2015 +0200 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Mon Aug 24 21:24:17 2015 +0200 @@ -16,6 +16,7 @@ import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel} import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener} +import scala.collection.immutable.SortedMap import scala.swing.{Button, Label, Component, ScrollPane, SplitPane, Orientation, CheckBox, BorderPanel} import scala.swing.event.ButtonClicked @@ -70,7 +71,7 @@ /* component state -- owned by GUI thread */ private var current_snapshot = Document.Snapshot.init - private var current_threads: Map[String, List[Debugger.Debug_State]] = Map.empty + private var current_threads: Debugger.Threads = SortedMap.empty private var current_output: List[XML.Tree] = Nil @@ -93,24 +94,10 @@ GUI_Thread.require {} val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot) - val new_threads = Debugger.threads() - val new_output = - { - val output = Debugger.output() - val current_thread_selection = thread_selection() - (for { - (thread_name, results) <- output - if current_thread_selection.isEmpty || current_thread_selection.get == thread_name - (_, tree) <- results.iterator - } yield tree).toList - } + val (new_threads, new_output) = Debugger.status(tree_selection()) - if (new_threads != current_threads) { - val threads = - (for ((a, b) <- new_threads.iterator) - yield Debugger.Context(a, b)).toList.sortBy(_.thread_name) - update_tree(threads) - } + if (new_threads != current_threads) + update_tree(new_threads) if (new_output != current_output) pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output)) @@ -141,27 +128,24 @@ 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]) + private def update_tree(threads: Debugger.Threads) { - require(threads.forall(_.index == 0)) + val thread_contexts = + (for ((a, b) <- threads.iterator) + yield Debugger.Context(a, b)).toList val new_tree_selection = tree_selection() match { - case Some(c) if threads.contains(c) => Some(c) - case Some(c) if threads.exists(t => c.thread_name == t.thread_name) => Some(c.reset) - case _ => threads.headOption + case Some(c) if thread_contexts.contains(c) => Some(c) + case Some(c) if thread_contexts.exists(t => c.thread_name == t.thread_name) => + Some(c.reset) + case _ => thread_contexts.headOption } tree.clearSelection root.removeAllChildren - for (thread <- threads) { + for (thread <- thread_contexts) { val thread_node = new DefaultMutableTreeNode(thread) for ((debug_state, i) <- thread.debug_states.zipWithIndex) thread_node.add(new DefaultMutableTreeNode(thread.select(i))) @@ -176,7 +160,7 @@ new_tree_selection match { case Some(c) => val i = - (for (t <- threads.iterator.takeWhile(t => c.thread_name != t.thread_name)) + (for (t <- thread_contexts.iterator.takeWhile(t => c.thread_name != t.thread_name)) yield t.size).sum tree.addSelectionRow(i + c.index + 1) case None => @@ -199,7 +183,7 @@ tree.addTreeSelectionListener( new TreeSelectionListener { override def valueChanged(e: TreeSelectionEvent) { - update_focus(focus_selection()) + update_focus() update_vals() } }) @@ -209,7 +193,7 @@ { val click = tree.getPathForLocation(e.getX, e.getY) if (click != null && e.getClickCount == 1) - update_focus(focus_selection()) + update_focus() } }) @@ -292,7 +276,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 +303,19 @@ 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) + } + JEdit_Lib.jedit_text_areas(view.getBuffer).foreach(_.repaint()) } @@ -370,7 +357,6 @@ PIDE.session.global_options -= main PIDE.session.debugger_updates -= main delay_resize.revoke() - update_focus(None) Debugger.exit() jEdit.propertiesChanged() } diff -r 6890d5875bc7 -r 0be2726382d9 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Mon Aug 24 16:25:40 2015 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Aug 24 21:24:17 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().iterator + pos <- c.debug_position.iterator + } yield pos).toList + 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,