more flexible sorting;
authorwenzelm
Thu Sep 01 14:10:52 2011 +0200 (2011-09-01)
changeset 446175db68864a967
parent 44616 4beeaf2a226d
child 44638 74fb317aaeb5
more flexible sorting;
tuned display;
src/Pure/library.ML
src/Pure/library.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Pure/library.ML	Thu Sep 01 13:39:40 2011 +0200
     1.2 +++ b/src/Pure/library.ML	Thu Sep 01 14:10:52 2011 +0200
     1.3 @@ -959,7 +959,7 @@
     1.4  fun sort_distinct ord = quicksort true ord;
     1.5  
     1.6  val sort_strings = sort string_ord;
     1.7 -fun sort_wrt sel xs = sort (string_ord o pairself sel) xs;
     1.8 +fun sort_wrt key xs = sort (string_ord o pairself key) xs;
     1.9  
    1.10  
    1.11  (* items tagged by integer index *)
     2.1 --- a/src/Pure/library.scala	Thu Sep 01 13:39:40 2011 +0200
     2.2 +++ b/src/Pure/library.scala	Thu Sep 01 14:10:52 2011 +0200
     2.3 @@ -14,6 +14,7 @@
     2.4  import scala.swing.ComboBox
     2.5  import scala.swing.event.SelectionChanged
     2.6  import scala.collection.mutable
     2.7 +import scala.math.Ordering
     2.8  import scala.util.Sorting
     2.9  
    2.10  
    2.11 @@ -62,13 +63,18 @@
    2.12  
    2.13    def split_lines(str: String): List[String] = space_explode('\n', str)
    2.14  
    2.15 -  def sort_strings(args: Seq[String]): List[String] =
    2.16 +  def sort_wrt[A](key: A => String, args: Seq[A]): List[A] =
    2.17    {
    2.18 -    val a = args.toArray
    2.19 -    Sorting.quickSort(a)
    2.20 +    val ordering: Ordering[A] =
    2.21 +      new Ordering[A] { def compare(x: A, y: A): Int = key(x) compare key(y) }
    2.22 +    val a = (new Array[Any](args.length)).asInstanceOf[Array[A]]
    2.23 +    for ((x, i) <- args.iterator zipWithIndex) a(i) = x
    2.24 +    Sorting.quickSort[A](a)(ordering)
    2.25      a.toList
    2.26    }
    2.27  
    2.28 +  def sort_strings(args: Seq[String]): List[String] = sort_wrt((x: String) => x, args)
    2.29 +
    2.30  
    2.31    /* iterate over chunks (cf. space_explode) */
    2.32  
     3.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Thu Sep 01 13:39:40 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Thu Sep 01 14:10:52 2011 +0200
     3.3 @@ -73,7 +73,7 @@
     3.4  
     3.5    /* component state -- owned by Swing thread */
     3.6  
     3.7 -  private var nodes_status: Map[String, String] = Map.empty
     3.8 +  private var nodes_status: Map[Document.Node.Name, String] = Map.empty
     3.9  
    3.10    private def handle_changed(changed_nodes: Set[Document.Node.Name])
    3.11    {
    3.12 @@ -88,12 +88,13 @@
    3.13              name <- changed_nodes
    3.14              node <- version.nodes.get(name)
    3.15              val status = Isar_Document.node_status(state, version, node)
    3.16 -          } nodes_status1 += (name.node -> status.toString)
    3.17 +          } nodes_status1 += (name -> status.toString)
    3.18  
    3.19            if (nodes_status != nodes_status1) {
    3.20              nodes_status = nodes_status1
    3.21 -            val order = Library.sort_strings(nodes_status.keySet.toList)
    3.22 -            status.listData = order.map(name => name + " " + nodes_status(name))
    3.23 +            val order =
    3.24 +              Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList)
    3.25 +            status.listData = order.map(name => name.theory + " " + nodes_status(name))
    3.26            }
    3.27        }
    3.28      }