equal
deleted
inserted
replaced
628 Pretty.big_list "case translations:" (map #2 (sort_wrt #1 (map pretty_data cases))) |
628 Pretty.big_list "case translations:" (map #2 (sort_wrt #1 (map pretty_data cases))) |
629 |> Pretty.writeln |
629 |> Pretty.writeln |
630 end; |
630 end; |
631 |
631 |
632 val _ = |
632 val _ = |
633 Outer_Syntax.command @{command_spec "print_case_translations"} |
633 Outer_Syntax.command @{command_keyword print_case_translations} |
634 "print registered case combinators and constructors" |
634 "print registered case combinators and constructors" |
635 (Scan.succeed (Toplevel.keep (print_case_translations o Toplevel.context_of))) |
635 (Scan.succeed (Toplevel.keep (print_case_translations o Toplevel.context_of))) |
636 |
636 |
637 end; |
637 end; |