# HG changeset patch
# User wenzelm
# Date 1261404822 -3600
# Node ID e65352f1242115abe4f86dae8accd944f08b7761
# Parent  c97335b7e8c3c4a3f57e89a29ea95c5be9907024
sort completions by plain string order;

diff -r c97335b7e8c3 -r e65352f12421 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Fri Dec 18 21:46:29 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Mon Dec 21 15:13:42 2009 +0100
@@ -92,7 +92,7 @@
       case Some((word, cs)) =>
         val ds =
           if (Isabelle_Encoding.is_active(buffer))
-            cs.map(Isabelle.system.symbols.decode(_)).sort(Completion.length_ord _)
+            cs.map(Isabelle.system.symbols.decode(_)).sort(_ < _)
           else cs
         new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
     }