--- a/src/Pure/Tools/debugger.scala Mon Aug 24 11:45:26 2015 +0200
+++ b/src/Pure/Tools/debugger.scala Mon Aug 24 19:49:17 2015 +0200
@@ -7,6 +7,9 @@
package isabelle
+import scala.collection.immutable.SortedMap
+
+
object Debugger
{
/* context */
@@ -46,12 +49,14 @@
/* 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
- 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
{
@@ -222,7 +227,7 @@
})
}
- def threads(): Map[String, List[Debug_State]] = global_state.value.threads
+ def threads(): Threads = global_state.value.threads
def focus(): List[Context] = global_state.value.focus.toList.map(_._2)
def set_focus(c: Context)
--- a/src/Tools/jEdit/src/debugger_dockable.scala Mon Aug 24 11:45:26 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Mon Aug 24 19:49: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
@@ -108,7 +109,7 @@
if (new_threads != current_threads) {
val threads =
(for ((a, b) <- new_threads.iterator)
- yield Debugger.Context(a, b)).toList.sortBy(_.thread_name)
+ yield Debugger.Context(a, b)).toList
update_tree(threads)
}