# HG changeset patch
# User wenzelm
# Date 1440438557 -7200
# Node ID 7c5a877b0f8ea9450037f8d8bb95aadfae8cee1a
# Parent  2c34ab15e3ebc25ae1ce93036a7dc9357a31571a
tuned;

diff -r 2c34ab15e3eb -r 7c5a877b0f8e src/Pure/Tools/debugger.scala
--- 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)
diff -r 2c34ab15e3eb -r 7c5a877b0f8e src/Tools/jEdit/src/debugger_dockable.scala
--- 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)
     }