prefer canonical order, to avoid potential fluctuation due to front-end edits;
authorwenzelm
Fri, 02 Aug 2013 22:13:31 +0200
changeset 52853 4ab66773a41f
parent 52852 08ecbffaf25c
child 52854 92932931bd82
prefer canonical order, to avoid potential fluctuation due to front-end edits;
src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Aug 02 20:47:02 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Aug 02 22:13:31 2013 +0200
@@ -222,6 +222,8 @@
 
 fun print_persistent (Print {persistent, ...}) = persistent;
 
+val overlay_ord = prod_ord string_ord (list_ord string_ord);
+
 in
 
 fun print command_visible command_overlays command_name eval old_prints =
@@ -266,7 +268,8 @@
 
     val new_prints =
       if command_visible then
-        distinct (op =) (fold (fn (a, _) => cons (a, [])) print_functions command_overlays)
+        fold (fn (a, _) => cons (a, [])) print_functions command_overlays
+        |> sort_distinct overlay_ord
         |> map_filter get_print
       else filter (fn print => print_finished print andalso print_persistent print) old_prints;
   in