equal
deleted
inserted
replaced
146 |
146 |
147 fun report () = |
147 fun report () = |
148 let val (keywords, commands) = CRITICAL (fn () => |
148 let val (keywords, commands) = CRITICAL (fn () => |
149 (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ())))) |
149 (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ())))) |
150 in map report_keyword keywords @ map report_command commands end |
150 in map report_keyword keywords @ map report_command commands end |
151 |> Pretty.chunks |> Pretty.string_of |> Output.status; |
151 |> List.app (Output.status o Pretty.string_of); |
152 |
152 |
153 |
153 |
154 (* augment tables *) |
154 (* augment tables *) |
155 |
155 |
156 fun keyword name = |
156 fun keyword name = |