# HG changeset patch # User wenzelm # Date 1440362821 -7200 # Node ID cccfd7f6317d72186cf08797ddec84c3558fa32a # Parent a9574cdd5eafc3aa4fcc8e55d34d0704bb40d52c more explicit type Debugger.Context; diff -r a9574cdd5eaf -r cccfd7f6317d src/Pure/Tools/debugger.scala --- a/src/Pure/Tools/debugger.scala Sun Aug 23 13:25:20 2015 +0200 +++ b/src/Pure/Tools/debugger.scala Sun Aug 23 22:47:01 2015 +0200 @@ -9,12 +9,42 @@ object Debugger { - /* global state */ + /* context */ sealed case class Debug_State( pos: Position.T, function: String) + sealed case class Context(thread_name: String, debug_states: List[Debug_State], index: Int = 0) + { + def size: Int = debug_states.length + 1 + def reset: Context = copy(index = 0) + def select(i: Int) = copy(index = i + 1) + + def thread_state: Option[Debug_State] = debug_states.headOption + + def stack_state: Option[Debug_State] = + if (1 <= index && index <= debug_states.length) + Some(debug_states(index - 1)) + else None + + def debug_state_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 + + override def toString: String = + stack_state match { + case None => thread_name + case Some(d) => d.function + } + } + + + /* global state */ + sealed case class State( session: Session = new Session(Resources.empty), // implicit session active: Int = 0, // active views @@ -216,21 +246,24 @@ delay_update.invoke() } - def eval(thread_name: String, index: Int, SML: Boolean, context: String, expression: String) + def eval(c: Context, SML: Boolean, context: String, expression: String) { global_state.change(state => { - input(thread_name, "eval", - index.toString, SML.toString, Symbol.encode(context), Symbol.encode(expression)) - state.clear_output(thread_name) + input(c.thread_name, "eval", c.debug_state_index.getOrElse(0).toString, + SML.toString, Symbol.encode(context), Symbol.encode(expression)) + state.clear_output(c.thread_name) }) delay_update.invoke() } - def print_vals(thread_name: String, index: Int, SML: Boolean, context: String) + def print_vals(c: Context, SML: Boolean, context: String) { + require(c.debug_state_index.isDefined) + global_state.change(state => { - input(thread_name, "print_vals", index.toString, SML.toString, Symbol.encode(context)) - state.clear_output(thread_name) + input(c.thread_name, "print_vals", c.debug_state_index.getOrElse(0).toString, + SML.toString, Symbol.encode(context)) + state.clear_output(c.thread_name) }) delay_update.invoke() } diff -r a9574cdd5eaf -r cccfd7f6317d src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Sun Aug 23 13:25:20 2015 +0200 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Sun Aug 23 22:47:01 2015 +0200 @@ -27,19 +27,6 @@ object Debugger_Dockable { - /* state entries */ - - sealed case class Thread_Entry(thread_name: String, debug_states: List[Debugger.Debug_State]) - { - override def toString: String = thread_name - } - - sealed case class Stack_Entry(debug_state: Debugger.Debug_State, index: Int) - { - override def toString: String = debug_state.function - } - - /* breakpoints */ def toggle_breakpoint(command: Command, breakpoint: Long) @@ -119,10 +106,10 @@ } if (new_threads != current_threads) { - val thread_entries = + val threads = (for ((a, b) <- new_threads.iterator) - yield Debugger_Dockable.Thread_Entry(a, b)).toList.sortBy(_.thread_name) - update_tree(thread_entries) + yield Debugger.Context(a, b)).toList.sortBy(_.thread_name) + update_tree(threads) } if (new_output != current_output) @@ -142,56 +129,42 @@ tree.setRowHeight(0) tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION) - def tree_selection(): Option[(Debugger_Dockable.Thread_Entry, Option[Int])] = - tree.getSelectionPath match { - case null => None - case path => - path.getPath.toList.map(n => n.asInstanceOf[DefaultMutableTreeNode].getUserObject) match { - case List(_, t: Debugger_Dockable.Thread_Entry) => - Some((t, None)) - case List(_, t: Debugger_Dockable.Thread_Entry, s: Debugger_Dockable.Stack_Entry) => - Some((t, Some(s.index))) + def tree_selection(): Option[Debugger.Context] = + tree.getLastSelectedPathComponent match { + case node: DefaultMutableTreeNode => + node.getUserObject match { + case c: Debugger.Context => Some(c) case _ => None } - } - - def thread_selection(): Option[String] = tree_selection().map(sel => sel._1.thread_name) - - def focus_selection(): Option[Position.T] = - tree_selection() match { - case Some((t, opt_index)) => - val i = opt_index getOrElse 0 - if (i < t.debug_states.length) Some(t.debug_states(i).pos) else None case _ => None } - private def update_tree(thread_entries: List[Debugger_Dockable.Thread_Entry]) + 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]) { - val new_tree_selection: Option[(String, Int)] = + require(threads.forall(_.index == 0)) + + val new_tree_selection = tree_selection() match { - case Some((t, opt_index)) - if thread_entries.exists(t1 => - t.thread_name == t1.thread_name && - (opt_index.isEmpty || opt_index.get < t1.debug_states.length)) => - val j = opt_index match { case None => 0 case Some(i) => i + 1 } - Some((t.thread_name, j)) - case _ => - thread_entries match { - case t :: _ => Some((t.thread_name, 0)) - case Nil => None - } + 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 } tree.clearSelection root.removeAllChildren - for (thread_entry <- thread_entries) { - val thread_node = new DefaultMutableTreeNode(thread_entry) - for ((debug_state, i) <- thread_entry.debug_states.zipWithIndex) { - val stack_node = - new DefaultMutableTreeNode(Debugger_Dockable.Stack_Entry(debug_state, i)) - thread_node.add(stack_node) - } + for (thread <- threads) { + val thread_node = new DefaultMutableTreeNode(thread) + for ((debug_state, i) <- thread.debug_states.zipWithIndex) + thread_node.add(new DefaultMutableTreeNode(thread.select(i))) root.add(thread_node) } @@ -201,11 +174,11 @@ for (i <- Range.inclusive(tree.getRowCount - 1, 1, -1)) tree.expandRow(i) new_tree_selection match { - case Some((thread_name, j)) => + case Some(c) => val i = - (for (t <- thread_entries.iterator.takeWhile(t => t.thread_name != thread_name)) - yield 1 + t.debug_states.length).sum - tree.addSelectionRow(i + j + 1) + (for (t <- threads.iterator.takeWhile(t => c.thread_name != t.thread_name)) + yield t.size).sum + tree.addSelectionRow(i + c.index + 1) case None => } @@ -215,11 +188,11 @@ def update_vals() { tree_selection() match { - case Some((t, None)) => - Debugger.clear_output(t.thread_name) - case Some((t, Some(i))) if i < t.debug_states.length => - Debugger.print_vals(t.thread_name, i, sml_button.selected, context_field.getText) - case _ => + case Some(c) if c.stack_state.isDefined => + Debugger.print_vals(c, sml_button.selected, context_field.getText) + case Some(c) => + Debugger.clear_output(c.thread_name) + case None => } } @@ -319,9 +292,8 @@ context_field.addCurrentToHistory() expression_field.addCurrentToHistory() tree_selection() match { - case Some((t, opt_index)) if t.debug_states.nonEmpty => - Debugger.eval(t.thread_name, opt_index getOrElse 0, - sml_button.selected, context_field.getText, expression_field.getText) + case Some(c) if c.debug_state_index.isDefined => + Debugger.eval(c, sml_button.selected, context_field.getText, expression_field.getText) case _ => } }