# HG changeset patch
# User wenzelm
# Date 1421618820 -3600
# Node ID 5d08b2332b765a017d8650a524688898d53e6456
# Parent  db65d45b6740ff11755f05af1f8d873651577968
discontinued attempt at alphabetic_order -- selection via regex should be sufficient;

diff -r db65d45b6740 -r 5d08b2332b76 src/Tools/Graphview/tree_panel.scala
--- a/src/Tools/Graphview/tree_panel.scala	Sun Jan 18 22:46:38 2015 +0100
+++ b/src/Tools/Graphview/tree_panel.scala	Sun Jan 18 23:07:00 2015 +0100
@@ -93,15 +93,6 @@
 
   /* controls */
 
-  private val alphabetic = new CheckBox {
-    tooltip = "Alphabetic order instead of topological order"
-    selected = visualizer.alphabetic_order
-    action = Action("Alphabetic order") {
-      visualizer.alphabetic_order = selected
-      refresh()
-    }
-  }
-
   private var selection_pattern: Option[Regex] = None
 
   private def selection_filter(node: Graph_Display.Node): Boolean =
@@ -151,7 +142,6 @@
   }
 
   private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
-    // FIXME alphabetic,
     selection_label, selection_field, selection_apply)
 
 
@@ -159,12 +149,7 @@
 
   def refresh()
   {
-    val new_nodes =
-      if (visualizer.alphabetic_order)
-        visualizer.visible_graph.keys_iterator.toList
-      else
-        visualizer.visible_graph.topological_order
-
+    val new_nodes = visualizer.visible_graph.topological_order
     if (new_nodes != nodes) {
       nodes = new_nodes
 
diff -r db65d45b6740 -r 5d08b2332b76 src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Sun Jan 18 22:46:38 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Sun Jan 18 23:07:00 2015 +0100
@@ -144,7 +144,6 @@
       Shapes.paint_node(gfx, visualizer, node)
   }
 
-  var alphabetic_order: Boolean = false
   var current_node: Option[Graph_Display.Node] = None
 
   object Selection