prefer canonical order, to avoid potential fluctuation due to front-end edits;
authorwenzelm
Fri, 02 Aug 2013 22:13:31 +0200
changeset 539904ab66773a41f
parent 53989 08ecbffaf25c
child 53991 92932931bd82
prefer canonical order, to avoid potential fluctuation due to front-end edits;
src/Pure/PIDE/command.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Fri Aug 02 20:47:02 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Aug 02 22:13:31 2013 +0200
     1.3 @@ -222,6 +222,8 @@
     1.4  
     1.5  fun print_persistent (Print {persistent, ...}) = persistent;
     1.6  
     1.7 +val overlay_ord = prod_ord string_ord (list_ord string_ord);
     1.8 +
     1.9  in
    1.10  
    1.11  fun print command_visible command_overlays command_name eval old_prints =
    1.12 @@ -266,7 +268,8 @@
    1.13  
    1.14      val new_prints =
    1.15        if command_visible then
    1.16 -        distinct (op =) (fold (fn (a, _) => cons (a, [])) print_functions command_overlays)
    1.17 +        fold (fn (a, _) => cons (a, [])) print_functions command_overlays
    1.18 +        |> sort_distinct overlay_ord
    1.19          |> map_filter get_print
    1.20        else filter (fn print => print_finished print andalso print_persistent print) old_prints;
    1.21    in