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