src/Pure/PIDE/command.ML
changeset 52853 4ab66773a41f
parent 52850 9fff9f78240a
child 52953 2c927b7501c5
equal deleted inserted replaced
52852:08ecbffaf25c 52853:4ab66773a41f
   219 fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
   219 fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
   220 
   220 
   221 fun print_finished (Print {print_process, ...}) = memo_finished print_process;
   221 fun print_finished (Print {print_process, ...}) = memo_finished print_process;
   222 
   222 
   223 fun print_persistent (Print {persistent, ...}) = persistent;
   223 fun print_persistent (Print {persistent, ...}) = persistent;
       
   224 
       
   225 val overlay_ord = prod_ord string_ord (list_ord string_ord);
   224 
   226 
   225 in
   227 in
   226 
   228 
   227 fun print command_visible command_overlays command_name eval old_prints =
   229 fun print command_visible command_overlays command_name eval old_prints =
   228   let
   230   let
   264           | SOME get_pr => new_print a b get_pr)
   266           | SOME get_pr => new_print a b get_pr)
   265       | some => some);
   267       | some => some);
   266 
   268 
   267     val new_prints =
   269     val new_prints =
   268       if command_visible then
   270       if command_visible then
   269         distinct (op =) (fold (fn (a, _) => cons (a, [])) print_functions command_overlays)
   271         fold (fn (a, _) => cons (a, [])) print_functions command_overlays
       
   272         |> sort_distinct overlay_ord
   270         |> map_filter get_print
   273         |> map_filter get_print
   271       else filter (fn print => print_finished print andalso print_persistent print) old_prints;
   274       else filter (fn print => print_finished print andalso print_persistent print) old_prints;
   272   in
   275   in
   273     if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
   276     if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
   274   end;
   277   end;