--- 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)
})
--- 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()
}
--- 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,