# HG changeset patch
# User wenzelm
# Date 1516371613 -3600
# Node ID aad088768872c9dc985ad8ed543ad8ba366300a6
# Parent  7ed8d4cdfb13dd05de3cd0365745b16aa2d6598c
sort completion result;

diff -r 7ed8d4cdfb13 -r aad088768872 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Fri Jan 19 15:14:43 2018 +0100
+++ b/src/Pure/PIDE/resources.ML	Fri Jan 19 15:20:13 2018 +0100
@@ -89,6 +89,7 @@
           Completion.make (name, pos) (fn completed =>
               names
               |> filter completed
+              |> sort_strings
               |> map (fn a => (a, (kind, a))));
         val report = Markup.markup_report (Completion.reported_text completion);
       in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ report) end